:: 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;