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]).
Yasushige Watase, Noboru Endou, Yasunari Shidama (2012)
Formalized Mathematics
Similarity:
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.
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
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.
Artur Korniłowicz (2010)
Formalized Mathematics
Similarity:
We prove that basic arithmetic operations preserve continuity of functions.
Haluška, Ján, Hutník, Ondrej (2010)
Banach Journal of Mathematical Analysis [electronic only]
Similarity:
K. Bhaskara Rao, R. Shortt (1992)
Colloquium Mathematicae
Similarity:
Takao Inoué, Noboru Endou, Yasunari Shidama (2010)
Formalized Mathematics
Similarity:
In this article, we define and develop differentiation of vector-valued functions on n-dimensional real normed linear spaces (refer to [16] and [17]).
Takao Inoué, Adam Naumowicz, Noboru Endou, Yasunari Shidama (2011)
Formalized Mathematics
Similarity:
In this article, we define and develop partial differentiation of vector-valued functions on n-dimensional real normed linear spaces (refer to [19] and [20]).
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].
Grzegorz Bancerek (2012)
Formalized Mathematics
Similarity:
In the paper the semantics of MML Query queries is given. The formalization is done according to [4]