- 【Updated on May 12, 2025】 Integration of CiNii Dissertations and CiNii Books into CiNii Research
- Trial version of CiNii Research Knowledge Graph Search feature is available on CiNii Labs
- 【Updated on June 30, 2025】Suspension and deletion of data provided by Nikkei BP
- Regarding the recording of “Research Data” and “Evidence Data”
Description
<jats:title>Abstract</jats:title> <jats:p> 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.</jats:p> <jats:p>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].</jats:p>
Journal
-
- Formalized Mathematics
-
Formalized Mathematics 24 199-204, 2016-09-01
Walter de Gruyter GmbH
- Tweet
Details 詳細情報について
-
- CRID
- 1873961342226322432
-
- ISSN
- 18989934
-
- HANDLE
- 11320/5554
-
- Data Source
-
- OpenAIRE