Displaying similar documents to “ On L 1 Space Formed by Complex-Valued Partial Functions ”

On L 1 Space Formed by Real-Valued Partial Functions

Yasushige Watase, Noboru Endou, Yasunari Shidama (2008)

Formalized Mathematics

Similarity:

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

On L p Space Formed by Real-Valued Partial Functions

Yasushige Watase, Noboru Endou, Yasunari Shidama (2010)

Formalized Mathematics

Similarity:

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

The Vector Space of Subsets of a Set Based on Symmetric Difference

Jesse Alama (2008)

Formalized Mathematics

Similarity:

For each set X, the power set of X forms a vector space over the field Z2 (the two-element field {0, 1} with addition and multiplication done modulo 2): vector addition is disjoint union, and scalar multiplication is defined by the two equations (1 · x:= x, 0 · x := ∅ for subsets x of X). See [10], Exercise 2.K, for more information.MML identifier: BSPACE, version: 7.8.05 4.89.993

On systems of null sets

K. Bhaskara Rao, R. Shortt (1999)

Colloquium Mathematicae

Similarity:

The collection of all sets of measure zero for a finitely additive, group-valued measure is studied and characterised from a combinatorial viewpoint.

The C k Space

Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama (2013)

Formalized Mathematics

Similarity:

In this article, we formalize continuous differentiability of realvalued functions on n-dimensional real normed linear spaces. Next, we give a definition of the Ck space according to [23].