Displaying similar documents to “ Integral of Measurable Function 1 ”

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.

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

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

The First Mean Value Theorem for Integrals

Keiko Narita, Noboru Endou, Yasunari Shidama (2008)

Formalized Mathematics

Similarity:

In this article, we prove the first mean value theorem for integrals [16]. The formalization of various theorems about the properties of the Lebesgue integral is also presented.MML identifier: MESFUNC7, version: 7.8.09 4.97.1001

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