Formalization of Separable Version of Banach–Alaoglu Theorem
Okazaki, Hiroyuki, Mieno, Takehiko
Posterior Probability on Finite Set
Okazaki, Hiroyuki
Inferior Limit, Superior Limit and Convergence of Sequences of Extended Real Numbers
Yamazaki, Hiroshi, Endou, Noboru, Shidama, Yasunari, Okazaki, Hiroyuki
Quotient Module of Z-module
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Uniqueness of Factoring an Integer and Multiplicative Group Z/pZ*
Okazaki, Hiroyuki, Shidama, Yasunari
Polynomially Bounded Sequences and Polynomial Sequences
Okazaki, Hiroyuki, Futa, Yuichi
Higher-Order Partial Differentiation
Endou, Noboru, Okazaki, Hiroyuki, Shidama, Yasunari
The Ck Space
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Finite Dimensional Real Normed Spaces are Proper Metric Spaces
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Shidama, Yasunari
Probability on Finite and Discrete Set and Uniform Distribution
Okazaki, Hiroyuki
On the Formalization of Gram-Schmidt Process for Orthonormalizing a Set of Vectors
Okazaki, Hiroyuki
Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki