Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm
Okazaki, Hiroyuki, Nagao, Koh-ichi, Futa, Yuichi
Banach Algebra of Bounded Complex-Valued Functionals
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Higher-Order Partial Differentiation
Endou, Noboru, Okazaki, Hiroyuki, Shidama, Yasunari
Probability on Finite and Discrete Set and Uniform Distribution
Okazaki, Hiroyuki
Normal Subgroup of Product of Groups
Okazaki, Hiroyuki, Arai, Kenichi, Shidama, Yasunari
Functional Space C(ω), C0(ω)
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of Orthogonal Complements of Normed Spaces
Okazaki, Hiroyuki
Probability on Finite Set and Real-Valued Random Variables
Okazaki, Hiroyuki, Shidama, Yasunari
On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors
Okazaki, Hiroyuki
Posterior Probability on Finite Set
Okazaki, Hiroyuki
Real Vector Space and Related Notions
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki