Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki
Formalization of the Advanced Encryption Standard. Part I
Arai, Kenichi, Okazaki, Hiroyuki
Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables
Okazaki, Hiroyuki, Shidama, Yasunari
Inferior Limit, Superior Limit and Convergence of Sequences of Extended Real Numbers
Yamazaki, Hiroshi, Endou, Noboru, Shidama, Yasunari, Okazaki, Hiroyuki
Extended Euclidean Algorithm and CRT Algorithm
Okazaki, Hiroyuki, Aoki, Yosiki, Shidama, Yasunari
Formalization of Separable Version of Banach–Alaoglu Theorem
Okazaki, Hiroyuki, Mieno, Takehiko
Cartesian Products of Family of Real Linear Spaces
Okazaki, Hiroyuki, Endou, Noboru, Shidama, Yasunari