Noboru Endou, Keiko Narita, Yasunari Shidama (2008)
Formalized Mathematics
Similarity:
In this article we prove the Fatou's Lemma and Lebesgue's Convergence Theorem [10].MML identifier: MESFUN10, version: 7.9.01 4.101.1015
Noboru Endou, Keiko Narita, Yasunari Shidama (2008)
Formalized Mathematics
Similarity:
In this article we prove the Monotone Convergence Theorem [16].MML identifier: MESFUNC9, version: 7.8.10 4.100.1011
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]).
Keiichi Miyajima, Artur Korniłowicz, Yasunari Shidama (2012)
Formalized Mathematics
Similarity:
In this article, we define the Riemann integral on functions R into n-dimensional real normed space and prove the linearity of this operator. As a result, the Riemann integration can be applied to the wider range. Our method refers to the [21].
Grzegorz Bancerek (2011)
Formalized Mathematics
Similarity:
We show that exchanging of pairs in an array which are in incorrect order leads to sorted array. It justifies correctness of Bubble Sort, Insertion Sort, and Quicksort.
Keiko Narita, Artur Kornilowicz, Yasunari Shidama (2011)
Formalized Mathematics
Similarity:
In this article we demonstrate basic properties of the continuous functions from R to Rn which correspond to state space equations in control engineering.
Keiko Narita, Noboru Endou, Yasunari Shidama (2013)
Formalized Mathematics
Similarity:
In this article we deal with the Riemann integral of functions from R into a real Banach space. The last theorem establishes the integrability of continuous functions on the closed interval of reals. To prove the integrability we defined uniform continuity for functions from R into a real normed space, and proved related theorems. We also stated some properties of finite sequences of elements of a real normed space and finite sequences of real numbers. In addition we proved some theorems...
Keiko Narita, Noboru Endou, Yasunari Shidama (2013)
Formalized Mathematics
Similarity:
In this article, we described basic properties of Riemann integral on functions from R into Real Banach Space. We proved mainly the linearity of integral operator about the integral of continuous functions on closed interval of the set of real numbers. These theorems were based on the article [10] and we referred to the former articles about Riemann integral. We applied definitions and theorems introduced in the article [9] and the article [11] to the proof. Using the definition of the...
Noboru Endou, Yasunari Shidama, Keiko Narita (2008)
Formalized Mathematics
Similarity:
The goal of this article is to prove Egoroff's Theorem [13]. However, there are not enough theorems related to sequence of measurable functions in Mizar Mathematical Library. So we proved many theorems about them. At the end of this article, we showed Egoroff's theorem.MML identifier: MESFUNC8, version: 7.8.10 4.100.1011
Francesco Saverio De Blasi, Giulio Pianigiani (1999)
Commentationes Mathematicae Universitatis Carolinae
Similarity:
We study a Cauchy problem for non-convex valued evolution inclusions in non separable Banach spaces under Filippov type assumptions. We establish existence and relaxation theorems.