Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables
Okazaki, Hiroyuki, Shidama, Yasunari
Binary Representation of Natural Numbers
Okazaki, Hiroyuki
Torsion Z-module and Torsion-free Z-module
Futa, Yuichi, Okazaki, Hiroyuki, Nakasho, Kazuhisa, Shidama, Yasunari
Algebra of Polynomially Bounded Sequences and Negligible Functions
Okazaki, Hiroyuki
Banach Algebra of Bounded Complex-Valued Functionals
Kanazashi, Katuhiko, Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of Orthogonal Decomposition for Hilbert Spaces
Okazaki, Hiroyuki
Isomorphisms of Direct Products of Finite Commutative Groups
Okazaki, Hiroyuki, Yamazaki, Hiroshi, Shidama, Yasunari
Random Variables and Product of Probability Spaces
Okazaki, Hiroyuki, Shidama, Yasunari
Formalization of Integral Linear Space
Futa, Yuichi, Okazaki, Hiroyuki, Shidama, Yasunari
Equivalent Expressions of Direct Sum Decomposition of Groups1
Nakasho, Kazuhisa, Okazaki, Hiroyuki, Yamazaki, Hiroshi, Shidama, Yasunari
Double Sequences and Limits
Endou, Noboru, Okazaki, Hiroyuki, Shidama, Yasunari
More on Continuous Functions on Normed Linear Spaces
Okazaki, Hiroyuki, Endou, Noboru, Shidama, Yasunari