<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

Published Online: Feb 23, 2017

Page range: 253 - 259

Received: Oct 18, 2016

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

Keywords
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

Published Online: Feb 23, 2017

Page range: 253 - 259

Received: Oct 18, 2016

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

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

Keywords
Riemann-Stieltjes integral, bounded variation, continuous function