let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for RV being random_variable of F, Borel_Sets
for K being Real
for w being Element of Omega holds (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).|
let F be SigmaField of Omega; :: thesis: for RV being random_variable of F, Borel_Sets
for K being Real
for w being Element of Omega holds (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).|
let RV be random_variable of F, Borel_Sets ; :: thesis: for K being Real
for w being Element of Omega holds (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).|
let K be Real; :: thesis: for w being Element of Omega holds (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).|
let w be Element of Omega; :: thesis: (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).|
set f1 = RV;
set f2 = (- 1) (#) (Omega --> K);
SS: ( dom RV = Omega & dom ((- 1) (#) (Omega --> K)) = Omega ) by FUNCT_2:def 1;
then w in (dom RV) /\ (dom ((- 1) (#) (Omega --> K))) ;
then C1: w in dom (RV + ((- 1) (#) (Omega --> K))) by VALUED_1:def 1;
( dom (Put-Option (RV,K)) = Omega & dom (Call-Option (RV,K)) = Omega ) by FUNCT_2:def 1;
then w in (dom (Put-Option (RV,K))) /\ (dom (Call-Option (RV,K))) ;
then B100: w in dom ((Put-Option (RV,K)) + (Call-Option (RV,K))) by VALUED_1:def 1;
c2: ( dom (Omega --> K) = Omega & dom ((- 1) (#) (Omega --> K)) = dom (Omega --> K) ) by VALUED_1:def 5;
c4: w in dom RV by SS;
then C6: w in dom ((- 1) (#) RV) by VALUED_1:def 5;

per cases ( (RV - (Omega --> K)) . w > 0 or (RV - (Omega --> K)) . w < 0 or (RV - (Omega --> K)) . w = 0 ) ;

suppose S1: (RV - (Omega --> K)) . w > 0 ; :: thesis: (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).|

then B0: |.((RV - (Omega --> K)) . w).| = (RV - (Omega --> K)) . w by COMPLEX1:43;
dom (- RV) = Omega by FUNCT_2:def 1;
then w in (dom (Omega --> K)) /\ (dom (- RV)) ;
then C7: w in dom ((Omega --> K) + (- RV)) by VALUED_1:def 1;
((Omega --> K) - RV) . w < 0

proof

(RV - (Omega --> K)) . w = (RV . w) + (((- 1) (#) (Omega --> K)) . w) by C1, VALUED_1:def 1
.= (RV . w) + ((- 1) * ((Omega --> K) . w)) by c2, VALUED_1:def 5 ;
then - ((RV . w) - K) < 0 by S1;
then K - (RV . w) < 0 ;
then ((Omega --> K) . w) + ((- 1) * (RV . w)) < 0 ;
then ((Omega --> K) . w) + (((- 1) (#) RV) . w) < 0 by C6, VALUED_1:def 5;
hence ((Omega --> K) - RV) . w < 0 by C7, VALUED_1:def 1; :: thesis: verum

end;

then B2: (Put-Option (RV,K)) . w = 0 by Def30;
((Put-Option (RV,K)) + (Call-Option (RV,K))) . w = ((Put-Option (RV,K)) . w) + ((Call-Option (RV,K)) . w) by B100, VALUED_1:def 1;
hence (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).| by B0, B2, FINANCE3:def 5, S1; :: thesis: verum

end;

suppose S1: (RV - (Omega --> K)) . w < 0 ; :: thesis: (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).|

( dom (Put-Option (RV,K)) = Omega & dom (Call-Option (RV,K)) = Omega ) by FUNCT_2:def 1;
then w in (dom (Put-Option (RV,K))) /\ (dom (Call-Option (RV,K))) ;
then B100: w in dom ((Put-Option (RV,K)) + (Call-Option (RV,K))) by VALUED_1:def 1;
c2: ( dom (Omega --> K) = Omega & dom ((- 1) (#) (Omega --> K)) = dom (Omega --> K) ) by VALUED_1:def 5;
C6: w in dom ((- 1) (#) RV) by VALUED_1:def 5, c4;
( dom (Omega --> K) = Omega & dom (- RV) = Omega ) by FUNCT_2:def 1;
then w in (dom (Omega --> K)) /\ (dom (- RV)) ;
then C7: w in dom ((Omega --> K) + (- RV)) by VALUED_1:def 1;
((Omega --> K) - RV) . w > 0

proof

(RV - (Omega --> K)) . w = (RV . w) + (((- 1) (#) (Omega --> K)) . w) by C1, VALUED_1:def 1
.= (RV . w) + ((- 1) * ((Omega --> K) . w)) by c2, VALUED_1:def 5 ;
then - ((RV . w) - K) > 0 by S1;
then K - (RV . w) > 0 ;
then ((Omega --> K) . w) + ((- 1) * (RV . w)) > 0 ;
then ((Omega --> K) . w) + (((- 1) (#) RV) . w) > 0 by C6, VALUED_1:def 5;
hence ((Omega --> K) - RV) . w > 0 by C7, VALUED_1:def 1; :: thesis: verum

end;

then B2: (Put-Option (RV,K)) . w = ((Omega --> K) - RV) . w by Def30;
(Call-Option (RV,K)) . w = 0 by FINANCE3:def 5, S1;
then B40: (Straddle (RV,K)) . w = 0 + (((Omega --> K) - RV) . w) by B2, B100, VALUED_1:def 1;
( dom (Omega --> K) = Omega & dom ((- 1) (#) RV) = Omega ) by FUNCT_2:def 1;
then w in (dom (Omega --> K)) /\ (dom ((- 1) (#) RV)) ;
then w in dom ((Omega --> K) + ((- 1) (#) RV)) by VALUED_1:def 1;
then U2: ((Omega --> K) - RV) . w = ((Omega --> K) . w) + (((- 1) (#) RV) . w) by VALUED_1:def 1;
dom ((- 1) (#) RV) = Omega by FUNCT_2:def 1;
then u3: ((Omega --> K) - RV) . w = ((Omega --> K) . w) + ((- 1) * (RV . w)) by U2, VALUED_1:def 5;
L1: (RV . w) + (- ((Omega --> K) . w)) = (RV . w) + ((- 1) * ((Omega --> K) . w)) ;
dom ((- 1) (#) (Omega --> K)) = Omega by FUNCT_2:def 1;
then L2: (RV . w) + (- ((Omega --> K) . w)) = (RV . w) + (((- 1) (#) (Omega --> K)) . w) by L1, VALUED_1:def 5;
w in (dom RV) /\ (dom (- (Omega --> K))) by SS;
then w in dom (RV + (- (Omega --> K))) by VALUED_1:def 1;
then (RV . w) + (- ((Omega --> K) . w)) = (RV + (- (Omega --> K))) . w by L2, VALUED_1:def 1;
then - ((RV - (Omega --> K)) . w) = ((Omega --> K) - RV) . w by u3;
hence (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).| by B40, S1, COMPLEX1:70; :: thesis: verum

end;

suppose S1: (RV - (Omega --> K)) . w = 0 ; :: thesis: (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).|

0 = (Straddle (RV,K)) . w

proof

H2: (RV . w) + (((- 1) (#) (Omega --> K)) . w) = 0 by VALUED_1:1, S1;
( dom (Omega --> K) = Omega & dom ((- 1) (#) (Omega --> K)) = Omega ) by FUNCT_2:def 1;
then h1: (RV . w) + ((- 1) * ((Omega --> K) . w)) = 0 by H2, VALUED_1:def 5;
dom ((- 1) (#) RV) = Omega by FUNCT_2:def 1;
then G2: ((Omega --> K) . w) + (((- 1) (#) RV) . w) = 0 by h1, VALUED_1:def 5;
( dom (Omega --> K) = Omega & dom (- RV) = Omega ) by FUNCT_2:def 1;
then w in (dom (Omega --> K)) /\ (dom (- RV)) ;
then w in dom ((Omega --> K) + (- RV)) by VALUED_1:def 1;
then ((Omega --> K) - RV) . w = 0 by G2, VALUED_1:def 1;
then (Put-Option (RV,K)) . w = - ((RV - (Omega --> K)) . w) by S1, Def30;
then F3: ((Call-Option (RV,K)) . w) + ((Put-Option (RV,K)) . w) = 0 by S1, FINANCE3:def 5;
( dom (Call-Option (RV,K)) = Omega & dom (Put-Option (RV,K)) = Omega ) by FUNCT_2:def 1;
then w in (dom (Call-Option (RV,K))) /\ (dom (Put-Option (RV,K))) ;
then w in dom ((Call-Option (RV,K)) + (Put-Option (RV,K))) by VALUED_1:def 1;
hence 0 = (Straddle (RV,K)) . w by F3, VALUED_1:def 1; :: thesis: verum

end;

hence (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).| by COMPLEX1:43, S1; :: thesis: verum

end;

end;