Displaying similar documents to “ Integral of Real-Valued Measurable Function 1 ”

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

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

Some Remarks on Indicatrices of Measurable Functions

Marcin Kysiak (2005)

Bulletin of the Polish Academy of Sciences. Mathematics

Similarity:

We show that for a wide class of σ-algebras 𝓐, indicatrices of 𝓐-measurable functions admit the same characterization as indicatrices of Lebesgue-measurable functions. In particular, this applies to functions measurable in the sense of Marczewski.

On measurable relation

C. Himmelberg, T. Parthasarathy, F. Van Vleck (1981)

Fundamenta Mathematicae

Similarity: