Summary
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}.
$$\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.
Probability Measure on Discrete Spaces and Algebra of Real-Valued Random Variables
