{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,11]],"date-time":"2023-02-11T17:12:42Z","timestamp":1676135562024},"reference-count":19,"publisher":"Walter de Gruyter GmbH","issue":"4","license":[{"start":{"date-parts":[[2016,12,1]],"date-time":"2016-12-01T00:00:00Z","timestamp":1480550400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,12,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p>In this article, the basic existence theorem of Riemann-Stieltjes integral is formalized. This theorem states that if <jats:italic>f<\/jats:italic> is a continuous function and <jats:italic>\u03c1<\/jats:italic> is a function of bounded variation in a closed interval of real line, <jats:italic>f<\/jats:italic> is Riemann-Stieltjes integrable with respect to <jats:italic>\u03c1<\/jats:italic>. 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].<\/jats:p>","DOI":"10.1515\/forma-2016-0021","type":"journal-article","created":{"date-parts":[[2017,2,25]],"date-time":"2017-02-25T10:00:53Z","timestamp":1488016853000},"page":"253-259","source":"Crossref","is-referenced-by-count":1,"title":["The Basic Existence Theorem of Riemann-Stieltjes Integral"],"prefix":"10.1515","volume":"24","author":[{"given":"Kazuhisa","family":"Nakasho","sequence":"first","affiliation":[{"name":"Akita Prefectural University, Akita, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Keiko","family":"Narita","sequence":"additional","affiliation":[{"name":"Hirosaki-city, Aomori, 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,23]]},"reference":[{"key":"2021040707354631309_j_forma-2016-0021_ref_001_w2aab2b8b1b1b7b1ab1ab1Aa","unstructured":"[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41\u201346, 1990."},{"key":"2021040707354631309_j_forma-2016-0021_ref_002_w2aab2b8b1b1b7b1ab1ab2Aa","unstructured":"[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107\u2013114, 1990."},{"key":"2021040707354631309_j_forma-2016-0021_ref_003_w2aab2b8b1b1b7b1ab1ab3Aa","unstructured":"[3] Czes\u0142aw Byli\u0144ski. The complex numbers. Formalized Mathematics, 1(3):507\u2013513, 1990."},{"key":"2021040707354631309_j_forma-2016-0021_ref_004_w2aab2b8b1b1b7b1ab1ab4Aa","unstructured":"[4] Czes\u0142aw Byli\u0144ski. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529\u2013536, 1990."},{"key":"2021040707354631309_j_forma-2016-0021_ref_005_w2aab2b8b1b1b7b1ab1ab5Aa","unstructured":"[5] Czes\u0142aw Byli\u0144ski. Functions and their basic properties. Formalized Mathematics, 1(1): 55\u201365, 1990."},{"key":"2021040707354631309_j_forma-2016-0021_ref_006_w2aab2b8b1b1b7b1ab1ab6Aa","unstructured":"[6] Czes\u0142aw Byli\u0144ski. Functions from a set to a set. Formalized Mathematics, 1(1):153\u2013164, 1990."},{"key":"2021040707354631309_j_forma-2016-0021_ref_007_w2aab2b8b1b1b7b1ab1ab7Aa","unstructured":"[7] Czes\u0142aw Byli\u0144ski. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661\u2013668, 1990."},{"key":"2021040707354631309_j_forma-2016-0021_ref_008_w2aab2b8b1b1b7b1ab1ab8Aa","unstructured":"[8] Czes\u0142aw Byli\u0144ski. Some basic properties of sets. Formalized Mathematics, 1(1):47\u201353, 1990."},{"key":"2021040707354631309_j_forma-2016-0021_ref_009_w2aab2b8b1b1b7b1ab1ab9Aa","unstructured":"[9] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Darboux\u2019s theorem. Formalized Mathematics, 9(1):197\u2013200, 2001."},{"key":"2021040707354631309_j_forma-2016-0021_ref_010_w2aab2b8b1b1b7b1ab1ac10Aa","unstructured":"[10] S.L. Gupta and Nisha Rani. Fundamental Real Analysis. Vikas Pub., 1986."},{"key":"2021040707354631309_j_forma-2016-0021_ref_011_w2aab2b8b1b1b7b1ab1ac11Aa","unstructured":"[11] Einar Hille. Methods in classical and functional analysis. Addison-Wesley Publishing Co., Halsted Press, 1974."},{"key":"2021040707354631309_j_forma-2016-0021_ref_012_w2aab2b8b1b1b7b1ab1ac12Aa","unstructured":"[12] H. Kestelman. Modern theories of integration. Dover Publications, 2nd edition, 1960."},{"key":"2021040707354631309_j_forma-2016-0021_ref_013_w2aab2b8b1b1b7b1ab1ac13Aa","doi-asserted-by":"crossref","unstructured":"[13] Keiko Narita, Noboru Endou, and Yasunari Shidama. Riemann integral of functions from \u211d into real Banach space. Formalized Mathematics, 21(2):145\u2013152, 2013. doi:10.2478\/forma-2013-0016.","DOI":"10.2478\/forma-2013-0016"},{"key":"2021040707354631309_j_forma-2016-0021_ref_014_w2aab2b8b1b1b7b1ab1ac14Aa","doi-asserted-by":"crossref","unstructured":"[14] Keiko Narita, Kazuhisa Nakasho, and Yasunari Shidama. Riemann-Stieltjes integral. Formalized Mathematics, 24(3):199\u2013204, 2016. doi:10.1515\/forma-2016-0016.","DOI":"10.1515\/forma-2016-0016"},{"key":"2021040707354631309_j_forma-2016-0021_ref_015_w2aab2b8b1b1b7b1ab1ac15Aa","unstructured":"[15] Daniel W. Stroock. A Concise Introduction to the Theory of Integration. Springer Science & Business Media, 1999."},{"key":"2021040707354631309_j_forma-2016-0021_ref_016_w2aab2b8b1b1b7b1ab1ac16Aa","unstructured":"[16] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329\u2013334, 1990."},{"key":"2021040707354631309_j_forma-2016-0021_ref_017_w2aab2b8b1b1b7b1ab1ac17Aa","unstructured":"[17] Micha\u0142 J. Trybulec. Integers. Formalized Mathematics, 1(3):501\u2013505, 1990."},{"key":"2021040707354631309_j_forma-2016-0021_ref_018_w2aab2b8b1b1b7b1ab1ac18Aa","unstructured":"[18] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569\u2013573, 1990."},{"key":"2021040707354631309_j_forma-2016-0021_ref_019_w2aab2b8b1b1b7b1ab1ac19Aa","unstructured":"[19] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73\u201383, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/24\/4\/article-p253.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0021","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,7]],"date-time":"2021-04-07T22:10:33Z","timestamp":1617833433000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0021"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,1]]},"references-count":19,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2017,2,23]]},"published-print":{"date-parts":[[2016,12,1]]}},"alternative-id":["10.1515\/forma-2016-0021"],"URL":"https:\/\/doi.org\/10.1515\/forma-2016-0021","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2016,12,1]]}}}