{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T01:13:19Z","timestamp":1648602799720},"reference-count":7,"publisher":"Walter de Gruyter GmbH","issue":"4","license":[{"start":{"date-parts":[[2017,12,20]],"date-time":"2017-12-20T00:00:00Z","timestamp":1513728000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,12,20]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p> We start proceeding with the stopping time theory in discrete time with the help of the Mizar system [1], [4]. We prove, that the expression for two stopping times k1 and k2 not always implies a stopping time (k<jats:sub>1<\/jats:sub> + k<jats:sub>2<\/jats:sub>) (see Theorem 6 in this paper). If you want to get a stopping time, you have to cut the function e.g. (k<jats:sub>1<\/jats:sub> + k<jats:sub>2<\/jats:sub>) \u22c2 T (see [2, p. 283 Remark 6.14]). Next we introduce the stopping time in continuous time. We are focused on the intervals [0, r] where r \u2208 \u211d. We prove, that for I = [0, r] or I = [0,+\u221e[ the set {A \u22c2 I : A \u2208 Borel-Sets} is a \u03c3-algebra of I (see Definition 6 in this paper, and more general given in [3, p.12 1.8e]). The interval I can be considered as a timeline from now to some point in the future. This set is necessary to define our next lemma. We prove the existence of the \u03c3-algebra of the \u03c4 -past, where \u03c4 is a stopping time (see Definition 11 in this paper and [6, p.187, Definition 9.19]). If \u03c4<jats:sub>1<\/jats:sub> and \u03c4<jats:sub>2<\/jats:sub> are stopping times with \u03c4<jats:sub>1<\/jats:sub> is smaller or equal than \u03c4<jats:sub>2<\/jats:sub> we can prove, that the \u03c3-algebra of the \u03c4<jats:sub>1<\/jats:sub>-past is a subset of the \u03c3-algebra of the \u03c4<jats:sub>2<\/jats:sub>-past (see Theorem 9 in this paper and [6, p.187 Lemma 9.21]). Suppose, that you want to use Lemma 9.21 with some events, that never occur, see as a comparison the paper [5] and the example for ST(1)={+\u221e} in the Summary. We don\u2019t have the element +1 in our above-mentioned time intervals [0, r[ and [0,+1[. This is only possible if we construct a new \u03c3-algebra on \u211d {\u2212\u221e,+\u221e}. This construction is similar to the Borel-Sets and we call this \u03c3-algebra extended Borel sets (see Definition 13 in this paper and [3, p. 21]). It can be proved, that {+\u221e} is an Element of extended Borel sets (see Theorem 21 in this paper). Now we use the interval [0,+\u221e] as a basis. We construct a \u03c3-algebra on [0,+\u221e] similar to the book ([3, p. 12 18e]), see Definition 18 in this paper, and call it extended Borel subsets. We prove for stopping times with this given \u03c3-algebra, that for \u03c4<jats:sub>1<\/jats:sub> and \u03c4<jats:sub>2<\/jats:sub> are stopping times with \u03c4<jats:sub>1<\/jats:sub> is smaller or equal than \u03c4<jats:sub>2<\/jats:sub> we have the \u03c3-algebra of the \u03c4<jats:sub>1<\/jats:sub>-past is a subset of the \u03c3-algebra of the \u03c4<jats:sub>2<\/jats:sub>-past, see Theorem 25 in this paper. It is obvious, that {+\u221e} 2 extended Borel subsets. In general, Lemma 9.21 is important for the proof of the Optional Sampling Theorem, see 10.11 Proof of (i) in [6, p. 203].<\/jats:p>","DOI":"10.1515\/forma-2017-0025","type":"journal-article","created":{"date-parts":[[2018,3,28]],"date-time":"2018-03-28T22:16:22Z","timestamp":1522275382000},"page":"261-268","source":"Crossref","is-referenced-by-count":0,"title":["Introduction to Stopping Time in Stochastic Finance Theory. Part II"],"prefix":"10.1515","volume":"25","author":[{"given":"Peter","family":"Jaeger","sequence":"first","affiliation":[{"name":"Siegmund-Schacky-Str. 18a 80993 Munich , Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2018,3,28]]},"reference":[{"key":"2021040611522109582_j_forma-2017-0025_ref_001_w2aab3b7b1b1b6b1ab1ab1Aa","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.10.1007\/978-3-319-20615-817","DOI":"10.1007\/978-3-319-20615-8"},{"key":"2021040611522109582_j_forma-2017-0025_ref_002_w2aab3b7b1b1b6b1ab1ab2Aa","doi-asserted-by":"crossref","unstructured":"[2] Hans F\u00f6llmer and Alexander Schied. Stochastic Finance: An Introduction in Discrete Time, volume 27 of Studies in Mathematics. de Gruyter, Berlin, 2nd edition, 2004.","DOI":"10.1515\/9783110212075"},{"key":"2021040611522109582_j_forma-2017-0025_ref_003_w2aab3b7b1b1b6b1ab1ab3Aa","unstructured":"[3] Hans-Otto Georgii. Stochastik, Einf\u00fchrung in die Wahrscheinlichkeitstheorie und Statistik. deGruyter, Berlin, 2nd edition, 2004."},{"key":"2021040611522109582_j_forma-2017-0025_ref_004_w2aab3b7b1b1b6b1ab1ab4Aa","unstructured":"[4] Adam Grabowski, Artur Korni\u0142owicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191-198, 2015. doi: 10.1007\/s10817-015-9345-1.10.1007\/s10817-015-9345-1"},{"key":"2021040611522109582_j_forma-2017-0025_ref_005_w2aab3b7b1b1b6b1ab1ab5Aa","unstructured":"[5] Peter Jaeger. Introduction to stopping time in stochastic finance theory. Formalized Mathematics, 25(2):101-105, 2017. doi: 10.1515\/forma-2017-0010.10.1515\/forma-2017-0010"},{"key":"2021040611522109582_j_forma-2017-0025_ref_006_w2aab3b7b1b1b6b1ab1ab6Aa","unstructured":"[6] Achim Klenke. Wahrscheinlichkeitstheorie. Springer-Verlag, Berlin, Heidelberg, 2006."},{"key":"2021040611522109582_j_forma-2017-0025_ref_007_w2aab3b7b1b1b6b1ab1ab7Aa","unstructured":"[7] Andrzej Nedzusiak. -fields and probability. Formalized Mathematics, 1(2):401-407, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/25\/4\/article-p261.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2017-0025","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,6]],"date-time":"2021-04-06T18:46:20Z","timestamp":1617734780000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2017-0025"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,20]]},"references-count":7,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2018,3,28]]},"published-print":{"date-parts":[[2017,12,20]]}},"alternative-id":["10.1515\/forma-2017-0025"],"URL":"https:\/\/doi.org\/10.1515\/forma-2017-0025","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2017,12,20]]}}}