let Omega be non empty set ; for F being SigmaField of Omega
for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for phi being Real_Sequence
for d being Nat holds RVPortfolioValueFut (phi,F,G,d) is random_variable of F, Borel_Sets
let F be SigmaField of Omega; for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for phi being Real_Sequence
for d being Nat holds RVPortfolioValueFut (phi,F,G,d) is random_variable of F, Borel_Sets
let G be sequence of (set_of_random_variables_on (F,Borel_Sets)); for phi being Real_Sequence
for d being Nat holds RVPortfolioValueFut (phi,F,G,d) is random_variable of F, Borel_Sets
let phi be Real_Sequence; for d being Nat holds RVPortfolioValueFut (phi,F,G,d) is random_variable of F, Borel_Sets
let d be Nat; RVPortfolioValueFut (phi,F,G,d) is random_variable of F, Borel_Sets
defpred S1[ Nat] means RVPortfolioValueFut (phi,F,G,$1) is random_variable of F, Borel_Sets ;
ElementsOfPortfolioValueProb_fut (F,(G . (0 + 1))) is random_variable of F, Borel_Sets
by FINANCE2:28;
then A1:
(phi . (0 + 1)) (#) (ElementsOfPortfolioValueProb_fut (F,(G . (0 + 1)))) is random_variable of F, Borel_Sets
by FINANCE2:26;
RVPortfolioValueFut (phi,F,G,0) is random_variable of F, Borel_Sets
proof
for
w being
Element of
Omega holds
(RVPortfolioValueFut (phi,F,G,0)) . w = ((phi . (0 + 1)) (#) (ElementsOfPortfolioValueProb_fut (F,(G . (0 + 1))))) . w
proof
let w be
Element of
Omega;
(RVPortfolioValueFut (phi,F,G,0)) . w = ((phi . (0 + 1)) (#) (ElementsOfPortfolioValueProb_fut (F,(G . (0 + 1))))) . w
consider k being
Nat such that B0:
k = 0
;
(RVPortfolioValueFut (phi,F,G,k)) . w =
PortfolioValueFut (
(k + 1),
phi,
F,
G,
w)
by Def4
.=
((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1) . k
by B0, SERIES_1:def 1
.=
(RVPortfolioValueFutExt_El (phi,F,G,w)) . (k + 1)
by NAT_1:def 3
.=
(RVElementsOfPortfolioValue_fut (phi,F,G,(k + 1))) . w
by FINANCE2:def 6
;
then
(RVPortfolioValueFut (phi,F,G,0)) . w = ((ElementsOfPortfolioValueProb_fut (F,(G . (0 + 1)))) . w) * (phi . (0 + 1))
by FINANCE2:def 5, B0;
hence
(RVPortfolioValueFut (phi,F,G,0)) . w = ((phi . (0 + 1)) (#) (ElementsOfPortfolioValueProb_fut (F,(G . (0 + 1))))) . w
by VALUED_1:6;
verum
end;
hence
RVPortfolioValueFut (
phi,
F,
G,
0) is
random_variable of
F,
Borel_Sets
by A1, FUNCT_2:63;
verum
end;
then J0:
S1[ 0 ]
;
J1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume B1:
S1[
n]
;
S1[n + 1]
C0:
for
w being
Element of
Omega holds
(RVPortfolioValueFut (phi,F,G,(n + 1))) . w = ((RVPortfolioValueFut (phi,F,G,n)) . w) + ((RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1))) . w)
proof
let w be
Element of
Omega;
(RVPortfolioValueFut (phi,F,G,(n + 1))) . w = ((RVPortfolioValueFut (phi,F,G,n)) . w) + ((RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1))) . w)
set k =
n + 1;
(RVPortfolioValueFut (phi,F,G,(n + 1))) . w = PortfolioValueFut (
((n + 1) + 1),
phi,
F,
G,
w)
by Def4;
then
(RVPortfolioValueFut (phi,F,G,(n + 1))) . w = (PortfolioValueFut ((n + 1),phi,F,G,w)) + (((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1) . (n + 1))
by SERIES_1:def 1;
then (RVPortfolioValueFut (phi,F,G,(n + 1))) . w =
((RVPortfolioValueFut (phi,F,G,n)) . w) + (((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1) . (n + 1))
by Def4
.=
((RVPortfolioValueFut (phi,F,G,n)) . w) + ((RVPortfolioValueFutExt_El (phi,F,G,w)) . ((n + 1) + 1))
by NAT_1:def 3
;
hence
(RVPortfolioValueFut (phi,F,G,(n + 1))) . w = ((RVPortfolioValueFut (phi,F,G,n)) . w) + ((RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1))) . w)
by FINANCE2:def 6;
verum
end;
K1:
RVElementsOfPortfolioValue_fut (
phi,
F,
G,
((n + 1) + 1)) is
random_variable of
F,
Borel_Sets
by FINANCE2:30;
C2:
dom (RVPortfolioValueFut (phi,F,G,n)) = Omega
by FUNCT_2:def 1;
dom (RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1))) = Omega
by FUNCT_2:def 1;
then
(
dom (RVPortfolioValueFut (phi,F,G,(n + 1))) = (dom (RVPortfolioValueFut (phi,F,G,n))) /\ (dom (RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1)))) & ( for
c being
object st
c in dom (RVPortfolioValueFut (phi,F,G,(n + 1))) holds
(RVPortfolioValueFut (phi,F,G,(n + 1))) . c = ((RVPortfolioValueFut (phi,F,G,n)) . c) + ((RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1))) . c) ) )
by C0, FUNCT_2:def 1, C2;
then
RVPortfolioValueFut (
phi,
F,
G,
(n + 1))
= (RVPortfolioValueFut (phi,F,G,n)) + (RVElementsOfPortfolioValue_fut (phi,F,G,((n + 1) + 1)))
by VALUED_1:def 1;
hence
S1[
n + 1]
by B1, K1, FINANCE2:23;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(J0, J1);
hence
RVPortfolioValueFut (phi,F,G,d) is random_variable of F, Borel_Sets
; verum