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 preliminary definition. We proved also some properties of finite sequences of real numbers. In Sec. 2, we defined variation. Using the definition, we a...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Sciendo
2016-09-01
|
| Series: | Formalized Mathematics |
| Subjects: | |
| Online Access: | https://doi.org/10.1515/forma-2016-0016 |
| id |
doaj-5cca4dfdbe834856b6b4cdde1a3ac72d |
|---|---|
| record_format |
Article |
| spelling |
doaj-5cca4dfdbe834856b6b4cdde1a3ac72d2021-09-05T20:45:03ZengSciendoFormalized Mathematics1898-99342016-09-0124319920410.1515/forma-2016-0016forma-2016-0016Riemann-Stieltjes IntegralNarita Keiko0Nakasho Kazuhisa1Shidama Yasunari2Hirosaki-city Aomori, JapanAkita Prefectural University Akita, JapanShinshu University Nagano, JapanIn 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.https://doi.org/10.1515/forma-2016-001626a4226a4503b35riemann-stieltjes integralbounded variationlinearityidentifier: integr22version: 8.1.05 5.37.1275 |
| collection |
DOAJ |
| language |
English |
| format |
Article |
| sources |
DOAJ |
| author |
Narita Keiko Nakasho Kazuhisa Shidama Yasunari |
| spellingShingle |
Narita Keiko Nakasho Kazuhisa Shidama Yasunari Riemann-Stieltjes Integral Formalized Mathematics 26a42 26a45 03b35 riemann-stieltjes integral bounded variation linearity identifier: integr22 version: 8.1.05 5.37.1275 |
| author_facet |
Narita Keiko Nakasho Kazuhisa Shidama Yasunari |
| author_sort |
Narita Keiko |
| title |
Riemann-Stieltjes Integral |
| title_short |
Riemann-Stieltjes Integral |
| title_full |
Riemann-Stieltjes Integral |
| title_fullStr |
Riemann-Stieltjes Integral |
| title_full_unstemmed |
Riemann-Stieltjes Integral |
| title_sort |
riemann-stieltjes integral |
| publisher |
Sciendo |
| series |
Formalized Mathematics |
| issn |
1898-9934 |
| publishDate |
2016-09-01 |
| description |
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. |
| topic |
26a42 26a45 03b35 riemann-stieltjes integral bounded variation linearity identifier: integr22 version: 8.1.05 5.37.1275 |
| url |
https://doi.org/10.1515/forma-2016-0016 |
| work_keys_str_mv |
AT naritakeiko riemannstieltjesintegral AT nakashokazuhisa riemannstieltjesintegral AT shidamayasunari riemannstieltjesintegral |
| _version_ |
1717784630208233472 |