<abstract xmlns="http://www.w3.org/1999/xhtml">Some authors have formalized the integral in the Mizar Mathematical Library (MML). The first article in a series on the Darboux/Riemann integral was written by Noboru Endou and Artur Korniłowicz: [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_006_w2aab3b7b5b1b6b1ab1ab6Aa">6</xref>]. The Lebesgue integral was formalized a little later [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_013_w2aab3b7b5b1b6b1ab1ac13Aa">13</xref>] and recently the integral of Riemann-Stieltjes was introduced in the MML by Keiko Narita, Kazuhisa Nakasho and Yasunari Shidama [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_012_w2aab3b7b5b1b6b1ab1ac12Aa">12</xref>].A presentation of definitions of integrals in other proof assistants or proof checkers (ACL2, COQ, Isabelle/HOL, HOL4, HOL Light, PVS, ProofPower) may be found in [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_010_w2aab3b7b5b1b6b1ab1ac10Aa">10</xref>] and [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_004_w2aab3b7b5b1b6b1ab1ab4Aa">4</xref>].Using the Mizar system [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_001_w2aab3b7b5b1b6b1ab1ab1Aa">1</xref>], we define the Gauge integral (Henstock-Kurzweil) of a real-valued function on a real interval [<italic>a, b</italic>] (see [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_002_w2aab3b7b5b1b6b1ab1ab2Aa">2</xref>], [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_003_w2aab3b7b5b1b6b1ab1ab3Aa">3</xref>], [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_015_w2aab3b7b5b1b6b1ab1ac15Aa">15</xref>], [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_014_w2aab3b7b5b1b6b1ab1ac14Aa">14</xref>], [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_011_w2aab3b7b5b1b6b1ab1ac11Aa">11</xref>]). In the next section we formalize that the Henstock-Kurzweil integral is linear.In the last section, we verified that a real-valued bounded integrable (in sense Darboux/Riemann [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_006_w2aab3b7b5b1b6b1ab1ab6Aa">6</xref>, <xref ref-type="bibr" rid="j_forma-2017-0021_ref_007_w2aab3b7b5b1b6b1ab1ab7Aa">7</xref>, <xref ref-type="bibr" rid="j_forma-2017-0021_ref_008_w2aab3b7b5b1b6b1ab1ab8Aa">8</xref>]) function over a interval <italic>a, b</italic> is Gauge integrable.Note that, in accordance with the possibilities of the MML [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_009_w2aab3b7b5b1b6b1ab1ab9Aa">9</xref>], we reuse a large part of demonstrations already present in another article. Instead of rewriting the proof already contained in [<xref ref-type="bibr" rid="j_forma-2017-0021_ref_007_w2aab3b7b5b1b6b1ab1ab7Aa">7</xref>] (MML Version: 5.42.1290), we slightly modified this article in order to use directly the expected results.</abstract>

Some authors have formalized the integral in the Mizar Mathematical Library (MML). The first article in a series on the Darboux/Riemann integral was written by Noboru Endou and Artur Korniłowicz: [6]. The Lebesgue integral was formalized a little later [13] and recently the integral of Riemann-Stieltjes was introduced in the MML by Keiko Narita, Kazuhisa Nakasho and Yasunari Shidama [12].A presentation of definitions of integrals in other proof assistants or proof checkers (ACL2, COQ, Isabelle/HOL, HOL4, HOL Light, PVS, ProofPower) may be found in [10] and [4].Using the Mizar system [1], we define the Gauge integral (Henstock-Kurzweil) of a real-valued function on a real interval [a, b] (see [2], [3], [15], [14], [11]). In the next section we formalize that the Henstock-Kurzweil integral is linear.In the last section, we verified that a real-valued bounded integrable (in sense Darboux/Riemann [6, 7, 8]) function over a interval a, b is Gauge integrable.Note that, in accordance with the possibilities of the MML [9], we reuse a large part of demonstrations already present in another article. Instead of rewriting the proof already contained in [7] (MML Version: 5.42.1290), we slightly modified this article in order to use directly the expected results.

Gauge Integral

Formalized Mathematics

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

{"article-title":"Gauge Integral"}

Some authors have formalized the integral in the Mizar Mathematical Library (MML). The first article in a series on the Darboux/Riemann integral was written by...

Gauge Integral

Pubblicato online: 19 dic 2017

Pagine: 217 - 225

Ricevuto: 03 set 2017

DOI: https://doi.org/10.1515/forma-2017-0021

Parole chiave
Gauge integral, Henstock-Kurzweil integral, generalized Riemann integral

© 2017 Roland Coghetto, published by De Gruyter Open

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

Gauge Integral

Pubblicato online: 19 dic 2017

Pagine: 217 - 225

Ricevuto: 03 set 2017

DOI: https://doi.org/10.1515/forma-2017-0021

Parole chiaveGauge integral, Henstock-Kurzweil integral, generalized Riemann integral

© 2017 Roland Coghetto, published by De Gruyter Open

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

Parole chiave
Gauge integral, Henstock-Kurzweil integral, generalized Riemann integral