Displaying similar documents to “Banach Algebra of Bounded Complex-Valued Functionals”

Dual Spaces and Hahn-Banach Theorem

Keiko Narita, Noboru Endou, Yasunari Shidama (2014)

Formalized Mathematics

Similarity:

In this article, we deal with dual spaces and the Hahn-Banach Theorem. At the first, we defined dual spaces of real linear spaces and proved related basic properties. Next, we defined dual spaces of real normed spaces. We formed the definitions based on dual spaces of real linear spaces. In addition, we proved properties of the norm about elements of dual spaces. For the proof we referred to descriptions in the article [21]. Finally, applying theorems of the second section, we proved...

Functional Space C (ω), C 0 (ω)

Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama (2012)

Formalized Mathematics

Similarity:

In this article, first we give a definition of a functional space which is constructed from all complex-valued continuous functions defined on a compact topological space. We prove that this functional space is a Banach algebra. Next, we give a definition of a function space which is constructed from all complex-valued continuous functions with bounded support. We also prove that this function space is a complex normed space.

Banach Algebra of Bounded Functionals

Yasunari Shidama, Hikofumi Suzuki, Noboru Endou (2008)

Formalized Mathematics

Similarity:

In this article, we describe some basic properties of the Banach algebra which is constructed from all bounded functionals.MML identifier: C0SP1, version: 7.8.10 4.99.1005

Banach Algebra of Continuous Functionals and the Space of Real-Valued Continuous Functionals with Bounded Support

Katuhiko Kanazashi, Noboru Endou, Yasunari Shidama (2010)

Formalized Mathematics

Similarity:

In this article, we give a definition of a functional space which is constructed from all continuous functions defined on a compact topological space. We prove that this functional space is a Banach algebra. Next, we give a definition of a function space which is constructed from all real-valued continuous functions with bounded support. We prove that this function space is a real normed space.

Banach’s Continuous Inverse Theorem and Closed Graph Theorem

Hideki Sakurai, Hiroyuki Okazaki, Yasunari Shidama (2012)

Formalized Mathematics

Similarity:

In this article we formalize one of the most important theorems of linear operator theory - the Closed Graph Theorem commonly used in a standard text book such as [10] in Chapter 24.3. It states that a surjective closed linear operator between Banach spaces is bounded.

Cartesian Products of Family of Real Linear Spaces

Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama (2011)

Formalized Mathematics

Similarity:

In this article we introduced the isomorphism mapping between cartesian products of family of linear spaces [4]. Those products had been formalized by two different ways, i.e., the way using the functor [:X, Y:] and ones using the functor "product". By the same way, the isomorphism mapping was defined between Cartesian products of family of linear normed spaces also.

Riemann Integral of Functions from R into Real Normed Space

Keiichi Miyajima, Takahiro Kato, Yasunari Shidama (2011)

Formalized Mathematics

Similarity:

In this article, we define the Riemann integral on functions from R into real normed space and prove the linearity of this operator. As a result, the Riemann integration can be applied to a wider range of functions. The proof method follows the [16].

Contracting Mapping on Normed Linear Space

Keiichi Miyajima, Artur Korniłowicz, Yasunari Shidama (2012)

Formalized Mathematics

Similarity:

In this article, we described the contracting mapping on normed linear space. Furthermore, we applied that mapping to ordinary differential equations on real normed space. Our method is based on the one presented by Schwarz [29].