<abstract xmlns="http://www.w3.org/1999/xhtml">Using the Mizar system [<xref ref-type="bibr" rid="j_forma-2018-0001_ref_001_w2aab3b7ab1b6b1ab1ab1Aa">1</xref>], [<xref ref-type="bibr" rid="j_forma-2018-0001_ref_005_w2aab3b7ab1b6b1ab1ab5Aa">5</xref>], we start to show, that the Call-Option, the Put-Option and the Straddle (more generally defined as in the literature) are random variables ([<xref ref-type="bibr" rid="j_forma-2018-0001_ref_004_w2aab3b7ab1b6b1ab1ab4Aa">4</xref>], p. 15), see (Def. 1) and (Def. 2). Next we construct and prove the simple random variables ([<xref ref-type="bibr" rid="j_forma-2018-0001_ref_002_w2aab3b7ab1b6b1ab1ab2Aa">2</xref>], p. 14) in (Def. 8).In the third section, we introduce the definition of arbitrage opportunity, see (Def. 12). Next we show, that this definition can be characterized in a different way (Lemma 1.3. in [<xref ref-type="bibr" rid="j_forma-2018-0001_ref_004_w2aab3b7ab1b6b1ab1ab4Aa">4</xref>], p. 5), see (17). In our formalization for Lemma 1.3 we make the assumption that <italic>ϕ</italic> is a sequence of real numbers (there are only finitely many valued of interest, the values of <italic>ϕ</italic> in <italic>Rd</italic>). For the definition of almost sure with probability 1 see p. 6 in [<xref ref-type="bibr" rid="j_forma-2018-0001_ref_002_w2aab3b7ab1b6b1ab1ab2Aa">2</xref>]. Last we introduce the risk-neutral probability (Definition 1.4, p. 6 in [<xref ref-type="bibr" rid="j_forma-2018-0001_ref_004_w2aab3b7ab1b6b1ab1ab4Aa">4</xref>]), here see (Def. 16).We give an example in real world: Suppose you have some assets like bonds (riskless assets). Then we can fix our price for these bonds with <italic>x</italic> for today and <italic>x</italic> · (1 + <italic>r</italic>) for tomorrow, <italic>r</italic> is the interest rate. So we simply assume, that in every possible market evolution of tomorrow we have a determinated value. Then every probability measure of Ω<italic>fut</italic>1 is a risk-neutral measure, see (21). This example shows the existence of some risk-neutral measure. If you find more than one of them, you can determine – with an additional conidition to the probability measures – whether a market model is arbitrage free or not (see Theorem 1.6. in [<xref ref-type="bibr" rid="j_forma-2018-0001_ref_004_w2aab3b7ab1b6b1ab1ab4Aa">4</xref>], p. 6.)A short graph for (21):Suppose we have a portfolio with many (in this example infinitely many) assets. For asset <italic>d</italic> we have the price <italic>π</italic>(<italic>d</italic>) for today, and the price <italic>π</italic>(<italic>d</italic>) (1 + <italic>r</italic>) for tomorrow with some interest rate <italic>r ></italic> 0.Let G be a sequence of random variables on Ω<italic>fut</italic>1, Borel sets. So you have many functions <italic>fk</italic> : {1, 2, 3, 4}→ <italic>R</italic> with <italic>G</italic>(<italic>k</italic>) = <italic>fk</italic> and <italic>fk</italic> is a random variable of Ω<italic>fut</italic>1, Borel sets. For every <italic>fk</italic> we have <italic>fk</italic>(<italic>w</italic>) = <italic>π</italic>(<italic>k</italic>)·(1+<italic>r</italic>) for <italic>w</italic> {1, 2, 3, 4}.<disp-formula><alternatives><graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2018-0001_eq_001.png"></graphic><math xmlns:mml="http://www.w3.org/1998/Math/MathML"><mrow><mtable><mtr><mtd><mrow><mi>Today</mi></mrow></mtd><mtd><mrow><mi>Tomorrow</mi></mrow></mtd></mtr><mtr><mtd><mrow><mtext>only</mtext><mi> </mi><mtext>one</mtext><mi> </mi><mtext>scenario</mtext></mrow></mtd><mtd><mrow><mrow><mo>{</mo><mrow><mtable><mtr><mtd><mrow><msub><mi>w</mi><mrow><mn>21</mn></mrow></msub><mo>=</mo><mrow><mo>{</mo><mrow><mn>1</mn><mo>,</mo><mn>2</mn></mrow><mo>}</mo></mrow></mrow></mtd></mtr><mtr><mtd><mrow><msub><mi>w</mi><mrow><mn>22</mn></mrow></msub><mo>=</mo><mrow><mo>{</mo><mrow><mn>3</mn><mo>,</mo><mn>4</mn></mrow><mo>}</mo></mrow></mrow></mtd></mtr></mtable></mrow></mrow></mrow></mtd></mtr><mtr><mtd><mrow><mtext>for</mtext><mi> </mi><mtext>all</mtext><mi> </mi><mi>d</mi><mo>∈</mo><mi>𝕅</mi><mi> </mi><mtext>holds</mtext><mi> </mi><mi>π</mi><mrow><mo>(</mo><mi>d</mi><mo>)</mo></mrow></mrow></mtd><mtd><mrow><mrow><mo>{</mo><mrow><mtable><mtr><mtd><mrow><msub><mi>f</mi><mi>d</mi></msub><mrow><mo>(</mo><mi>w</mi><mo>)</mo></mrow><mo>=</mo><mi>G</mi><mrow><mo>(</mo><mi>d</mi><mo>)</mo></mrow><mrow><mo>(</mo><mi>w</mi><mo>)</mo></mrow><mo>=</mo><mi>π</mi><mrow><mo>(</mo><mi>d</mi><mo>)</mo></mrow><mo>⋅</mo><mrow><mo>(</mo><mrow><mn>1</mn><mo>+</mo><mi>r</mi></mrow><mo>)</mo></mrow><mo>,</mo></mrow></mtd></mtr><mtr><mtd><mrow><mi>w</mi><mo>∈</mo><msub><mi>w</mi><mrow><mn>21</mn></mrow></msub><mi> </mi><mi>or</mi><mi> </mi><mi>w</mi><mo>∈</mo><msub><mi>w</mi><mrow><mn>22</mn></mrow></msub><mo>,</mo></mrow></mtd></mtr><mtr><mtd><mrow><mi>r</mi><mo>></mo><mn>0</mn><mi> </mi><mtext>is</mtext><mi> </mi><mtext>the</mtext><mi> </mi><mtext>interest</mtext><mi> </mi><mtext>rate</mtext><mo>.</mo></mrow></mtd></mtr></mtable></mrow></mrow></mrow></mtd></mtr></mtable></mrow></math><tex-math>$$\matrix{ {Today} &amp; {Tomorrow} \cr {{\rm{only}}\,{\rm{one}}\,{\rm{scenario}}} &amp; {\left\{ {\matrix{ {w_{21} = \left\{ {1,2} \right\}} \hfill \cr {w_{22} = \left\{ {3,4} \right\}} \hfill \cr } } \right.} \cr {{\rm{for}}\,{\rm{all}}\,d \in N\,{\rm{holds}}\,\pi \left( d \right)} &amp; {\left\{ {\matrix{ {f_d \left( w \right) = G\left( d \right)\left( w \right) = \pi \left( d \right) \cdot \left( {1 + r} \right),} \hfill \cr {w \in w_{21} \,or\,w \in w_{22} ,} \hfill \cr {r > 0\,{\rm{is}}\,{\rm{the}}\,{\rm{interest}}\,{\rm{rate}}.} \hfill \cr } } \right.} \cr }$$</tex-math></alternatives></disp-formula>Here, every probability measure of Ω<italic>fut</italic>1 is a risk-neutral measure.</abstract>

Using the Mizar system [1], [5], we start to show, that the Call-Option, the Put-Option and the Straddle (more generally defined as in the literature) are random variables ([4], p. 15), see (Def. 1) and (Def. 2). Next we construct and prove the simple random variables ([2], p. 14) in (Def. 8).In the third section, we introduce the definition of arbitrage opportunity, see (Def. 12). Next we show, that this definition can be characterized in a different way (Lemma 1.3. in [4], p. 5), see (17). In our formalization for Lemma 1.3 we make the assumption that ϕ is a sequence of real numbers (there are only finitely many valued of interest, the values of ϕ in Rd). For the definition of almost sure with probability 1 see p. 6 in [2]. Last we introduce the risk-neutral probability (Definition 1.4, p. 6 in [4]), here see (Def. 16).We give an example in real world: Suppose you have some assets like bonds (riskless assets). Then we can fix our price for these bonds with x for today and x · (1 + r) for tomorrow, r is the interest rate. So we simply assume, that in every possible market evolution of tomorrow we have a determinated value. Then every probability measure of Ωfut1 is a risk-neutral measure, see (21). This example shows the existence of some risk-neutral measure. If you find more than one of them, you can determine – with an additional conidition to the probability measures – whether a market model is arbitrage free or not (see Theorem 1.6. in [4], p. 6.)A short graph for (21):Suppose we have a portfolio with many (in this example infinitely many) assets. For asset d we have the price π(d) for today, and the price π(d) (1 + r) for tomorrow with some interest rate r > 0.Let G be a sequence of random variables on Ωfut1, Borel sets. So you have many functions fk : {1, 2, 3, 4}→ R with G(k) = fk and fk is a random variable of Ωfut1, Borel sets. For every fk we have fk(w) = π(k)·(1+r) for w {1, 2, 3, 4}.TodayTomorrowonly one scenario{w21={1,2}w22={3,4}for all d∈𝕅 holds π(d){fd(w)=G(d)(w)=π(d)⋅(1+r),w∈w21 or w∈w22,r>0 is the interest rate.$$\matrix{  {Today} & {Tomorrow} \cr  {{\rm{only}}\,{\rm{one}}\,{\rm{scenario}}} & {\left\{ {\matrix{  {w_{21} = \left\{ {1,2} \right\}} \hfill \cr  {w_{22} = \left\{ {3,4} \right\}} \hfill \cr } } \right.} \cr  {{\rm{for}}\,{\rm{all}}\,d \in N\,{\rm{holds}}\,\pi \left( d \right)} & {\left\{ {\matrix{  {f_d \left( w \right) = G\left( d \right)\left( w \right) = \pi \left( d \right) \cdot \left( {1 + r} \right),} \hfill \cr  {w \in w_{21} \,or\,w \in w_{22} ,} \hfill \cr  {r > 0\,{\rm{is}}\,{\rm{the}}\,{\rm{interest}}\,{\rm{rate}}.} \hfill \cr } } \right.} \cr }$$Here, every probability measure of Ωfut1 is a risk-neutral measure.

Introduction to Stochastic Finance: Random Variables and Arbitrage Theory

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Introduction to Stochastic Finance: Random Variables and Arbitrage Theory"}

Using the Mizar system [1], [5], we start to show, that the Call-Option, the Put-Option and the Straddle (more generally defined as in the literature) are...

Introduction to Stochastic Finance: Random Variables and Arbitrage Theory

Published Online: Jul 28, 2018

Page range: 1 - 9

Received: Mar 27, 2018

DOI: https://doi.org/10.2478/forma-2018-0001

Keywords
random variable, arbitrage theory, risk-neutral measure

© 2018 Peter Jaeger, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Introduction to Stochastic Finance: Random Variables and Arbitrage Theory

Published Online: Jul 28, 2018

Page range: 1 - 9

Received: Mar 27, 2018

DOI: https://doi.org/10.2478/forma-2018-0001

Keywordsrandom variable, arbitrage theory, risk-neutral measure

© 2018 Peter Jaeger, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Keywords
random variable, arbitrage theory, risk-neutral measure