The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
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]