The Basic Existence Theorem of Riemann-Stieltjes Integral

• Autorzy: Kazuhisa Nakasho , Keiko Narita , Yasunari Shidama
• Języki publikacji: EN

Abstrakty

EN

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

Słowa kluczowe

EN

Riemann-Stieltjes integral; bounded variation; continuous function

Kategorie tematyczne

• 03B35: Mechanization of proofs and logical operations
• 26A45: Functions of bounded variation, generalizations
• 26A42: Integrals of Riemann, Stieltjes and Lebesgue type

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2016
• Tom: 24
• Numer: 4
• Strony: 253-259

Daty

wydano

2016-12-01

otrzymano

2016-10-18

online

2017-02-23

Twórcy

autor

Kazuhisa Nakasho

• Akita Prefectural University, Akita,

autor

Keiko Narita

• Hirosaki-city, Aomori,

autor

Yasunari Shidama

• Shinshu University, Nagano,

Identyfikatory

DOI

10.1515/forma-2016-0021