let Omega be non empty set ; 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; 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 ; for K being Real
for w being Element of Omega holds (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).|
let K be Real; for w being Element of Omega holds (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).|
let w be Element of Omega; (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
;
(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
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;
verum end; suppose S1:
(RV - (Omega --> K)) . w < 0
;
(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
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;
verum suppose S1:
(RV - (Omega --> K)) . w = 0
;
(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;
verum
end; hence
(Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).|
by COMPLEX1:43, S1;
verum end;