In this article we introduce the convergence of extended realvalued double sequences , . It is similar to our previous articles , . In addition, we also prove Fatou’s lemma and the monotone convergence theorem for double sequences.
The purpose of this article is to show Fubini’s theorem on measure , , , , . Some theorems have the possibility of slight generalization, but we have priority to avoid the complexity of the description. First of all, for the product measure constructed in , we show some theorems. Then we introduce the section which plays an important role in Fubini’s theorem, and prove the relevant proposition. Finally we show Fubini’s theorem on measure.
In our previous article , we showed complete additivity as a condition for extension of a measure. However, this condition premised the existence of a σ-field and the measure on it. In general, the existence of the measure on σ-field is not obvious. On the other hand, the proof of existence of a measure on a semialgebra is easier than in the case of a σ-field. Therefore, in this article we define a measure (pre-measure) on a semialgebra and extend it to a measure on a σ-field. Furthermore, we give a σ-measure as an extension of the measure on a σ-field. We follow , , and .
In this paper the author constructs several properties for double series and its convergence. The notions of convergence of double sequence have already been introduced in our previous paper . In section 1 we introduce double series and their convergence. Then we show the relationship between Pringsheim-type convergence and iterated convergence. In section 2 we study double series having non-negative terms. As a result, we have equality of three type sums of non-negative double sequence. In section 3 we show that if a non-negative sequence is summable, then the sequence of rearrangement of terms is summable and it has the same sums. In the last section two basic relations between double sequences and matrices are introduced.
The goal of this article is to show Fubini’s theorem for non-negative or non-positive measurable functions , , , using the Mizar system , . We formalized Fubini’s theorem in our previous article , but in that case we showed the Fubini’s theorem for measurable sets and it was not enough as the integral does not appear explicitly.
On the other hand, the theorems obtained in this paper are more general and it can be easily extended to a general integrable function. Furthermore, it also can be easy to extend to functional space Lp . It should be mentioned also that Hölzl and Heller  have introduced the Lebesgue integration theory in Isabelle/HOL and have proved Fubini’s theorem there.
In this article we formalize in Mizar  product pre-measure on product sets of measurable sets. Although there are some approaches to construct product measure , , , , , we start it from σ-measure because existence of σ-measure on any semialgebras has been proved in . In this approach, we use some theorems for integrals.
Fubini theorem is an essential tool for the analysis of high-dimensional space , , , a theorem about the multiple integral and iterated integral. The author has been working on formalizing Fubini’s theorem over the past few years ,  in the Mizar system , . As a result, Fubini’s theorem (30) was proved in complete form by this article.
In the Mizar system (, ), Józef Białas has already given the one-dimensional Lebesgue measure . However, the measure introduced by Białas limited the outer measure to a field with finite additivity. So, although it satisfies the nature of the measure, it cannot specify the length of measurable sets and also it cannot determine what kind of set is a measurable set. From the above, the authors first determined the length of the interval by the outer measure. Specifically, we used the compactness of the real space. Next, we constructed the pre-measure by limiting the outer measure to a semialgebra of intervals. Furthermore, by repeating the extension of the previous measure, we reconstructed the one-dimensional Lebesgue measure , .
In this article we formalized the Fréchet differentiation. It is defined as a generalization of the differentiation of a real-valued function of a single real variable to more general functions whose domain and range are subsets of normed spaces .