<abstract xmlns="http://www.w3.org/1999/xhtml">The goal of this article is to show Fubini’s theorem for non-negative or non-positive measurable functions [<xref ref-type="bibr" rid="j_forma-2018-0005_ref_010_w2aab3b7b4b1b6b1ab1ac10Aa">10</xref>], [<xref ref-type="bibr" rid="j_forma-2018-0005_ref_002_w2aab3b7b4b1b6b1ab1ab2Aa">2</xref>], [<xref ref-type="bibr" rid="j_forma-2018-0005_ref_003_w2aab3b7b4b1b6b1ab1ab3Aa">3</xref>], using the Mizar system [<xref ref-type="bibr" rid="j_forma-2018-0005_ref_001_w2aab3b7b4b1b6b1ab1ab1Aa">1</xref>], [<xref ref-type="bibr" rid="j_forma-2018-0005_ref_009_w2aab3b7b4b1b6b1ab1ab9Aa">9</xref>]. We formalized Fubini’s theorem in our previous article [<xref ref-type="bibr" rid="j_forma-2018-0005_ref_005_w2aab3b7b4b1b6b1ab1ab5Aa">5</xref>], 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 <italic>Lp</italic> [<xref ref-type="bibr" rid="j_forma-2018-0005_ref_012_w2aab3b7b4b1b6b1ab1ac12Aa">12</xref>]. It should be mentioned also that Hölzl and Heller [<xref ref-type="bibr" rid="j_forma-2018-0005_ref_011_w2aab3b7b4b1b6b1ab1ac11Aa">11</xref>] have introduced the Lebesgue integration theory in Isabelle/HOL and have proved Fubini’s theorem there.</abstract>

The goal of this article is to show Fubini’s theorem for non-negative or non-positive measurable functions [10], [2], [3], using the Mizar system [1], [9]. We formalized Fubini’s theorem in our previous article [5], 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 [12]. It should be mentioned also that Hölzl and Heller [11] have introduced the Lebesgue integration theory in Isabelle/HOL and have proved Fubini’s theorem there.

Fubini’s Theorem for Non-Negative or Non-Positive Functions

National Institute of Technology, Gifu College

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Fubini\u2019s Theorem for Non-Negative or Non-Positive Functions"}

The goal of this article is to show Fubini’s theorem for non-negative or non-positive measurable functions [10], [2], [3], using the Mizar system [1], [9]. We...

Fubini’s Theorem for Non-Negative or Non-Positive Functions

Publicado en línea: 28 jul 2018

Páginas: 49 - 67

Recibido: 27 mar 2018

DOI: https://doi.org/10.2478/forma-2018-0005

Palabras clave
Fubini’ s theorem, extended real-valued non-negative (or non-positive) measurable function

© 2018 Noboru Endou, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Fubini’s Theorem for Non-Negative or Non-Positive Functions

Publicado en línea: 28 jul 2018

Páginas: 49 - 67

Recibido: 27 mar 2018

DOI: https://doi.org/10.2478/forma-2018-0005

Palabras claveFubini’ s theorem, extended real-valued non-negative (or non-positive) measurable function

© 2018 Noboru Endou, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Palabras clave
Fubini’ s theorem, extended real-valued non-negative (or non-positive) measurable function