The Distortion of Hilbert Space.
The First Mean Value Theorem for Integrals
In this article, we prove the first mean value theorem for integrals [16]. The formalization of various theorems about the properties of the Lebesgue integral is also presented.MML identifier: MESFUNC7, version: 7.8.09 4.97.1001
The Lebesgue Monotone Convergence Theorem
In this article we prove the Monotone Convergence Theorem [16].MML identifier: MESFUNC9, version: 7.8.10 4.100.1011
The Minlos lemma for positive-definite functions on additive subgroups of
Let H be a real Hilbert space. It is well known that a positive-definite function φ on H is the Fourier transform of a Radon measure on the dual space if (and only if) φ is continuous in the Sazonov topology (resp. the Gross topology) on H. Let G be an additive subgroup of H and let (resp. ) be the character group endowed with the topology of uniform convergence on precompact (resp. bounded) subsets of G. It is proved that if a positive-definite function φ on G is continuous in the Gross topology,...
The -dual space of the space of -summable sequences
In the theory of normed spaces, we have the concept of bounded linear functionals and dual spaces. Now, given an -normed space, we are interested in bounded multilinear -functionals and -dual spaces. The concept of bounded multilinear -functionals on an -normed space was initially intoduced by White (1969), and studied further by Batkunde et al., and Gozali et al. (2010). In this paper, we revisit the definition of bounded multilinear -functionals, introduce the concept of -dual spaces, and...
The Orthogonal Projection and the Riesz Representation Theorem
In this article, the orthogonal projection and the Riesz representation theorem are mainly formalized. In the first section, we defined the norm of elements on real Hilbert spaces, and defined Mizar functor RUSp2RNSp, real normed spaces as real Hilbert spaces. By this definition, we regarded sequences of real Hilbert spaces as sequences of real normed spaces, and proved some properties of real Hilbert spaces. Furthermore, we defined the continuity and the Lipschitz the continuity of functionals...
Topological groups and convex sets homeomorphic to non-separable Hilbert spaces
Let X be a topological group or a convex set in a linear metric space. We prove that X is homeomorphic to (a manifold modeled on) an infinite-dimensional Hilbert space if and only if X is a completely metrizable absolute (neighborhood) retract with ω-LFAP, the countable locally finite approximation property. The latter means that for any open cover of X there is a sequence of maps (f n: X → X)nεgw such that each f n is -near to the identity map of X and the family f n(X)n∈ω is locally finite...
Total Minimality of the Unitary Groups.
Two examples of non-separable metrizable spaces