Riemann-Stieltjes Integral

Keiko Narita, Kazuhisa Nakasho, and Yasunari Shidama. "Riemann-Stieltjes Integral." Formalized Mathematics 24.3 (2016): 199-204. <http://eudml.org/doc/287977>.

@article{KeikoNarita2016,
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].},
author = {Keiko Narita, Kazuhisa Nakasho, Yasunari Shidama},
journal = {Formalized Mathematics},
keywords = {Riemann-Stieltjes integral; bounded variation; linearity},
language = {eng},
number = {3},
pages = {199-204},
title = {Riemann-Stieltjes Integral},
url = {http://eudml.org/doc/287977},
volume = {24},
year = {2016},
}

TY - JOUR
AU - Keiko Narita
AU - Kazuhisa Nakasho
AU - Yasunari Shidama
TI - Riemann-Stieltjes Integral
JO - Formalized Mathematics
PY - 2016
VL - 24
IS - 3
SP - 199
EP - 204
AB - 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].
LA - eng
KW - Riemann-Stieltjes integral; bounded variation; linearity
UR - http://eudml.org/doc/287977
ER -