<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

Data publikacji: 23 lut 2017

Zakres stron: 253 - 259

Otrzymano: 18 paź 2016

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

Słowa kluczowe
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

Data publikacji: 23 lut 2017

Zakres stron: 253 - 259

Otrzymano: 18 paź 2016

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

Słowa kluczoweRiemann-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.

Słowa kluczowe
Riemann-Stieltjes integral, bounded variation, continuous function