Page 1

Displaying 1 – 9 of 9

Showing per page

The First Mean Value Theorem for Integrals

Keiko Narita, Noboru Endou, Yasunari Shidama (2008)

Formalized Mathematics

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

Noboru Endou, Keiko Narita, Yasunari Shidama (2008)

Formalized Mathematics

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 n

W. Banaszczyk (1997)

Studia Mathematica

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 G p c (resp. G b ) 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 n -dual space of the space of p -summable sequences

Yosafat E. P. Pangalela, Hendra Gunawan (2013)

Mathematica Bohemica

In the theory of normed spaces, we have the concept of bounded linear functionals and dual spaces. Now, given an n -normed space, we are interested in bounded multilinear n -functionals and n -dual spaces. The concept of bounded multilinear n -functionals on an n -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 n -functionals, introduce the concept of n -dual spaces, and...

The Orthogonal Projection and the Riesz Representation Theorem

Keiko Narita, Noboru Endou, Yasunari Shidama (2015)

Formalized Mathematics

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

Taras Banakh, Igor Zarichnyy (2008)

Open Mathematics

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...

Currently displaying 1 – 9 of 9

Page 1