<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this article, the basic existence theorem of Riemann-Stieltjes integral is formalized. This theorem states that if <italic>f</italic> is a continuous function and <italic>ρ</italic> is a function of bounded variation in a closed interval of real line, <italic>f</italic> is Riemann-Stieltjes integrable with respect to <italic>ρ</italic>. In the first section, basic properties of real finite sequences are formalized as preliminaries. In the second section, we formalized the existence theorem of the Riemann-Stieltjes integral. These formalizations are based on [<xref ref-type="bibr" rid="j_forma-2016-0021_ref_015_w2aab2b8b1b1b7b1ab1ac15Aa">15</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0021_ref_012_w2aab2b8b1b1b7b1ab1ac12Aa">12</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0021_ref_010_w2aab2b8b1b1b7b1ab1ac10Aa">10</xref>], and [<xref ref-type="bibr" rid="j_forma-2016-0021_ref_011_w2aab2b8b1b1b7b1ab1ac11Aa">11</xref>].</p></abstract>

In this article, the basic existence theorem of Riemann-Stieltjes integral is formalized. This theorem states that if f is a continuous function and ρ is a function of bounded variation in a closed interval of real line, f is Riemann-Stieltjes integrable with respect to ρ. In the first section, basic properties of real finite sequences are formalized as preliminaries. In the second section, we formalized the existence theorem of the Riemann-Stieltjes integral. These formalizations are based on [15], [12], [10], and [11].

The Basic Existence Theorem of Riemann-Stieltjes Integral

Formalized Mathematics

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

{"article-title":"The Basic Existence Theorem of Riemann-Stieltjes Integral"}

In this article, the basic existence theorem of Riemann-Stieltjes integral is formalized. This theorem states that if f is a continuous function and ρ is a...

The Basic Existence Theorem of Riemann-Stieltjes Integral

Online veröffentlicht: 23. Feb. 2017

Seitenbereich: 253 - 259

Eingereicht: 18. Okt. 2016

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

Schlüsselwörter
Riemann-Stieltjes integral, bounded variation, continuous function

© 2016 Kazuhisa Nakasho et al., published by De Gruyter Open

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

The Basic Existence Theorem of Riemann-Stieltjes Integral

Online veröffentlicht: 23. Feb. 2017

Seitenbereich: 253 - 259

Eingereicht: 18. Okt. 2016

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

SchlüsselwörterRiemann-Stieltjes integral, bounded variation, continuous function

© 2016 Kazuhisa Nakasho et al., published by De Gruyter Open

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

Schlüsselwörter
Riemann-Stieltjes integral, bounded variation, continuous function