Displaying similar documents to “The First Mean Value Theorem for Integrals”

Integral of Complex-Valued Measurable Function

Keiko Narita, Noboru Endou, Yasunari Shidama (2008)

Formalized Mathematics

Similarity:

In this article, we formalized the notion of the integral of a complex-valued function considered as a sum of its real and imaginary parts. Then we defined the measurability and integrability in this context, and proved the linearity and several other basic properties of complex-valued measurable functions. The set of properties showed in this paper is based on [15], where the case of real-valued measurable functions is considered.MML identifier: MESFUN6C, version: 7.9.01 4.101.1015 ...

Egoroff's Theorem

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

The Measurability of Complex-Valued Functional Sequences

Keiko Narita, Noboru Endou, Yasunari Shidama (2009)

Formalized Mathematics

Similarity:

In this article, we formalized the measurability of complex-valued functional sequences. First, we proved the measurability of the limits of real-valued functional sequences. Next, we defined complex-valued functional sequences dividing real part into imaginary part. Then using the former theorems, we proved the measurability of each part. Lastly, we proved the measurability of the limits of complex-valued functional sequences. We also showed several properties of complex-valued measurable...

Lebesgue's Convergence Theorem of Complex-Valued Function

Keiko Narita, Noboru Endou, Yasunari Shidama (2009)

Formalized Mathematics

Similarity:

In this article, we formalized Lebesgue's Convergence theorem of complex-valued function. We proved Lebesgue's Convergence Theorem of realvalued function using the theorem of extensional real-valued function. Then applying the former theorem to real part and imaginary part of complex-valued functional sequences, we proved Lebesgue's Convergence Theorem of complex-valued function. We also defined partial sums of real-valued functional sequences and complex-valued functional sequences...

Fatou's Lemma and the Lebesgue's Convergence Theorem

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

The Lebesgue Monotone Convergence Theorem

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

Sorting by Exchanging

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.

Integral of Real-Valued Measurable Function 1

Yasunari Shidama, Noboru Endou (2006)

Formalized Mathematics

Similarity:

Based on [16], authors formalized the integral of an extended real valued measurable function in [12] before. However, the integral argued in [12] cannot be applied to real-valued functions unconditionally. Therefore, in this article we have formalized the integral of a real-value function.

More on Continuous Functions on Normed Linear Spaces

Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama (2011)

Formalized Mathematics

Similarity:

In this article we formalize the definition and some facts about continuous functions from R into normed linear spaces [14].

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