{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T01:02:07Z","timestamp":1777424527543,"version":"3.51.4"},"reference-count":0,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2016,3,1]],"date-time":"2016-03-01T00:00:00Z","timestamp":1456790400000},"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,3,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p> First we give an implementation in Mizar [2] basic important definitions of stochastic finance, i.e. filtration ([9], pp. 183 and 185), adapted stochastic process ([9], p. 185) and predictable stochastic process ([6], p. 224). Second we give some concrete formalization and verification to real world examples. <\/jats:p>\n               <jats:p>In article [8] we started to define random variables for a similar presentation to the book [6]. Here we continue this study. Next we define the stochastic process. For further definitions based on stochastic process we implement the definition of filtration. <\/jats:p>\n               <jats:p>To get a better understanding we give a real world example and connect the statements to the theorems. Other similar examples are given in [10], pp. 143-159 and in [12], pp. 110-124. First we introduce sets which give informations referring to today (\u03a9<jats:sub>now<\/jats:sub>, Def.6), tomorrow (\u03a9<jats:sub>fut1<\/jats:sub> , Def.7) and the day after tomorrow (\u03a9<jats:sub>fut2<\/jats:sub> , Def.8). We give an overview for some events in the \u03c3-algebras \u03a9<jats:sub>now<\/jats:sub>, \u03a9<jats:sub>fut1<\/jats:sub> and \u03a9<jats:sub>fut2<\/jats:sub>, see theorems (22) and (23). <\/jats:p>\n               <jats:p>The given events are necessary for creating our next functions. The implementations take the form of: \u03a9<jats:sub>now<\/jats:sub> \u2282 \u03a9<jats:sub>fut1<\/jats:sub> \u2282 \u03a9<jats:sub>fut2<\/jats:sub> see theorem (24). This tells us growing informations from now to the future 1=now, 2=tomorrow, 3=the day after tomorrow. <\/jats:p>\n               <jats:p>We install functions f : {1, 2, 3, 4} \u2192 \u211d as following: <\/jats:p>\n               <jats:p>f<jats:sub>1<\/jats:sub> : x \u2192 100, \u2200x \u2208 dom f, see theorem (36), <\/jats:p>\n               <jats:p>f<jats:sub>2<\/jats:sub> : x \u2192 80, for x = 1 or x = 2 and <\/jats:p>\n               <jats:p>f<jats:sub>2<\/jats:sub> : x \u2192 120, for x = 3 or x = 4, see theorem (37), <\/jats:p>\n               <jats:p>f<jats:sub>3<\/jats:sub> : x \u2192 60, for x = 1, f<jats:sub>3<\/jats:sub> : x \u2192 80, for x = 2 and <\/jats:p>\n               <jats:p>f<jats:sub>3<\/jats:sub> : x \u2192 100, for x = 3, f<jats:sub>3<\/jats:sub> : x \u2192 120, for x = 4 see theorem (38). <\/jats:p>\n               <jats:p>These functions are real random variable: f<jats:sub>1<\/jats:sub> over \u03a9<jats:sub>now<\/jats:sub>, f<jats:sub>2<\/jats:sub> over \u03a9<jats:sub>fut1<\/jats:sub>, f<jats:sub>3<\/jats:sub> over \u03a9<jats:sub>fut2<\/jats:sub>, see theorems (46), (43) and (40). We can prove that these functions can be used for giving an example for an adapted stochastic process. See theorem (49). <\/jats:p>\n               <jats:p>We want to give an interpretation to these functions: suppose you have an equity A which has now (= w<jats:sub>1<\/jats:sub>) the value 100. Tomorrow A changes depending which scenario occurs \u2212 e.g. another marketing strategy. In scenario 1 (= w<jats:sub>11<\/jats:sub>) it has the value 80, in scenario 2 (= w<jats:sub>12<\/jats:sub>) it has the value 120. The day after tomorrow A changes again. In scenario 1 (= w<jats:sub>111<\/jats:sub>) it has the value 60, in scenario 2 (= w<jats:sub>112<\/jats:sub>) the value 80, in scenario 3 (= w<jats:sub>121<\/jats:sub>) the value 100 and in scenario 4 (= w<jats:sub>122<\/jats:sub>) it has the value 120. For a visualization refer to the tree: <\/jats:p>\n               <jats:p>\n                  <jats:inline-formula>\n                     <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/Untitled-1.jpg\"\/>\n                     <\/jats:alternatives>\n                  <\/jats:inline-formula>\n               <\/jats:p>\n               <jats:p>The sets w<jats:sub>1<\/jats:sub>,w<jats:sub>11<\/jats:sub>,w<jats:sub>12<\/jats:sub>,w<jats:sub>111<\/jats:sub>,w<jats:sub>112<\/jats:sub>,w<jats:sub>121<\/jats:sub>,w<jats:sub>122<\/jats:sub> which are subsets of {1, 2, 3, 4}, see (22), tell us which market scenario occurs. The functions tell us the values to the relevant market scenario: <\/jats:p>\n               <jats:p>\n                  <jats:inline-formula>\n                     <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/Untitled-2.jpg\"\/>\n                     <\/jats:alternatives>\n                  <\/jats:inline-formula>\n               <\/jats:p>\n               <jats:p>For a better understanding of the definition of the random variable and the relation to the functions refer to [7], p. 20. For the proof of certain sets as \u03c3-fields refer to [7], pp. 10-11 and [9], pp. 1-2. <\/jats:p>\n               <jats:p>This article is the next step to the arbitrage opportunity. If you use for example a simple probability measure, refer, for example to literature [3], pp. 28-34, [6], p. 6 and p. 232 you can calculate whether an arbitrage exists or not. Note, that the example given in literature [3] needs 8 instead of 4 informations as in our model. If we want to code the first 3 given time points into our model we would have the following graph, see theorems (47), (44) and (41): <\/jats:p>\n               <jats:p>\n                  <jats:inline-formula>\n                     <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/Untitled-3.jpg\"\/>\n                     <\/jats:alternatives>\n                  <\/jats:inline-formula>\n               <\/jats:p>\n               <jats:p>The function for the \u201cCall-Option\u201d is given in literature [3], p. 28. The function is realized in Def.5. As a background, more examples for using the definition of filtration are given in [9], pp. 185-188. <\/jats:p>","DOI":"10.1515\/forma-2016-0001","type":"journal-article","created":{"date-parts":[[2016,8,22]],"date-time":"2016-08-22T14:36:23Z","timestamp":1471876583000},"page":"1-16","source":"Crossref","is-referenced-by-count":1,"title":["Modelling Real World Using Stochastic Processes and Filtration"],"prefix":"10.1515","volume":"24","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":[[2016,8,31]]},"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/24\/1\/article-p1.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0001","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,8]],"date-time":"2021-04-08T02:12:37Z","timestamp":1617847957000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0001"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3,1]]},"references-count":0,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2016,8,31]]},"published-print":{"date-parts":[[2016,3,1]]}},"alternative-id":["10.1515\/forma-2016-0001"],"URL":"https:\/\/doi.org\/10.1515\/forma-2016-0001","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3,1]]}}}