# Gauge Integral

Formalized Mathematics (2017)

- Volume: 25, Issue: 3, page 217-225
- ISSN: 1426-2630

## Access Full Article

top## Abstract

top## How to cite

topRoland Coghetto. "Gauge Integral." Formalized Mathematics 25.3 (2017): 217-225. <http://eudml.org/doc/288312>.

@article{RolandCoghetto2017,

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

author = {Roland Coghetto},

journal = {Formalized Mathematics},

keywords = {Gauge integral; Henstock-Kurzweil integral; generalized Riemann integral},

language = {eng},

number = {3},

pages = {217-225},

title = {Gauge Integral},

url = {http://eudml.org/doc/288312},

volume = {25},

year = {2017},

}

TY - JOUR

AU - Roland Coghetto

TI - Gauge Integral

JO - Formalized Mathematics

PY - 2017

VL - 25

IS - 3

SP - 217

EP - 225

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

LA - eng

KW - Gauge integral; Henstock-Kurzweil integral; generalized Riemann integral

UR - http://eudml.org/doc/288312

ER -

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.