:: FINANCE1 semantic presentation
begin
notation
let a, r be real number ;
synonym halfline_fin (a,r) for [.a,r.[;
end;
definition
let a, r be real number ;
:: original: halfline_fin
redefine func halfline_fin (a,r) -> Subset of REAL;
coherence
halfline_fin (a,r) is Subset of REAL
proof
halfline_fin (a,r) = [.a,r.[ ;
hence halfline_fin (a,r) is Subset of REAL ; ::_thesis: verum
end;
end;
theorem :: FINANCE1:1
for k being real number holds REAL \ [.k,+infty.[ = ].-infty,k.[
proof
let k be real number ; ::_thesis: REAL \ [.k,+infty.[ = ].-infty,k.[
A1: k in REAL by XREAL_0:def_1;
for x being set holds
( x in REAL \ [.k,+infty.[ iff x in ].-infty,k.[ )
proof
let x be set ; ::_thesis: ( x in REAL \ [.k,+infty.[ iff x in ].-infty,k.[ )
hereby ::_thesis: ( x in ].-infty,k.[ implies x in REAL \ [.k,+infty.[ )
assume A2: x in REAL \ [.k,+infty.[ ; ::_thesis: x in ].-infty,k.[
A3: ( x in ].-infty,+infty.[ & not x in [.k,+infty.[ ) by A2, XBOOLE_0:def_5, XXREAL_1:224;
consider y being Element of REAL such that
A4: x = y by A2;
( y in ].-infty,+infty.[ & not y >= k ) by A4, A3, XXREAL_1:236;
hence x in ].-infty,k.[ by A4, XXREAL_1:233; ::_thesis: verum
end;
assume A5: x in ].-infty,k.[ ; ::_thesis: x in REAL \ [.k,+infty.[
then ( k in REAL & x in ].-infty,k.[ & x in { a where a is Element of ExtREAL : ( -infty < a & a < k ) } ) by XREAL_0:def_1, XXREAL_1:def_4;
then consider a being Element of ExtREAL such that
A6: ( a = x & -infty < a & a < k ) ;
consider y being Element of ExtREAL such that
A7: x = y by A6;
reconsider y = y as Element of REAL by A1, A6, A7, XXREAL_0:47;
y < k by A5, A7, XXREAL_1:233;
then ( y in REAL & not y in [.k,+infty.[ ) by XXREAL_1:236;
hence x in REAL \ [.k,+infty.[ by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
hence REAL \ [.k,+infty.[ = ].-infty,k.[ by TARSKI:1; ::_thesis: verum
end;
theorem Th2: :: FINANCE1:2
for k being real number holds REAL \ ].-infty,k.[ = [.k,+infty.[
proof
let k be real number ; ::_thesis: REAL \ ].-infty,k.[ = [.k,+infty.[
A1: k in REAL by XREAL_0:def_1;
for x being set holds
( x in REAL \ ].-infty,k.[ iff x in [.k,+infty.[ )
proof
let x be set ; ::_thesis: ( x in REAL \ ].-infty,k.[ iff x in [.k,+infty.[ )
hereby ::_thesis: ( x in [.k,+infty.[ implies x in REAL \ ].-infty,k.[ )
assume A2: x in REAL \ ].-infty,k.[ ; ::_thesis: x in [.k,+infty.[
A3: ( x in ].-infty,+infty.[ & not x in ].-infty,k.[ ) by A2, XBOOLE_0:def_5, XXREAL_1:224;
consider y being Element of REAL such that
A4: x = y by A2;
A5: ( y in ].-infty,+infty.[ & not y < k ) by A4, A3, XXREAL_1:233;
thus x in [.k,+infty.[ by A5, A4, XXREAL_1:236; ::_thesis: verum
end;
assume A6: x in [.k,+infty.[ ; ::_thesis: x in REAL \ ].-infty,k.[
then ( k in REAL & x in [.k,+infty.[ & x in { a where a is Element of ExtREAL : ( k <= a & a < +infty ) } ) by XREAL_0:def_1, XXREAL_1:def_2;
then consider a being Element of ExtREAL such that
A7: ( a = x & k <= a & a < +infty ) ;
consider y being Element of ExtREAL such that
A8: x = y by A7;
reconsider y = y as Element of REAL by A7, A8, A1, XXREAL_0:46;
y >= k by A6, A8, XXREAL_1:236;
then ( y in REAL & not y in ].-infty,k.[ ) by XXREAL_1:233;
hence x in REAL \ ].-infty,k.[ by A8, XBOOLE_0:def_5; ::_thesis: verum
end;
hence REAL \ ].-infty,k.[ = [.k,+infty.[ by TARSKI:1; ::_thesis: verum
end;
definition
let a, b be real number ;
func half_open_sets (a,b) -> SetSequence of REAL means :Def1: :: FINANCE1:def 1
( it . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds it . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) );
existence
ex b1 being SetSequence of REAL st
( b1 . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds b1 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) )
proof
defpred S1[ set , set , set ] means for x, y being Subset of REAL
for s being Nat st s = $1 & x = $2 & y = $3 holds
y = halfline_fin (a,(b + (1 / (s + 1))));
A1: for n being Element of NAT
for x being Subset of REAL ex y being Subset of REAL st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Subset of REAL ex y being Subset of REAL st S1[n,x,y]
let x be Subset of REAL; ::_thesis: ex y being Subset of REAL st S1[n,x,y]
take halfline_fin (a,(b + (1 / (n + 1)))) ; ::_thesis: S1[n,x, halfline_fin (a,(b + (1 / (n + 1))))]
thus S1[n,x, halfline_fin (a,(b + (1 / (n + 1))))] ; ::_thesis: verum
end;
consider F being SetSequence of REAL such that
A2: F . 0 = halfline_fin (a,(b + 1)) and
A3: for n being Element of NAT holds S1[n,F . n,F . (n + 1)] from RECDEF_1:sch_2(A1);
take F ; ::_thesis: ( F . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds F . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) )
thus F . 0 = halfline_fin (a,(b + 1)) by A2; ::_thesis: for n being Element of NAT holds F . (n + 1) = halfline_fin (a,(b + (1 / (n + 1))))
let n be Nat; ::_thesis: ( n is Element of REAL & n is Element of NAT implies F . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) )
reconsider n = n as Element of NAT by ORDINAL1:def_12;
S1[n,F . n,F . (n + 1)] by A3;
hence ( n is Element of REAL & n is Element of NAT implies F . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being SetSequence of REAL st b1 . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds b1 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) & b2 . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds b2 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) holds
b1 = b2
proof
let S1, S2 be SetSequence of REAL; ::_thesis: ( S1 . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds S1 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) & S2 . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds S2 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) implies S1 = S2 )
assume that
A4: ( S1 . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds S1 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) ) and
A5: ( S2 . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds S2 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) ) ; ::_thesis: S1 = S2
defpred S1[ set ] means S1 . $1 = S2 . $1;
for n being set st n in NAT holds
S1[n]
proof
let n be set ; ::_thesis: ( n in NAT implies S1[n] )
assume n in NAT ; ::_thesis: S1[n]
then reconsider n = n as Element of NAT ;
A6: S1[ 0 ] by A4, A5;
A7: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1 . k = S2 . k ; ::_thesis: S1[k + 1]
thus S1 . (k + 1) = halfline_fin (a,(b + (1 / (k + 1)))) by A4
.= S2 . (k + 1) by A5 ; ::_thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A6, A7);
then S1 . n = S2 . n ;
hence S1[n] ; ::_thesis: verum
end;
hence S1 = S2 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines half_open_sets FINANCE1:def_1_:_
for a, b being real number
for b3 being SetSequence of REAL holds
( b3 = half_open_sets (a,b) iff ( b3 . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds b3 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) ) );
definition
mode pricefunction -> Real_Sequence means :Def2: :: FINANCE1:def 2
( it . 0 = 1 & ( for n being Element of NAT holds it . n >= 0 ) );
existence
ex b1 being Real_Sequence st
( b1 . 0 = 1 & ( for n being Element of NAT holds b1 . n >= 0 ) )
proof
reconsider j = 1 as Element of REAL ;
take NAT --> j ; ::_thesis: ( (NAT --> j) . 0 = 1 & ( for n being Element of NAT holds (NAT --> j) . n >= 0 ) )
thus ( (NAT --> j) . 0 = 1 & ( for n being Element of NAT holds (NAT --> j) . n >= 0 ) ) by FUNCOP_1:7; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines pricefunction FINANCE1:def_2_:_
for b1 being Real_Sequence holds
( b1 is pricefunction iff ( b1 . 0 = 1 & ( for n being Element of NAT holds b1 . n >= 0 ) ) );
notation
let phi, jpi be Real_Sequence;
synonym ElementsOfBuyPortfolio (phi,jpi) for phi (#) jpi;
end;
definition
let phi, jpi be Real_Sequence;
:: original: ElementsOfBuyPortfolio
redefine func ElementsOfBuyPortfolio (phi,jpi) -> Real_Sequence;
coherence
ElementsOfBuyPortfolio (phi,jpi) is Real_Sequence
proof
ElementsOfBuyPortfolio (phi,jpi) = phi (#) jpi ;
hence ElementsOfBuyPortfolio (phi,jpi) is Real_Sequence ; ::_thesis: verum
end;
end;
definition
let d be Nat;
let phi, jpi be Real_Sequence;
func BuyPortfolioExt (phi,jpi,d) -> Element of REAL equals :: FINANCE1:def 3
(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . d;
coherence
(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . d is Element of REAL ;
func BuyPortfolio (phi,jpi,d) -> Element of REAL equals :: FINANCE1:def 4
(Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1);
coherence
(Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1) is Element of REAL ;
end;
:: deftheorem defines BuyPortfolioExt FINANCE1:def_3_:_
for d being Nat
for phi, jpi being Real_Sequence holds BuyPortfolioExt (phi,jpi,d) = (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . d;
:: deftheorem defines BuyPortfolio FINANCE1:def_4_:_
for d being Nat
for phi, jpi being Real_Sequence holds BuyPortfolio (phi,jpi,d) = (Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1);
definition
let Omega, Omega2 be set ;
let Sigma be SigmaField of Omega;
let Sigma2 be SigmaField of Omega2;
let X be Function;
predX is_random_variable_on Sigma,Sigma2 means :Def5: :: FINANCE1:def 5
for x being Element of Sigma2 holds { y where y is Element of Omega : X . y is Element of x } is Element of Sigma;
end;
:: deftheorem Def5 defines is_random_variable_on FINANCE1:def_5_:_
for Omega, Omega2 being set
for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for X being Function holds
( X is_random_variable_on Sigma,Sigma2 iff for x being Element of Sigma2 holds { y where y is Element of Omega : X . y is Element of x } is Element of Sigma );
definition
let Omega, Omega2 be set ;
let F be SigmaField of Omega;
let F2 be SigmaField of Omega2;
func set_of_random_variables_on (F,F2) -> set equals :: FINANCE1:def 6
{ f where f is Function of Omega,Omega2 : f is_random_variable_on F,F2 } ;
coherence
{ f where f is Function of Omega,Omega2 : f is_random_variable_on F,F2 } is set ;
end;
:: deftheorem defines set_of_random_variables_on FINANCE1:def_6_:_
for Omega, Omega2 being set
for F being SigmaField of Omega
for F2 being SigmaField of Omega2 holds set_of_random_variables_on (F,F2) = { f where f is Function of Omega,Omega2 : f is_random_variable_on F,F2 } ;
registration
let Omega, Omega2 be non empty set ;
let F be SigmaField of Omega;
let F2 be SigmaField of Omega2;
cluster set_of_random_variables_on (F,F2) -> non empty ;
coherence
not set_of_random_variables_on (F,F2) is empty
proof
set X = set_of_random_variables_on (F,F2);
ex z being Function of Omega,Omega2 st z is_random_variable_on F,F2
proof
set k = the Element of Omega2;
set z = Omega --> the Element of Omega2;
A1: ( Omega --> the Element of Omega2 is_random_variable_on F,F2 iff for x being Element of F2 holds { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } is Element of F ) by Def5;
for x being Element of F2 holds { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } is Element of F
proof
let x be Element of F2; ::_thesis: { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } is Element of F
set K = { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } ;
percases ( the Element of Omega2 is Element of x or not the Element of Omega2 is Element of x ) ;
supposeA2: the Element of Omega2 is Element of x ; ::_thesis: { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } is Element of F
for s being set holds
( s in { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } iff s in Omega )
proof
let s be set ; ::_thesis: ( s in { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } iff s in Omega )
hereby ::_thesis: ( s in Omega implies s in { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } )
assume s in { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } ; ::_thesis: s in Omega
then ex y being Element of Omega st
( y = s & (Omega --> the Element of Omega2) . y is Element of x ) ;
hence s in Omega ; ::_thesis: verum
end;
assume s in Omega ; ::_thesis: s in { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x }
then ( s in Omega & (Omega --> the Element of Omega2) . s is Element of x ) by A2, FUNCOP_1:7;
hence s in { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } ; ::_thesis: verum
end;
then { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } = Omega by TARSKI:1;
hence { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } is Element of F by PROB_1:23; ::_thesis: verum
end;
supposeA3: the Element of Omega2 is not Element of x ; ::_thesis: { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } is Element of F
for r being set holds not r in { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x }
proof
let r be set ; ::_thesis: not r in { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x }
assume r in { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } ; ::_thesis: contradiction
then ex y being Element of Omega st
( y = r & (Omega --> the Element of Omega2) . y is Element of x ) ;
hence contradiction by A3, FUNCOP_1:7; ::_thesis: verum
end;
then { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } = {} by XBOOLE_0:def_1;
hence { y where y is Element of Omega : (Omega --> the Element of Omega2) . y is Element of x } is Element of F by PROB_1:4; ::_thesis: verum
end;
end;
end;
hence ex z being Function of Omega,Omega2 st z is_random_variable_on F,F2 by A1; ::_thesis: verum
end;
then consider z being Function of Omega,Omega2 such that
A4: z is_random_variable_on F,F2 ;
z in set_of_random_variables_on (F,F2) by A4;
hence not set_of_random_variables_on (F,F2) is empty ; ::_thesis: verum
end;
end;
definition
let Omega, Omega2 be non empty set ;
let F be SigmaField of Omega;
let F2 be SigmaField of Omega2;
let X be set ;
assume T1: X = set_of_random_variables_on (F,F2) ;
let k be Element of X;
func Change_Element_to_Func (F,F2,k) -> Function of Omega,Omega2 equals :Def7: :: FINANCE1:def 7
k;
coherence
k is Function of Omega,Omega2
proof
k in X by T1;
then ex f being Function of Omega,Omega2 st
( f = k & f is_random_variable_on F,F2 ) by T1;
hence k is Function of Omega,Omega2 ; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines Change_Element_to_Func FINANCE1:def_7_:_
for Omega, Omega2 being non empty set
for F being SigmaField of Omega
for F2 being SigmaField of Omega2
for X being set st X = set_of_random_variables_on (F,F2) holds
for k being Element of X holds Change_Element_to_Func (F,F2,k) = k;
definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let X be non empty set ;
let k be Element of X;
func ElementsOfPortfolioValueProb_fut (F,k) -> Function of Omega,REAL means :Def8: :: FINANCE1:def 8
for w being Element of Omega holds it . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w;
existence
ex b1 being Function of Omega,REAL st
for w being Element of Omega holds b1 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w
proof
deffunc H1( Element of Omega) -> Element of REAL = (Change_Element_to_Func (F,Borel_Sets,k)) . $1;
ex f being Function of Omega,REAL st
for d being Element of Omega holds f . d = H1(d) from FUNCT_2:sch_4();
hence ex b1 being Function of Omega,REAL st
for w being Element of Omega holds b1 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of Omega,REAL st ( for w being Element of Omega holds b1 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ) & ( for w being Element of Omega holds b2 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ) holds
b1 = b2
proof
let f1, f2 be Function of Omega,REAL; ::_thesis: ( ( for w being Element of Omega holds f1 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ) & ( for w being Element of Omega holds f2 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ) implies f1 = f2 )
assume that
A1: for w being Element of Omega holds f1 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w and
A2: for w being Element of Omega holds f2 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ; ::_thesis: f1 = f2
let w be Element of Omega; :: according to FUNCT_2:def_8 ::_thesis: f1 . w = f2 . w
( f1 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w & f2 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ) by A1, A2;
hence f1 . w = f2 . w ; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines ElementsOfPortfolioValueProb_fut FINANCE1:def_8_:_
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for k being Element of X
for b5 being Function of Omega,REAL holds
( b5 = ElementsOfPortfolioValueProb_fut (F,k) iff for w being Element of Omega holds b5 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w );
definition
let p be Nat;
let Omega, Omega2 be non empty set ;
let F be SigmaField of Omega;
let F2 be SigmaField of Omega2;
let X be set ;
assume T1: X = set_of_random_variables_on (F,F2) ;
let G be Function of NAT,X;
func Element_Of (F,F2,G,p) -> Function of Omega,Omega2 equals :Def9: :: FINANCE1:def 9
G . p;
coherence
G . p is Function of Omega,Omega2
proof
reconsider p = p as Element of NAT by ORDINAL1:def_12;
G . p in { f where f is Function of Omega,Omega2 : f is_random_variable_on F,F2 } by T1;
then ex f being Function of Omega,Omega2 st
( f = G . p & f is_random_variable_on F,F2 ) ;
hence G . p is Function of Omega,Omega2 ; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines Element_Of FINANCE1:def_9_:_
for p being Nat
for Omega, Omega2 being non empty set
for F being SigmaField of Omega
for F2 being SigmaField of Omega2
for X being set st X = set_of_random_variables_on (F,F2) holds
for G being Function of NAT,X holds Element_Of (F,F2,G,p) = G . p;
definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let X be non empty set ;
let w be Element of Omega;
let G be Function of NAT,X;
let phi be Real_Sequence;
func ElementsOfPortfolioValue_fut (phi,F,w,G) -> Real_Sequence means :Def10: :: FINANCE1:def 10
for n being Element of NAT holds it . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n);
existence
ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n)
proof
deffunc H1( Element of NAT ) -> Element of REAL = ((ElementsOfPortfolioValueProb_fut (F,(G . $1))) . w) * (phi . $1);
ex f being Real_Sequence st
for d being Element of NAT holds f . d = H1(d) from FUNCT_2:sch_4();
hence ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) & ( for n being Element of NAT holds b2 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) holds
b1 = b2
proof
let f1, f2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds f1 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) & ( for n being Element of NAT holds f2 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) implies f1 = f2 )
assume that
A1: for d being Element of NAT holds f1 . d = ((ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d) and
A2: for d being Element of NAT holds f2 . d = ((ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d) ; ::_thesis: f1 = f2
let d be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: f1 . d = f2 . d
( f1 . d = ((ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d) & f2 . d = ((ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d) ) by A1, A2;
hence f1 . d = f2 . d ; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines ElementsOfPortfolioValue_fut FINANCE1:def_10_:_
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for w being Element of Omega
for G being Function of NAT,X
for phi, b7 being Real_Sequence holds
( b7 = ElementsOfPortfolioValue_fut (phi,F,w,G) iff for n being Element of NAT holds b7 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) );
definition
let d be Nat;
let phi be Real_Sequence;
let Omega be non empty set ;
let F be SigmaField of Omega;
let X be non empty set ;
let G be Function of NAT,X;
let w be Element of Omega;
func PortfolioValueFutExt (d,phi,F,G,w) -> Element of REAL equals :: FINANCE1:def 11
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . d;
coherence
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . d is Element of REAL ;
func PortfolioValueFut (d,phi,F,G,w) -> Element of REAL equals :: FINANCE1:def 12
(Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1);
coherence
(Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1) is Element of REAL ;
end;
:: deftheorem defines PortfolioValueFutExt FINANCE1:def_11_:_
for d being Nat
for phi being Real_Sequence
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for G being Function of NAT,X
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . d;
:: deftheorem defines PortfolioValueFut FINANCE1:def_12_:_
for d being Nat
for phi being Real_Sequence
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for G being Function of NAT,X
for w being Element of Omega holds PortfolioValueFut (d,phi,F,G,w) = (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1);
registration
cluster non empty for Element of Borel_Sets ;
existence
not for b1 being Element of Borel_Sets holds b1 is empty
proof
consider m being real number such that
A1: m > -infty ;
set L = halfline m;
set LL = Family_of_halflines ;
A2: not halfline m is empty by A1, XXREAL_1:33;
m in REAL by XREAL_0:def_1;
then A3: halfline m in Family_of_halflines ;
Family_of_halflines is Subset of Borel_Sets by PROB_1:def_9;
hence not for b1 being Element of Borel_Sets holds b1 is empty by A3, A2; ::_thesis: verum
end;
end;
theorem Th3: :: FINANCE1:3
for k being real number holds
( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets )
proof
let k be real number ; ::_thesis: ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets )
A1: k in REAL by XREAL_0:def_1;
set R = ].-infty,k.[;
A2: ].-infty,k.[ in Borel_Sets
proof
set L = halfline k;
A3: ( halfline k in Family_of_halflines & halfline k = ].-infty,k.[ ) by A1;
Family_of_halflines c= sigma Family_of_halflines by PROB_1:def_9;
hence ].-infty,k.[ in Borel_Sets by A3; ::_thesis: verum
end;
then ].-infty,k.[ ` in Borel_Sets by PROB_1:def_1;
hence ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets ) by Th2, A2; ::_thesis: verum
end;
theorem Th4: :: FINANCE1:4
for k1, k2 being real number holds [.k2,k1.[ is Element of Borel_Sets
proof
let k1, k2 be real number ; ::_thesis: [.k2,k1.[ is Element of Borel_Sets
set R = ].-infty,k2.[;
( k1 in REAL & k2 in REAL ) by XREAL_0:def_1;
then A1: ( -infty < k2 & k1 < +infty ) by XXREAL_0:9, XXREAL_0:12;
A2: REAL \ ].-infty,k2.[ = [.k2,+infty.[ by Th2;
( ].-infty,k2.[ ` is Element of Borel_Sets & ].-infty,k1.[ is Element of Borel_Sets & [.k1,+infty.[ is Element of Borel_Sets ) by Th3, A2;
then ].-infty,k1.[ /\ (].-infty,k2.[ `) is Element of Borel_Sets by FINSUB_1:def_2;
then ].-infty,k1.[ /\ [.k2,+infty.[ is Element of Borel_Sets by Th2;
hence [.k2,k1.[ is Element of Borel_Sets by A1, XXREAL_1:154; ::_thesis: verum
end;
theorem Th5: :: FINANCE1:5
for a, b being real number holds Intersection (half_open_sets (a,b)) is Element of Borel_Sets
proof
let a, b be real number ; ::_thesis: Intersection (half_open_sets (a,b)) is Element of Borel_Sets
for n being Element of NAT holds (Complement (half_open_sets (a,b))) . n is Element of Borel_Sets
proof
let n be Element of NAT ; ::_thesis: (Complement (half_open_sets (a,b))) . n is Element of Borel_Sets
((half_open_sets (a,b)) . n) ` is Element of Borel_Sets
proof
(half_open_sets (a,b)) . n is Element of Borel_Sets
proof
percases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6;
supposeA1: n = 0 ; ::_thesis: (half_open_sets (a,b)) . n is Element of Borel_Sets
(half_open_sets (a,b)) . 0 = halfline_fin (a,(b + 1)) by Def1;
hence (half_open_sets (a,b)) . n is Element of Borel_Sets by A1, Th4; ::_thesis: verum
end;
suppose ex k being Nat st n = k + 1 ; ::_thesis: (half_open_sets (a,b)) . n is Element of Borel_Sets
then consider k being Nat such that
A2: n = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
(half_open_sets (a,b)) . (k + 1) = halfline_fin (a,(b + (1 / (k + 1)))) by Def1;
hence (half_open_sets (a,b)) . n is Element of Borel_Sets by A2, Th4; ::_thesis: verum
end;
end;
end;
hence ((half_open_sets (a,b)) . n) ` is Element of Borel_Sets by PROB_1:def_1; ::_thesis: verum
end;
hence (Complement (half_open_sets (a,b))) . n is Element of Borel_Sets by PROB_1:def_2; ::_thesis: verum
end;
then Complement (half_open_sets (a,b)) is SetSequence of Borel_Sets by PROB_1:25;
then Union (Complement (half_open_sets (a,b))) is Element of Borel_Sets by PROB_1:26;
hence Intersection (half_open_sets (a,b)) is Element of Borel_Sets by PROB_1:def_1; ::_thesis: verum
end;
theorem Th6: :: FINANCE1:6
for a, b being real number holds Intersection (half_open_sets (a,b)) = [.a,b.]
proof
let a, b be real number ; ::_thesis: Intersection (half_open_sets (a,b)) = [.a,b.]
A1: for c being set st not c in [.a,b.] holds
not c in Intersection (half_open_sets (a,b))
proof
let c be set ; ::_thesis: ( not c in [.a,b.] implies not c in Intersection (half_open_sets (a,b)) )
assume A2: not c in [.a,b.] ; ::_thesis: not c in Intersection (half_open_sets (a,b))
percases ( not c in REAL or ( c in REAL & not c in [.a,b.] ) ) by A2;
suppose not c in REAL ; ::_thesis: not c in Intersection (half_open_sets (a,b))
hence not c in Intersection (half_open_sets (a,b)) ; ::_thesis: verum
end;
supposeA3: ( c in REAL & not c in [.a,b.] ) ; ::_thesis: not c in Intersection (half_open_sets (a,b))
then reconsider c = c as Element of REAL ;
A4: not c in { q where q is Element of ExtREAL : ( a <= q & q <= b ) } by A3, XXREAL_1:def_1;
A5: ( a > c or c > b )
proof
reconsider q = c as Element of ExtREAL by XXREAL_0:def_1;
( not c = q or not a <= c or not c <= b ) by A4;
hence ( a > c or c > b ) ; ::_thesis: verum
end;
percases ( a > c or c > b ) by A5;
supposeA6: a > c ; ::_thesis: not c in Intersection (half_open_sets (a,b))
not for n being Element of NAT holds c in (half_open_sets (a,b)) . n
proof
take n = 0 ; ::_thesis: not c in (half_open_sets (a,b)) . n
( c in (half_open_sets (a,b)) . 0 implies c in halfline_fin (a,(b + 1)) ) by Def1;
then ( c in (half_open_sets (a,b)) . 0 implies c in { q where q is Element of ExtREAL : ( a <= q & q < b + 1 ) } ) by XXREAL_1:def_2;
then ex q being Element of ExtREAL st
( c in (half_open_sets (a,b)) . 0 implies ( c = q & a <= q & q < b + 1 ) ) ;
hence not c in (half_open_sets (a,b)) . n by A6; ::_thesis: verum
end;
hence not c in Intersection (half_open_sets (a,b)) by PROB_1:13; ::_thesis: verum
end;
suppose c > b ; ::_thesis: not c in Intersection (half_open_sets (a,b))
then consider n being Element of NAT such that
A7: ( 1 / n < c - b & n > 0 ) by FRECHET:36, XREAL_1:50;
A8: (1 / n) + b < (c - b) + b by A7, XREAL_1:6;
( c in Intersection (half_open_sets (a,b)) implies not b + (1 / n) < c )
proof
assume c in Intersection (half_open_sets (a,b)) ; ::_thesis: not b + (1 / n) < c
then c in (half_open_sets (a,b)) . (n + 1) by PROB_1:13;
then c in [.a,(b + (1 / (n + 1))).[ by Def1;
then c in { q where q is Element of ExtREAL : ( a <= q & q < b + (1 / (n + 1)) ) } by XXREAL_1:def_2;
then consider q being Element of ExtREAL such that
A9: ( c = q & a <= q & q < b + (1 / (n + 1)) ) ;
reconsider a = 1 as Element of NAT ;
n * 1 < (n + 1) * 1 by NAT_1:13;
then A10: a / (n + 1) < a / n by A7, XREAL_1:106;
b + (1 / (n + 1)) < b + (1 / n) by A10, XREAL_1:6;
hence not b + (1 / n) < c by A9, XXREAL_0:2; ::_thesis: verum
end;
hence not c in Intersection (half_open_sets (a,b)) by A8; ::_thesis: verum
end;
end;
end;
end;
end;
A11: for c being set st c in [.a,b.] holds
c in Intersection (half_open_sets (a,b))
proof
let c be set ; ::_thesis: ( c in [.a,b.] implies c in Intersection (half_open_sets (a,b)) )
( c in [.a,b.] implies for n being Element of NAT holds c in (half_open_sets (a,b)) . n )
proof
assume A12: c in [.a,b.] ; ::_thesis: for n being Element of NAT holds c in (half_open_sets (a,b)) . n
let n be Element of NAT ; ::_thesis: c in (half_open_sets (a,b)) . n
A13: b < b + 1 by XREAL_1:29;
[.a,b.] c= (half_open_sets (a,b)) . n
proof
percases ( n = 0 or n > 0 ) ;
supposeA14: n = 0 ; ::_thesis: [.a,b.] c= (half_open_sets (a,b)) . n
(half_open_sets (a,b)) . 0 = halfline_fin (a,(b + 1)) by Def1;
hence [.a,b.] c= (half_open_sets (a,b)) . n by A14, A13, XXREAL_1:43; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: [.a,b.] c= (half_open_sets (a,b)) . n
then consider k being Nat such that
A15: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A16: (half_open_sets (a,b)) . (k + 1) = halfline_fin (a,(b + (1 / (k + 1)))) by Def1;
b < b + (1 / n) by A15, XREAL_1:29;
hence [.a,b.] c= (half_open_sets (a,b)) . n by A16, A15, XXREAL_1:43; ::_thesis: verum
end;
end;
end;
hence c in (half_open_sets (a,b)) . n by A12; ::_thesis: verum
end;
hence ( c in [.a,b.] implies c in Intersection (half_open_sets (a,b)) ) by PROB_1:13; ::_thesis: verum
end;
for c being set holds
( c in Intersection (half_open_sets (a,b)) iff c in [.a,b.] ) by A11, A1;
hence Intersection (half_open_sets (a,b)) = [.a,b.] by TARSKI:1; ::_thesis: verum
end;
theorem :: FINANCE1:7
for a, b being real number
for n being Nat holds (Partial_Intersection (half_open_sets (a,b))) . n is Element of Borel_Sets
proof
let a, b be real number ; ::_thesis: for n being Nat holds (Partial_Intersection (half_open_sets (a,b))) . n is Element of Borel_Sets
defpred S1[ Nat] means (Partial_Intersection (half_open_sets (a,b))) . $1 is Element of Borel_Sets ;
A1: S1[ 0 ]
proof
(Partial_Intersection (half_open_sets (a,b))) . 0 = (half_open_sets (a,b)) . 0 by PROB_3:def_1;
then (Partial_Intersection (half_open_sets (a,b))) . 0 = halfline_fin (a,(b + 1)) by Def1;
hence S1[ 0 ] by Th4; ::_thesis: verum
end;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: (Partial_Intersection (half_open_sets (a,b))) . k is Element of Borel_Sets ; ::_thesis: S1[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def_12;
(Partial_Intersection (half_open_sets (a,b))) . (k + 1) = ((Partial_Intersection (half_open_sets (a,b))) . k) /\ ((half_open_sets (a,b)) . (k + 1)) by PROB_3:def_1;
then A4: (Partial_Intersection (half_open_sets (a,b))) . (k + 1) = ((Partial_Intersection (half_open_sets (a,b))) . k) /\ (halfline_fin (a,(b + (1 / (k + 1))))) by Def1;
( [.a,(b + (1 / (k + 1))).[ is Element of Borel_Sets & (Partial_Intersection (half_open_sets (a,b))) . k is Element of Borel_Sets ) by Th4, A3;
hence S1[k + 1] by A4, FINSUB_1:def_2; ::_thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2);
hence for n being Nat holds (Partial_Intersection (half_open_sets (a,b))) . n is Element of Borel_Sets ; ::_thesis: verum
end;
theorem Th8: :: FINANCE1:8
for k1, k2 being real number holds [.k2,k1.] is Element of Borel_Sets
proof
let a, b be real number ; ::_thesis: [.b,a.] is Element of Borel_Sets
Intersection (half_open_sets (b,a)) = [.b,a.] by Th6;
hence [.b,a.] is Element of Borel_Sets by Th5; ::_thesis: verum
end;
theorem Th9: :: FINANCE1:9
for Omega being non empty set
for Sigma being SigmaField of Omega
for X being Function of Omega,REAL st X is_random_variable_on Sigma, Borel_Sets holds
( ( for k being real number holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being real number st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being real number st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being real number holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being real number holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being real number holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being real number holds eq_dom (X,r) is Element of Sigma ) )
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for X being Function of Omega,REAL st X is_random_variable_on Sigma, Borel_Sets holds
( ( for k being real number holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being real number st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being real number st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being real number holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being real number holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being real number holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being real number holds eq_dom (X,r) is Element of Sigma ) )
let Sigma be SigmaField of Omega; ::_thesis: for X being Function of Omega,REAL st X is_random_variable_on Sigma, Borel_Sets holds
( ( for k being real number holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being real number st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being real number st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being real number holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being real number holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being real number holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being real number holds eq_dom (X,r) is Element of Sigma ) )
let X be Function of Omega,REAL; ::_thesis: ( X is_random_variable_on Sigma, Borel_Sets implies ( ( for k being real number holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being real number st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being real number st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being real number holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being real number holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being real number holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being real number holds eq_dom (X,r) is Element of Sigma ) ) )
assume A1: X is_random_variable_on Sigma, Borel_Sets ; ::_thesis: ( ( for k being real number holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being real number st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being real number st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being real number holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being real number holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being real number holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being real number holds eq_dom (X,r) is Element of Sigma ) )
A2: for k being real number holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma )
proof
let k be real number ; ::_thesis: ( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma )
A3: for q being set holds
( ex w being Element of Omega st
( q = w & X . w >= k ) iff ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) )
proof
let q be set ; ::_thesis: ( ex w being Element of Omega st
( q = w & X . w >= k ) iff ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) )
now__::_thesis:_(_ex_w_being_Element_of_Omega_st_
(_q_=_w_&_X_._w_in_[.k,+infty.]_)_implies_ex_w_being_Element_of_Omega_st_
(_q_=_w_&_X_._w_>=_k_)_)
assume ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) ; ::_thesis: ex w being Element of Omega st
( q = w & X . w >= k )
then consider w being Element of Omega such that
A4: ( q = w & X . w in [.k,+infty.] ) ;
X . w in { z where z is Element of ExtREAL : ( k <= z & z <= +infty ) } by A4, XXREAL_1:def_1;
then ex z being Element of ExtREAL st
( X . w = z & k <= z & z <= +infty ) ;
hence ex w being Element of Omega st
( q = w & X . w >= k ) by A4; ::_thesis: verum
end;
hence ( ex w being Element of Omega st
( q = w & X . w >= k ) iff ex w being Element of Omega st
( q = w & X . w in [.k,+infty.] ) ) by XXREAL_1:219; ::_thesis: verum
end;
A5: for x being set holds
( x in { w where w is Element of Omega : X . w >= k } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } )
proof
let x be set ; ::_thesis: ( x in { w where w is Element of Omega : X . w >= k } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } )
( x in { w where w is Element of Omega : X . w >= k } iff ex w being Element of Omega st
( x = w & X . w >= k ) ) ;
then A6: ( x in { w where w is Element of Omega : X . w >= k } iff ex w being Element of Omega st
( x = w & X . w in [.k,+infty.] ) ) by A3;
( x in { w where w is Element of Omega : X . w in [.k,+infty.] } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } )
proof
hereby ::_thesis: ( x in { w where w is Element of Omega : X . w in [.k,+infty.[ } implies x in { w where w is Element of Omega : X . w in [.k,+infty.] } )
assume x in { w where w is Element of Omega : X . w in [.k,+infty.] } ; ::_thesis: x in { g where g is Element of Omega : X . g in [.k,+infty.[ }
then consider w being Element of Omega such that
A7: ( w = x & X . w in [.k,+infty.] ) ;
X . w in { a where a is Element of ExtREAL : ( k <= a & a <= +infty ) } by A7, XXREAL_1:def_1;
then consider a being Element of ExtREAL such that
A8: ( X . w = a & k <= a & a <= +infty ) ;
A9: ( X . w = a & k <= a & a < +infty ) by A8, XXREAL_0:9;
{ z where z is Element of ExtREAL : ( k <= z & z < +infty ) } = [.k,+infty.[ by XXREAL_1:def_2;
then X . w in [.k,+infty.[ by A9;
hence x in { g where g is Element of Omega : X . g in [.k,+infty.[ } by A7; ::_thesis: verum
end;
assume x in { w where w is Element of Omega : X . w in [.k,+infty.[ } ; ::_thesis: x in { w where w is Element of Omega : X . w in [.k,+infty.] }
then consider w being Element of Omega such that
A10: ( w = x & X . w in [.k,+infty.[ ) ;
( w = x & X . w in { u where u is Element of ExtREAL : ( k <= u & u < +infty ) } ) by A10, XXREAL_1:def_2;
then ( w = x & ex u being Element of ExtREAL st
( u = X . w & k <= u & u < +infty ) ) ;
then ( w = x & X . w in { u where u is Element of ExtREAL : ( k <= u & u <= +infty ) } ) ;
then ( w = x & X . w in [.k,+infty.] ) by XXREAL_1:def_1;
hence x in { w where w is Element of Omega : X . w in [.k,+infty.] } ; ::_thesis: verum
end;
hence ( x in { w where w is Element of Omega : X . w >= k } iff x in { w where w is Element of Omega : X . w in [.k,+infty.[ } ) by A6; ::_thesis: verum
end;
k in REAL by XREAL_0:def_1;
then A11: not [.k,+infty.[ is empty by XXREAL_0:9, XXREAL_1:31;
A12: { w where w is Element of Omega : X . w >= k } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ }
proof
{ w where w is Element of Omega : X . w in [.k,+infty.[ } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ }
proof
for x being set holds
( x in { w where w is Element of Omega : X . w in [.k,+infty.[ } iff x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } )
proof
let x be set ; ::_thesis: ( x in { w where w is Element of Omega : X . w in [.k,+infty.[ } iff x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } )
hereby ::_thesis: ( x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } implies x in { w where w is Element of Omega : X . w in [.k,+infty.[ } )
assume x in { w where w is Element of Omega : X . w in [.k,+infty.[ } ; ::_thesis: x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ }
then ex w being Element of Omega st
( w = x & X . w in [.k,+infty.[ ) ;
hence x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } ; ::_thesis: verum
end;
assume x in { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } ; ::_thesis: x in { w where w is Element of Omega : X . w in [.k,+infty.[ }
then consider w being Element of Omega such that
A13: ( w = x & X . w is Element of [.k,+infty.[ ) ;
thus x in { w where w is Element of Omega : X . w in [.k,+infty.[ } by A13, A11; ::_thesis: verum
end;
hence { w where w is Element of Omega : X . w in [.k,+infty.[ } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } by TARSKI:1; ::_thesis: verum
end;
hence { w where w is Element of Omega : X . w >= k } = { w where w is Element of Omega : X . w is Element of [.k,+infty.[ } by A5, TARSKI:1; ::_thesis: verum
end;
A14: ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets ) by Th3;
A15: for q being set holds
( ex w being Element of Omega st
( q = w & X . w < k ) iff ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) )
proof
let q be set ; ::_thesis: ( ex w being Element of Omega st
( q = w & X . w < k ) iff ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) )
now__::_thesis:_(_ex_w_being_Element_of_Omega_st_
(_q_=_w_&_X_._w_in_[.-infty,k.[_)_implies_ex_w_being_Element_of_Omega_st_
(_q_=_w_&_X_._w_<_k_)_)
assume ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) ; ::_thesis: ex w being Element of Omega st
( q = w & X . w < k )
then consider w being Element of Omega such that
A16: ( q = w & X . w in [.-infty,k.[ ) ;
X . w in { z where z is Element of ExtREAL : ( -infty <= z & z < k ) } by A16, XXREAL_1:def_2;
then ex z being Element of ExtREAL st
( X . w = z & -infty <= z & z < k ) ;
hence ex w being Element of Omega st
( q = w & X . w < k ) by A16; ::_thesis: verum
end;
hence ( ex w being Element of Omega st
( q = w & X . w < k ) iff ex w being Element of Omega st
( q = w & X . w in [.-infty,k.[ ) ) by XXREAL_1:221; ::_thesis: verum
end;
for x being set holds
( x in { w where w is Element of Omega : X . w < k } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } )
proof
let x be set ; ::_thesis: ( x in { w where w is Element of Omega : X . w < k } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } )
( x in { w where w is Element of Omega : X . w < k } iff ex w being Element of Omega st
( x = w & X . w < k ) ) ;
then A17: ( x in { w where w is Element of Omega : X . w < k } iff ex w being Element of Omega st
( x = w & X . w in [.-infty,k.[ ) ) by A15;
( x in { w where w is Element of Omega : X . w in [.-infty,k.[ } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } )
proof
hereby ::_thesis: ( x in { w where w is Element of Omega : X . w in ].-infty,k.[ } implies x in { w where w is Element of Omega : X . w in [.-infty,k.[ } )
assume x in { w where w is Element of Omega : X . w in [.-infty,k.[ } ; ::_thesis: x in { g where g is Element of Omega : X . g in ].-infty,k.[ }
then consider w being Element of Omega such that
A18: ( w = x & X . w in [.-infty,k.[ ) ;
X . w in { a where a is Element of ExtREAL : ( -infty <= a & a < k ) } by A18, XXREAL_1:def_2;
then consider a being Element of ExtREAL such that
A19: ( X . w = a & -infty <= a & a < k ) ;
A20: ( X . w = a & -infty < a & a < k ) by A19, XXREAL_0:12;
{ z where z is Element of ExtREAL : ( -infty < z & z < k ) } = ].-infty,k.[ by XXREAL_1:def_4;
then X . w in ].-infty,k.[ by A20;
hence x in { g where g is Element of Omega : X . g in ].-infty,k.[ } by A18; ::_thesis: verum
end;
assume x in { w where w is Element of Omega : X . w in ].-infty,k.[ } ; ::_thesis: x in { w where w is Element of Omega : X . w in [.-infty,k.[ }
then consider w being Element of Omega such that
A21: ( w = x & X . w in ].-infty,k.[ ) ;
( w = x & X . w in { u where u is Element of ExtREAL : ( -infty < u & u < k ) } ) by A21, XXREAL_1:def_4;
then ( w = x & ex u being Element of ExtREAL st
( u = X . w & -infty < u & u < k ) ) ;
then ( w = x & X . w in { u where u is Element of ExtREAL : ( -infty <= u & u < k ) } ) ;
then ( w = x & X . w in [.-infty,k.[ ) by XXREAL_1:def_2;
hence x in { w where w is Element of Omega : X . w in [.-infty,k.[ } ; ::_thesis: verum
end;
hence ( x in { w where w is Element of Omega : X . w < k } iff x in { w where w is Element of Omega : X . w in ].-infty,k.[ } ) by A17; ::_thesis: verum
end;
then A22: { w where w is Element of Omega : X . w < k } = { w where w is Element of Omega : X . w in ].-infty,k.[ } by TARSKI:1;
{ w where w is Element of Omega : X . w < k } is Element of Sigma
proof
A23: ( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets ) by Th3;
k in REAL by XREAL_0:def_1;
then A24: not ].-infty,k.[ is empty by XXREAL_0:12, XXREAL_1:33;
for x being set holds
( x in { w where w is Element of Omega : X . w in ].-infty,k.[ } iff x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } )
proof
let x be set ; ::_thesis: ( x in { w where w is Element of Omega : X . w in ].-infty,k.[ } iff x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } )
hereby ::_thesis: ( x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } implies x in { w where w is Element of Omega : X . w in ].-infty,k.[ } )
assume x in { w where w is Element of Omega : X . w in ].-infty,k.[ } ; ::_thesis: x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ }
then ex w being Element of Omega st
( w = x & X . w in ].-infty,k.[ ) ;
hence x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } ; ::_thesis: verum
end;
assume x in { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } ; ::_thesis: x in { w where w is Element of Omega : X . w in ].-infty,k.[ }
then consider w being Element of Omega such that
A25: ( w = x & X . w is Element of ].-infty,k.[ ) ;
thus x in { w where w is Element of Omega : X . w in ].-infty,k.[ } by A25, A24; ::_thesis: verum
end;
then { w where w is Element of Omega : X . w < k } = { w where w is Element of Omega : X . w is Element of ].-infty,k.[ } by A22, TARSKI:1;
hence { w where w is Element of Omega : X . w < k } is Element of Sigma by A23, A1, Def5; ::_thesis: verum
end;
hence ( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) by A14, A1, Def5, A12; ::_thesis: verum
end;
A26: for k1, k2 being real number st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma
proof
let k1, k2 be real number ; ::_thesis: ( k1 < k2 implies { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma )
assume A27: k1 < k2 ; ::_thesis: { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma
proof
for x being set holds
( x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } iff x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } )
proof
let x be set ; ::_thesis: ( x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } iff x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } )
hereby ::_thesis: ( x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } implies x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } )
assume x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } ; ::_thesis: x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.[ }
then consider w being Element of Omega such that
A28: ( x = w & k1 <= X . w & X . w < k2 ) ;
consider a being Element of ExtREAL such that
A29: a = R_EAL (X . w) ;
a = X . w by A29, MEASURE6:def_1;
then X . w in { z where z is Element of ExtREAL : ( k1 <= z & z < k2 ) } by A28;
then X . w is Element of [.k1,k2.[ by XXREAL_1:def_2;
hence x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.[ } by A28; ::_thesis: verum
end;
assume x in { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } ; ::_thesis: x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) }
then consider w being Element of Omega such that
A30: ( x = w & X . w is Element of [.k1,k2.[ ) ;
A31: not [.k1,k2.[ is empty by A27, XXREAL_1:31;
X . w in [.k1,k2.[ by A30, A31;
then X . w in { a where a is Element of ExtREAL : ( k1 <= a & a < k2 ) } by XXREAL_1:def_2;
then ex a being Element of ExtREAL st
( a = X . w & k1 <= a & a < k2 ) ;
hence x in { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } by A30; ::_thesis: verum
end;
then A32: { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } = { w where w is Element of Omega : X . w is Element of [.k1,k2.[ } by TARSKI:1;
( [.k2,k1.[ is Element of Borel_Sets & [.k1,k2.[ is Element of Borel_Sets ) by Th4;
hence { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma by A1, Def5, A32; ::_thesis: verum
end;
hence { w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ; ::_thesis: verum
end;
A33: for k1, k2 being real number st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma
proof
let k1, k2 be real number ; ::_thesis: ( k1 <= k2 implies { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma )
assume A34: k1 <= k2 ; ::_thesis: { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma
for x being set holds
( x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } iff x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] } )
proof
let x be set ; ::_thesis: ( x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } iff x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] } )
hereby ::_thesis: ( x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] } implies x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } )
assume x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } ; ::_thesis: x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.] }
then consider w being Element of Omega such that
A35: ( x = w & k1 <= X . w & X . w <= k2 ) ;
consider a being Element of ExtREAL such that
A36: a = R_EAL (X . w) ;
a = X . w by A36, MEASURE6:def_1;
then X . w in { z where z is Element of ExtREAL : ( k1 <= z & z <= k2 ) } by A35;
then X . w is Element of [.k1,k2.] by XXREAL_1:def_1;
hence x in { w1 where w1 is Element of Omega : X . w1 is Element of [.k1,k2.] } by A35; ::_thesis: verum
end;
assume x in { w where w is Element of Omega : X . w is Element of [.k1,k2.] } ; ::_thesis: x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) }
then consider w being Element of Omega such that
A37: ( x = w & X . w is Element of [.k1,k2.] ) ;
A38: not [.k1,k2.] is empty by A34, XXREAL_1:30;
X . w in [.k1,k2.] by A37, A38;
then X . w in { a where a is Element of ExtREAL : ( k1 <= a & a <= k2 ) } by XXREAL_1:def_1;
then ex a being Element of ExtREAL st
( a = X . w & k1 <= a & a <= k2 ) ;
hence x in { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } by A37; ::_thesis: verum
end;
then A39: { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } = { w where w is Element of Omega : X . w is Element of [.k1,k2.] } by TARSKI:1;
( [.k1,k2.[ is Element of Borel_Sets & [.k1,k2.] is Element of Borel_Sets ) by Th8, Th4;
hence { w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma by A1, Def5, A39; ::_thesis: verum
end;
A40: for r being real number holds less_dom (X,r) = { w where w is Element of Omega : X . w < r }
proof
let r be real number ; ::_thesis: less_dom (X,r) = { w where w is Element of Omega : X . w < r }
for x being set holds
( x in less_dom (X,r) iff x in { w where w is Element of Omega : X . w < r } )
proof
let x be set ; ::_thesis: ( x in less_dom (X,r) iff x in { w where w is Element of Omega : X . w < r } )
( x in less_dom (X,r) iff ( x in dom X & X . x < r ) ) by MESFUNC1:def_11;
then ( x in less_dom (X,r) iff ( x in Omega & X . x < r ) ) by FUNCT_2:def_1;
then ( x in less_dom (X,r) iff ex q being Element of Omega st
( q = x & X . q < r ) ) ;
hence ( x in less_dom (X,r) iff x in { w where w is Element of Omega : X . w < r } ) ; ::_thesis: verum
end;
hence less_dom (X,r) = { w where w is Element of Omega : X . w < r } by TARSKI:1; ::_thesis: verum
end;
A41: for r being real number holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r }
proof
let r be real number ; ::_thesis: great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r }
for x being set holds
( x in great_eq_dom (X,r) iff x in { w where w is Element of Omega : X . w >= r } )
proof
let x be set ; ::_thesis: ( x in great_eq_dom (X,r) iff x in { w where w is Element of Omega : X . w >= r } )
( x in great_eq_dom (X,r) iff ( x in dom X & X . x >= r ) ) by MESFUNC1:def_14;
then ( x in great_eq_dom (X,r) iff ( x in Omega & X . x >= r ) ) by FUNCT_2:def_1;
then ( x in great_eq_dom (X,r) iff ex q being Element of Omega st
( q = x & X . q >= r ) ) ;
hence ( x in great_eq_dom (X,r) iff x in { w where w is Element of Omega : X . w >= r } ) ; ::_thesis: verum
end;
hence great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } by TARSKI:1; ::_thesis: verum
end;
A42: for r being real number holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r }
proof
let r be real number ; ::_thesis: eq_dom (X,r) = { w where w is Element of Omega : X . w = r }
for x being set holds
( x in eq_dom (X,r) iff x in { w where w is Element of Omega : X . w = r } )
proof
let x be set ; ::_thesis: ( x in eq_dom (X,r) iff x in { w where w is Element of Omega : X . w = r } )
( x in eq_dom (X,r) iff ( x in dom X & X . x = r ) ) by MESFUNC1:def_15;
then ( x in eq_dom (X,r) iff ( x in Omega & X . x = r ) ) by FUNCT_2:def_1;
then ( x in eq_dom (X,r) iff ex q being Element of Omega st
( q = x & X . q = r ) ) ;
hence ( x in eq_dom (X,r) iff x in { w where w is Element of Omega : X . w = r } ) ; ::_thesis: verum
end;
hence eq_dom (X,r) = { w where w is Element of Omega : X . w = r } by TARSKI:1; ::_thesis: verum
end;
for r being real number holds eq_dom (X,r) is Element of Sigma
proof
let r be real number ; ::_thesis: eq_dom (X,r) is Element of Sigma
for x being set holds
( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff x in { w where w is Element of Omega : X . w = r } )
proof
let x be set ; ::_thesis: ( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff x in { w where w is Element of Omega : X . w = r } )
( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff ex q being Element of Omega st
( x = q & r <= X . q & X . q <= r ) ) ;
then ( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff ex q being Element of Omega st
( x = q & X . q = r ) ) by XXREAL_0:1;
hence ( x in { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } iff x in { w where w is Element of Omega : X . w = r } ) ; ::_thesis: verum
end;
then { w where w is Element of Omega : ( r <= X . w & X . w <= r ) } = { w where w is Element of Omega : X . w = r } by TARSKI:1;
then { w where w is Element of Omega : X . w = r } is Element of Sigma by A33;
hence eq_dom (X,r) is Element of Sigma by A42; ::_thesis: verum
end;
hence ( ( for k being real number holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being real number st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being real number st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being real number holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being real number holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being real number holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being real number holds eq_dom (X,r) is Element of Sigma ) ) by A2, A26, A33, A40, A41, A42; ::_thesis: verum
end;
theorem :: FINANCE1:10
for Omega being non empty set
for Sigma being SigmaField of Omega
for s being real number holds Omega --> s is_random_variable_on Sigma, Borel_Sets
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for s being real number holds Omega --> s is_random_variable_on Sigma, Borel_Sets
let Sigma be SigmaField of Omega; ::_thesis: for s being real number holds Omega --> s is_random_variable_on Sigma, Borel_Sets
let s be real number ; ::_thesis: Omega --> s is_random_variable_on Sigma, Borel_Sets
set X = Omega --> s;
Omega --> s is_random_variable_on Sigma, Borel_Sets
proof
let x be Element of Borel_Sets ; :: according to FINANCE1:def_5 ::_thesis: { y where y is Element of Omega : (Omega --> s) . y is Element of x } is Element of Sigma
percases ( s is Element of x or not s is Element of x ) ;
supposeA1: s is Element of x ; ::_thesis: { y where y is Element of Omega : (Omega --> s) . y is Element of x } is Element of Sigma
for q being set holds
( q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } iff q in Omega )
proof
let q be set ; ::_thesis: ( q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } iff q in Omega )
hereby ::_thesis: ( q in Omega implies q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } )
assume q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } ; ::_thesis: q in Omega
then ex w being Element of Omega st
( w = q & (Omega --> s) . w is Element of x ) ;
hence q in Omega ; ::_thesis: verum
end;
assume q in Omega ; ::_thesis: q in { w where w is Element of Omega : (Omega --> s) . w is Element of x }
then reconsider w = q as Element of Omega ;
(Omega --> s) . w is Element of x by A1, FUNCOP_1:7;
hence q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } ; ::_thesis: verum
end;
then { w where w is Element of Omega : (Omega --> s) . w is Element of x } = Omega by TARSKI:1;
hence { y where y is Element of Omega : (Omega --> s) . y is Element of x } is Element of Sigma by PROB_1:23; ::_thesis: verum
end;
supposeA2: s is not Element of x ; ::_thesis: { y where y is Element of Omega : (Omega --> s) . y is Element of x } is Element of Sigma
for q being set holds
( q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } iff q in {} )
proof
let q be set ; ::_thesis: ( q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } iff q in {} )
now__::_thesis:_(_q_in__{__w_where_w_is_Element_of_Omega_:_(Omega_-->_s)_._w_is_Element_of_x__}__implies_q_in_{}_)
assume q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } ; ::_thesis: q in {}
then consider w being Element of Omega such that
A3: ( w = q & (Omega --> s) . w is Element of x ) ;
thus q in {} by A2, A3, FUNCOP_1:7; ::_thesis: verum
end;
hence ( q in { w where w is Element of Omega : (Omega --> s) . w is Element of x } iff q in {} ) ; ::_thesis: verum
end;
then { w where w is Element of Omega : (Omega --> s) . w is Element of x } = {} by TARSKI:1;
hence { y where y is Element of Omega : (Omega --> s) . y is Element of x } is Element of Sigma by PROB_1:22; ::_thesis: verum
end;
end;
end;
hence Omega --> s is_random_variable_on Sigma, Borel_Sets ; ::_thesis: verum
end;
theorem Th11: :: FINANCE1:11
for phi being Real_Sequence
for jpi being pricefunction
for d being Nat st d > 0 holds
BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d))
proof
let phi be Real_Sequence; ::_thesis: for jpi being pricefunction
for d being Nat st d > 0 holds
BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d))
let jpi be pricefunction ; ::_thesis: for d being Nat st d > 0 holds
BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d))
let d be Nat; ::_thesis: ( d > 0 implies BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d)) )
assume d > 0 ; ::_thesis: BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d))
then A1: d - 1 is Element of NAT by NAT_1:20;
defpred S1[ Nat] means (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . ($1 + 1) = (phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . $1);
(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = (phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0)
proof
(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = ((Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . 0) + ((ElementsOfBuyPortfolio (phi,jpi)) . 1) by SERIES_1:def_1;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = ((ElementsOfBuyPortfolio (phi,jpi)) . 0) + ((ElementsOfBuyPortfolio (phi,jpi)) . 1) by SERIES_1:def_1;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = ((ElementsOfBuyPortfolio (phi,jpi)) . 0) + (((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1) . 0) by NAT_1:def_3;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = ((ElementsOfBuyPortfolio (phi,jpi)) . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0) by SERIES_1:def_1;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = ((phi . 0) * (jpi . 0)) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0) by VALUED_1:5;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = ((phi . 0) * 1) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0) by Def2;
hence (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (0 + 1) = (phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . 0) ; ::_thesis: verum
end;
then A2: S1[ 0 ] ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . (k + 1) = (phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k) ; ::_thesis: S1[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def_12;
(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . ((k + 1) + 1) = ((phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k)) + ((ElementsOfBuyPortfolio (phi,jpi)) . ((k + 1) + 1)) by A4, SERIES_1:def_1;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . ((k + 1) + 1) = ((phi . 0) + ((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k)) + (((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1) . (k + 1)) by NAT_1:def_3;
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . ((k + 1) + 1) = (phi . 0) + (((Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . k) + (((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1) . (k + 1))) ;
hence S1[k + 1] by SERIES_1:def_1; ::_thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch_2(A2, A3);
then (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . ((d - 1) + 1) = (phi . 0) + (BuyPortfolio (phi,jpi,d)) by A1;
hence BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d)) ; ::_thesis: verum
end;
theorem Th12: :: FINANCE1:12
for Omega being non empty set
for F being SigmaField of Omega
for d being Nat st d > 0 holds
for r being real number
for phi being Real_Sequence
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
proof
let Omega be non empty set ; ::_thesis: for F being SigmaField of Omega
for d being Nat st d > 0 holds
for r being real number
for phi being Real_Sequence
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
let F be SigmaField of Omega; ::_thesis: for d being Nat st d > 0 holds
for r being real number
for phi being Real_Sequence
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
let d be Nat; ::_thesis: ( d > 0 implies for r being real number
for phi being Real_Sequence
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w)) )
assume A1: d > 0 ; ::_thesis: for r being real number
for phi being Real_Sequence
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
let r be real number ; ::_thesis: for phi being Real_Sequence
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
let phi be Real_Sequence; ::_thesis: for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
set X = set_of_random_variables_on (F,Borel_Sets);
let G be Function of NAT,(set_of_random_variables_on (F,Borel_Sets)); ::_thesis: ( Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) implies for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w)) )
assume A2: Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) ; ::_thesis: for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
let w be Element of Omega; ::_thesis: PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
A3: d - 1 is Element of NAT by A1, NAT_1:20;
defpred S1[ Nat] means (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . ($1 + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . $1);
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (0 + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . 0)
proof
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (0 + 1) = ((Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . 0) + ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . 1) by SERIES_1:def_1;
then (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (0 + 1) = ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . 0) + ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . 1) by SERIES_1:def_1;
then (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (0 + 1) = ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . 0) + (((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1) . 0) by NAT_1:def_3;
then (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (0 + 1) = ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . 0) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . 0) by SERIES_1:def_1;
then consider d being Element of NAT such that
A4: ( d = 0 & (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (d + 1) = ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . d) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . d) ) ;
A5: (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (d + 1) = (((ElementsOfPortfolioValueProb_fut (F,(G . d))) . w) * (phi . d)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . d) by A4, Def10;
set g = G . d;
set g2 = Change_Element_to_Func (F,Borel_Sets,(G . d));
(Change_Element_to_Func (F,Borel_Sets,(G . d))) . w = 1 + r
proof
( Element_Of (F,Borel_Sets,G,0) = G . 0 & Change_Element_to_Func (F,Borel_Sets,(G . d)) = G . 0 & Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) ) by A2, Def9, Def7, A4;
hence (Change_Element_to_Func (F,Borel_Sets,(G . d))) . w = 1 + r by FUNCOP_1:7; ::_thesis: verum
end;
hence (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (0 + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . 0) by A4, A5, Def8; ::_thesis: verum
end;
then A6: S1[ 0 ] ;
A7: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A8: (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . (k + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k) ; ::_thesis: S1[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def_12;
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . ((k + 1) + 1) = (((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k)) + ((ElementsOfPortfolioValue_fut (phi,F,w,G)) . ((k + 1) + 1)) by A8, SERIES_1:def_1;
then (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . ((k + 1) + 1) = (((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k)) + (((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1) . (k + 1)) by NAT_1:def_3;
then (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . ((k + 1) + 1) = ((1 + r) * (phi . 0)) + (((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . k) + (((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1) . (k + 1))) ;
hence S1[k + 1] by SERIES_1:def_1; ::_thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch_2(A6, A7);
then (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . ((d - 1) + 1) = ((1 + r) * (phi . 0)) + ((Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1)) by A3;
hence PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w)) ; ::_thesis: verum
end;
theorem Th13: :: FINANCE1:13
for Omega being non empty set
for F being SigmaField of Omega
for d being Nat st d > 0 holds
for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
proof
let Omega be non empty set ; ::_thesis: for F being SigmaField of Omega
for d being Nat st d > 0 holds
for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
let F be SigmaField of Omega; ::_thesis: for d being Nat st d > 0 holds
for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
let d be Nat; ::_thesis: ( d > 0 implies for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) )
assume A1: d > 0 ; ::_thesis: for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
let r be real number ; ::_thesis: ( r > - 1 implies for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) )
assume A2: r > - 1 ; ::_thesis: for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
let phi be Real_Sequence; ::_thesis: for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
let jpi be pricefunction ; ::_thesis: for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) holds
for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
set X = set_of_random_variables_on (F,Borel_Sets);
let G be Function of NAT,(set_of_random_variables_on (F,Borel_Sets)); ::_thesis: ( Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) implies for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) )
assume A3: Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) ; ::_thesis: for w being Element of Omega st BuyPortfolioExt (phi,jpi,d) <= 0 holds
PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
let w be Element of Omega; ::_thesis: ( BuyPortfolioExt (phi,jpi,d) <= 0 implies PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) )
assume A4: BuyPortfolioExt (phi,jpi,d) <= 0 ; ::_thesis: PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
A5: (1 + r) * (BuyPortfolioExt (phi,jpi,d)) <= 0
proof
1 + r > 0 by A2, XREAL_1:62;
hence (1 + r) * (BuyPortfolioExt (phi,jpi,d)) <= 0 by A4; ::_thesis: verum
end;
((1 + r) * (BuyPortfolioExt (phi,jpi,d))) + ((PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolioExt (phi,jpi,d)))) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolioExt (phi,jpi,d))) by A5, XREAL_1:32;
then PortfolioValueFut (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * ((phi . 0) + (BuyPortfolio (phi,jpi,d)))) by A1, Th11;
then PortfolioValueFut (d,phi,F,G,w) <= ((PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))) - ((1 + r) * (phi . 0)) ;
then (PortfolioValueFut (d,phi,F,G,w)) + ((1 + r) * (phi . 0)) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) by XREAL_1:19;
hence PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) by A1, A3, Th12; ::_thesis: verum
end;
theorem :: FINANCE1:14
for Omega being non empty set
for F being SigmaField of Omega
for d being Nat st d > 0 holds
for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
proof
let Omega be non empty set ; ::_thesis: for F being SigmaField of Omega
for d being Nat st d > 0 holds
for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
let F be SigmaField of Omega; ::_thesis: for d being Nat st d > 0 holds
for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
let d be Nat; ::_thesis: ( d > 0 implies for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } ) )
assume A1: d > 0 ; ::_thesis: for r being real number st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
let r be real number ; ::_thesis: ( r > - 1 implies for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } ) )
assume A2: r > - 1 ; ::_thesis: for phi being Real_Sequence
for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
let phi be Real_Sequence; ::_thesis: for jpi being pricefunction
for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
let jpi be pricefunction ; ::_thesis: for G being Function of NAT,(set_of_random_variables_on (F,Borel_Sets)) st Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 holds
( { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
set X = set_of_random_variables_on (F,Borel_Sets);
let G be Function of NAT,(set_of_random_variables_on (F,Borel_Sets)); ::_thesis: ( Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) & BuyPortfolioExt (phi,jpi,d) <= 0 implies ( { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } ) )
assume A3: Element_Of (F,Borel_Sets,G,0) = Omega --> (1 + r) ; ::_thesis: ( not BuyPortfolioExt (phi,jpi,d) <= 0 or ( { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } ) )
assume A4: BuyPortfolioExt (phi,jpi,d) <= 0 ; ::_thesis: ( { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
A5: { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } or x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
assume x in { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } ; ::_thesis: x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) }
then consider w being Element of Omega such that
A6: ( x = w & PortfolioValueFutExt (d,phi,F,G,w) >= 0 ) ;
0 <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) by A1, A2, A3, A4, Th13, A6;
then 0 + ((1 + r) * (BuyPortfolio (phi,jpi,d))) <= PortfolioValueFut (d,phi,F,G,w) by XREAL_1:19;
hence x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } by A6; ::_thesis: verum
end;
{ w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } or x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
assume x in { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } ; ::_thesis: x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) }
then consider w being Element of Omega such that
A7: ( x = w & PortfolioValueFutExt (d,phi,F,G,w) > 0 ) ;
PortfolioValueFutExt (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d))) by A1, A2, A3, A4, Th13;
then 0 + ((1 + r) * (BuyPortfolio (phi,jpi,d))) < ((PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))) + ((1 + r) * (BuyPortfolio (phi,jpi,d))) by A7, XREAL_1:6;
hence x in { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } by A7; ::_thesis: verum
end;
hence ( { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } & { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } ) by A5; ::_thesis: verum
end;
theorem Th15: :: FINANCE1:15
for Omega being non empty set
for Sigma being SigmaField of Omega
for f being Function of Omega,REAL st f is_random_variable_on Sigma, Borel_Sets holds
( f is_measurable_on [#] Sigma & f is Real-Valued-Random-Variable of Sigma )
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega
for f being Function of Omega,REAL st f is_random_variable_on Sigma, Borel_Sets holds
( f is_measurable_on [#] Sigma & f is Real-Valued-Random-Variable of Sigma )
let Sigma be SigmaField of Omega; ::_thesis: for f being Function of Omega,REAL st f is_random_variable_on Sigma, Borel_Sets holds
( f is_measurable_on [#] Sigma & f is Real-Valued-Random-Variable of Sigma )
let f be Function of Omega,REAL; ::_thesis: ( f is_random_variable_on Sigma, Borel_Sets implies ( f is_measurable_on [#] Sigma & f is Real-Valued-Random-Variable of Sigma ) )
assume A1: f is_random_variable_on Sigma, Borel_Sets ; ::_thesis: ( f is_measurable_on [#] Sigma & f is Real-Valued-Random-Variable of Sigma )
A2: for r being Element of REAL holds Omega /\ (less_dom (f,r)) in Sigma
proof
let r be Element of REAL ; ::_thesis: Omega /\ (less_dom (f,r)) in Sigma
less_dom (f,r) = { w where w is Element of Omega : f . w < r } by A1, Th9;
then less_dom (f,r) is Element of Sigma by A1, Th9;
then less_dom (f,r) in Sigma ;
hence Omega /\ (less_dom (f,r)) in Sigma by XBOOLE_1:28; ::_thesis: verum
end;
A3: for r being real number holds ([#] Sigma) /\ (less_dom (f,r)) in Sigma
proof
let r be real number ; ::_thesis: ([#] Sigma) /\ (less_dom (f,r)) in Sigma
reconsider r = r as Element of REAL by XREAL_0:def_1;
([#] Sigma) /\ (less_dom (f,r)) in Sigma by A2;
hence ([#] Sigma) /\ (less_dom (f,r)) in Sigma ; ::_thesis: verum
end;
f is Real-Valued-Random-Variable of Sigma
proof
ex X being Element of Sigma st
( X = Omega & f is_measurable_on X )
proof
reconsider X = [#] Sigma as Element of Sigma ;
f is_measurable_on X by A3, MESFUNC6:12;
hence ex X being Element of Sigma st
( X = Omega & f is_measurable_on X ) ; ::_thesis: verum
end;
hence f is Real-Valued-Random-Variable of Sigma by RANDOM_1:def_2; ::_thesis: verum
end;
hence ( f is_measurable_on [#] Sigma & f is Real-Valued-Random-Variable of Sigma ) by A3, MESFUNC6:12; ::_thesis: verum
end;
theorem :: FINANCE1:16
for Omega being non empty set
for Sigma being SigmaField of Omega holds set_of_random_variables_on (Sigma,Borel_Sets) c= Real-Valued-Random-Variables-Set Sigma
proof
let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega holds set_of_random_variables_on (Sigma,Borel_Sets) c= Real-Valued-Random-Variables-Set Sigma
let Sigma be SigmaField of Omega; ::_thesis: set_of_random_variables_on (Sigma,Borel_Sets) c= Real-Valued-Random-Variables-Set Sigma
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in set_of_random_variables_on (Sigma,Borel_Sets) or x in Real-Valued-Random-Variables-Set Sigma )
assume x in set_of_random_variables_on (Sigma,Borel_Sets) ; ::_thesis: x in Real-Valued-Random-Variables-Set Sigma
then consider f being Function of Omega,REAL such that
A1: ( x = f & f is_random_variable_on Sigma, Borel_Sets ) ;
A2: ( f is_random_variable_on Sigma, Borel_Sets implies f is Real-Valued-Random-Variable of Sigma ) by Th15;
x in { q where q is Real-Valued-Random-Variable of Sigma : verum } by A2, A1;
hence x in Real-Valued-Random-Variables-Set Sigma by RANDOM_2:def_3; ::_thesis: verum
end;