Page 1 Next

Displaying 1 – 20 of 78

Showing per page

Banach’s Continuous Inverse Theorem and Closed Graph Theorem

Hideki Sakurai, Hiroyuki Okazaki, Yasunari Shidama (2012)

Formalized Mathematics

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.

On L 1 Space Formed by Complex-Valued Partial Functions

Yasushige Watase, Noboru Endou, Yasunari Shidama (2012)

Formalized Mathematics

In this article, we formalized L1 space formed by complexvalued partial functions [11], [15]. The real-valued case was formalized in [22] and this article is its generalization.

On L 1 Space Formed by Real-Valued Partial Functions

Yasushige Watase, Noboru Endou, Yasunari Shidama (2008)

Formalized Mathematics

This article contains some definitions and properties refering to function spaces formed by partial functions defined over a measurable space. We formalized a function space, the so-called L1 space and proved that the space turns out to be a normed space. The formalization of a real function space was given in [16]. The set of all function forms additive group. Here addition is defined by point-wise addition of two functions. However it is not true for partial functions. The set of partial functions...

On L p Space Formed by Real-Valued Partial Functions

Yasushige Watase, Noboru Endou, Yasunari Shidama (2010)

Formalized Mathematics

This article is the continuation of [31]. We define the set of Lp integrable functions - the set of all partial functions whose absolute value raised to the p-th power is integrable. We show that Lp integrable functions form the Lp space. We also prove Minkowski's inequality, Hölder's inequality and that Lp space is Banach space ([15], [27]).

Currently displaying 1 – 20 of 78

Page 1 Next