Displaying similar documents to “The Measurability of Complex-Valued Functional Sequences”

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

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

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.

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

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.

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

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

Arithmetic Operations on Functions from Sets into Functional Sets

Artur Korniłowicz (2009)

Formalized Mathematics

Similarity:

In this paper we introduce sets containing number-valued functions. Different arithmetic operations on maps between any set and such functional sets are later defined.MML identifier: VALUED 2, version: 7.11.01 4.117.1046