{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T19:05:49Z","timestamp":1649012749460},"reference-count":8,"publisher":"Walter de Gruyter GmbH","issue":"3","license":[{"start":{"date-parts":[[2016,9,1]],"date-time":"2016-09-01T00:00:00Z","timestamp":1472688000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/3.0\/legalcode"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,9,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <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>\n               <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>","DOI":"10.1515\/forma-2016-0016","type":"journal-article","created":{"date-parts":[[2017,2,14]],"date-time":"2017-02-14T10:02:03Z","timestamp":1487066523000},"page":"199-204","source":"Crossref","is-referenced-by-count":3,"title":["Riemann-Stieltjes Integral"],"prefix":"10.1515","volume":"24","author":[{"given":"Keiko","family":"Narita","sequence":"first","affiliation":[{"name":"Hirosaki-city Aomori, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kazuhisa","family":"Nakasho","sequence":"additional","affiliation":[{"name":"Akita Prefectural University Akita, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yasunari","family":"Shidama","sequence":"additional","affiliation":[{"name":"Shinshu University Nagano, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2017,2,21]]},"reference":[{"key":"2021040805180296918_j_forma-2016-0016_ref_1_w2aab2b8b8b1b7b1ab1ab1Aa","doi-asserted-by":"crossref","unstructured":"[1] Grzegorz Bancerek, Czes\u0142aw Bylinski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261-279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007\/978-3-319-20615-8_17.","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2021040805180296918_j_forma-2016-0016_ref_2_w2aab2b8b8b1b7b1ab1ab2Aa","unstructured":"[2] Czes\u0142aw Bylinski. The complex numbers. Formalized Mathematics, 1(3):507-513, 1990."},{"key":"2021040805180296918_j_forma-2016-0016_ref_3_w2aab2b8b8b1b7b1ab1ab3Aa","unstructured":"[3] S.L. Gupta and Nisha Rani. Fundamental Real Analysis. Vikas Pub., 1986."},{"key":"2021040805180296918_j_forma-2016-0016_ref_4_w2aab2b8b8b1b7b1ab1ab4Aa","unstructured":"[4] Einar Hille. Methods in classical and functional analysis. Addison-Wesley Publishing Co., Halsted Press, 1974."},{"key":"2021040805180296918_j_forma-2016-0016_ref_5_w2aab2b8b8b1b7b1ab1ab5Aa","unstructured":"[5] H. Kestelman. Modern theories of integration. Dover Publications, 2nd edition, 1960."},{"key":"2021040805180296918_j_forma-2016-0016_ref_6_w2aab2b8b8b1b7b1ab1ab6Aa","unstructured":"[6] Jaros\u0142aw Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477-481, 1990."},{"key":"2021040805180296918_j_forma-2016-0016_ref_7_w2aab2b8b8b1b7b1ab1ab7Aa","doi-asserted-by":"crossref","unstructured":"[7] Keiichi Miyajima, Takahiro Kato, and Yasunari Shidama. Riemann integral of functions from \u211d into real normed space. Formalized Mathematics, 19(1):17-22, 2011. doi:10.2478\/v10037-011-0003-8.","DOI":"10.2478\/v10037-011-0003-8"},{"key":"2021040805180296918_j_forma-2016-0016_ref_8_w2aab2b8b8b1b7b1ab1ab8Aa","unstructured":"[8] Daniel W. Stroock. A Concise Introduction to the Theory of Integration. Springer Science & Business Media, 1999."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/24\/3\/article-p199.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0016","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,8]],"date-time":"2021-04-08T17:08:01Z","timestamp":1617901681000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0016"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,1]]},"references-count":8,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2017,2,21]]},"published-print":{"date-parts":[[2016,9,1]]}},"alternative-id":["10.1515\/forma-2016-0016"],"URL":"https:\/\/doi.org\/10.1515\/forma-2016-0016","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9,1]]}}}