PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
2017 | 25 | 3 | 217-225
Tytuł artykułu

Gauge Integral

Autorzy
Treść / Zawartość
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
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.
Wydawca
Rocznik
Tom
25
Numer
3
Strony
217-225
Opis fizyczny
Daty
wydano
2017-10-01
otrzymano
2017-09-03
online
2017-12-19
Twórcy
  • Rue de la Brasserie 5, ,
Bibliografia
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.doi-10_1515_forma-2017-0021
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.