@MISC{INTEGR22.MIZ,
  AUTHOR = {Nakasho, Kazuhisa and Narita, Keiko and Shidama, Yasunari},
  TITLE = {The Basic Existence Theorem of Riemann-Stieltjes Integral},
  SECTION1 = {Preliminaries},
  SECTION2 = {Existence of Riemann-Stieltjes Integral for Continuous Functions},
  DAY = {18},
  MONTH = {October},
  YEAR = {2016},
  ADDRESS1 = {Akita Prefectural University\\Akita, Japan},
  ADDRESS2 = {Hirosaki-city, Aomori, Japan},
  ADDRESS3 = {Shinshu University\\Nagano, Japan},
  MSC2010 = {26A42 26A45},
  KEYWORDS = {Riemann-Stieltjes integral; bounded variation; continuous function},
  SUMMARY = {In this article, The basic existence theorem of Riemann-Stieltjes Integral is formalized.
  This theorem describes if $f$ is a continuous function and $\rho$ is a function of bounded variation
  in a closed interval of real line, $f$ is Riemann-Stieltjes Integrable with respect to $\rho$.
  In the first section, basic properties of real finite sequences are formalized as preliminaries.
  In the second section, we formalized the existence theorem of Riemann-Stieltjes integral.
  These formalizations are based on \cite{Stroock1999}, \cite{Kestelman1960}, \cite{Gupta1986}, and \cite{Hille1974}.}}

@BOOK{Stroock1999,
  TITLE = {A Concise Introduction to the Theory of Integration}
  AUTHOR = {Daniel W. Stroock},
  PUBLISHER = {Springer Science \& Business Media}
  YEAR  = {1999},
}
@BOOK{Kestelman1960,
  TITLE={Modern theories of integration},
  AUTHOR={H Kestelman},
  PUBLISHER={Dover Publications},
  YEAR={1960},
  EDITION={2nd}
}
@BOOK{Gupta1986,
  TITLE = {Fundamental Real Analysis},
  AUTHOR = {S. L. Gupta and Nisha Rani},
  PUBLISHER = {Vikas Pub},
  YEAR = {1986}
}
@BOOK{Hille1974,
  TITLE={Methods in classical and functional analysis},
  AUTHOR={Hille, Einar},
  PUBLISHER={Addison-Wesley Publishing Co., Halsted Press}
  YEAR={1974},
}
