<abstract xmlns="http://www.w3.org/1999/xhtml"><p> In this article, the definitions and basic properties of Riemann-Stieltjes integral are formalized in Mizar [1]. In the first section, we showed the preliminary definition. We proved also some properties of finite sequences of real numbers. In Sec. 2, we defined variation. Using the definition, we also defined bounded variation and total variation, and proved theorems about related properties.</p><p>In Sec. 3, we defined Riemann-Stieltjes integral. Referring to the way of the article [7], we described the definitions. In the last section, we proved theorems about linearity of Riemann-Stieltjes integral. Because there are two types of linearity in Riemann-Stieltjes integral, we proved linearity in two ways. We showed the proof of theorems based on the description of the article [7]. These formalizations are based on [8], [5], [3], and [4].</p></abstract>

In this article, the definitions and basic properties of Riemann-Stieltjes integral are formalized in Mizar [1]. In the first section, we showed the preliminary definition. We proved also some properties of finite sequences of real numbers. In Sec. 2, we defined variation. Using the definition, we also defined bounded variation and total variation, and proved theorems about related properties.In Sec. 3, we defined Riemann-Stieltjes integral. Referring to the way of the article [7], we described the definitions. In the last section, we proved theorems about linearity of Riemann-Stieltjes integral. Because there are two types of linearity in Riemann-Stieltjes integral, we proved linearity in two ways. We showed the proof of theorems based on the description of the article [7]. These formalizations are based on [8], [5], [3], and [4].

Riemann-Stieltjes Integral

Formalized Mathematics

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License

{"article-title":"Riemann-Stieltjes Integral"}

In this article, the definitions and basic properties of Riemann-Stieltjes integral are formalized in Mizar [1]. In the first section, we showed the...

Riemann-Stieltjes Integral

Data publikacji: 21 lut 2017

Zakres stron: 199 - 204

Otrzymano: 30 cze 2016

DOI: https://doi.org/10.1515/forma-2016-0016

Słowa kluczowe
Riemann-Stieltjes integral, bounded variation, linearity

© by Keiko Narita

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License

Riemann-Stieltjes Integral

Data publikacji: 21 lut 2017

Zakres stron: 199 - 204

Otrzymano: 30 cze 2016

DOI: https://doi.org/10.1515/forma-2016-0016

Słowa kluczoweRiemann-Stieltjes integral, bounded variation, linearity

© by Keiko Narita

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License

Słowa kluczowe
Riemann-Stieltjes integral, bounded variation, linearity