:: by Peter Jaeger

::

:: Received March 22, 2011

:: Copyright (c) 2011-2019 Association of Mizar Users

definition

let a, r be Real;

:: original: halfline_fin

redefine func halfline_fin (a,r) -> Subset of REAL;

coherence

halfline_fin (a,r) is Subset of REAL

end;
:: original: halfline_fin

redefine func halfline_fin (a,r) -> Subset of REAL;

coherence

halfline_fin (a,r) is Subset of REAL

proof end;

definition

let a, b be Real;

ex b_{1} being SetSequence of REAL st

( b_{1} . 0 = halfline_fin (a,(b + 1)) & ( for n being Nat holds b_{1} . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) )

for b_{1}, b_{2} being SetSequence of REAL st b_{1} . 0 = halfline_fin (a,(b + 1)) & ( for n being Nat holds b_{1} . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) & b_{2} . 0 = halfline_fin (a,(b + 1)) & ( for n being Nat holds b_{2} . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) holds

b_{1} = b_{2}

end;
func half_open_sets (a,b) -> SetSequence of REAL means :Def1: :: FINANCE1:def 1

( it . 0 = halfline_fin (a,(b + 1)) & ( for n being Nat holds it . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) );

existence ( it . 0 = halfline_fin (a,(b + 1)) & ( for n being Nat holds it . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines half_open_sets FINANCE1:def 1 :

for a, b being Real

for b_{3} being SetSequence of REAL holds

( b_{3} = half_open_sets (a,b) iff ( b_{3} . 0 = halfline_fin (a,(b + 1)) & ( for n being Nat holds b_{3} . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) ) );

for a, b being Real

for b

( b

definition

ex b_{1} being Real_Sequence st

( b_{1} . 0 = 1 & ( for n being Element of NAT holds b_{1} . n >= 0 ) )
end;

mode pricefunction -> Real_Sequence means :Def2: :: FINANCE1:def 2

( it . 0 = 1 & ( for n being Element of NAT holds it . n >= 0 ) );

existence ( it . 0 = 1 & ( for n being Element of NAT holds it . n >= 0 ) );

ex b

( b

proof end;

:: deftheorem Def2 defines pricefunction FINANCE1:def 2 :

for b_{1} being Real_Sequence holds

( b_{1} is pricefunction iff ( b_{1} . 0 = 1 & ( for n being Element of NAT holds b_{1} . n >= 0 ) ) );

for b

( b

notation
end;

definition

let phi, jpi be Real_Sequence;

:: original: ElementsOfBuyPortfolio

redefine func ElementsOfBuyPortfolio (phi,jpi) -> Real_Sequence;

coherence

ElementsOfBuyPortfolio (phi,jpi) is Real_Sequence

end;
:: original: ElementsOfBuyPortfolio

redefine func ElementsOfBuyPortfolio (phi,jpi) -> Real_Sequence;

coherence

ElementsOfBuyPortfolio (phi,jpi) is Real_Sequence

proof end;

definition

let d be Nat;

let phi, jpi be Real_Sequence;

(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . d is Real ;

(Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1) is Real ;

end;
let phi, jpi be Real_Sequence;

func BuyPortfolioExt (phi,jpi,d) -> Real equals :: FINANCE1:def 3

(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . d;

coherence (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . d;

(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . d is Real ;

func BuyPortfolio (phi,jpi,d) -> Real equals :: FINANCE1:def 4

(Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1);

coherence (Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1);

(Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1) is Real ;

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

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

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 of Omega,Omega2;

end;
let Sigma be SigmaField of Omega;

let Sigma2 be SigmaField of Omega2;

let X be Function of Omega,Omega2;

attr X is Sigma,Sigma2 -random_variable-like means :: FINANCE1:def 5

for x being set st x in Sigma2 holds

X " x in Sigma;

for x being set st x in Sigma2 holds

X " x in Sigma;

:: deftheorem defines -random_variable-like FINANCE1:def 5 :

for Omega, Omega2 being set

for Sigma being SigmaField of Omega

for Sigma2 being SigmaField of Omega2

for X being Function of Omega,Omega2 holds

( X is Sigma,Sigma2 -random_variable-like iff for x being set st x in Sigma2 holds

X " x in Sigma );

for Omega, Omega2 being set

for Sigma being SigmaField of Omega

for Sigma2 being SigmaField of Omega2

for X being Function of Omega,Omega2 holds

( X is Sigma,Sigma2 -random_variable-like iff for x being set st x in Sigma2 holds

X " x in Sigma );

Lm1: for Omega, Omega2 being non empty set

for F being Function of Omega,Omega2

for y being non empty set holds { z where z is Element of Omega : F . z is Element of y } = F " y

proof end;

LemmaExample: for Omega, Omega2 being non empty set

for F being SigmaField of Omega

for F2 being SigmaField of Omega2

for f being Function of Omega,Omega2 st f = Omega --> the Element of Omega2 holds

f is F,F2 -random_variable-like

proof end;

registration

let Omega1, Omega2 be non empty set ;

let S1 be SigmaField of Omega1;

let S2 be SigmaField of Omega2;

ex b_{1} being Function of Omega1,Omega2 st b_{1} is S1,S2 -random_variable-like

end;
let S1 be SigmaField of Omega1;

let S2 be SigmaField of Omega2;

cluster V1() V4(Omega1) V5(Omega2) non empty Function-like V28(Omega1) V32(Omega1,Omega2) S1,S2 -random_variable-like for Element of Trivial-SigmaField K17(Omega1,Omega2);

existence ex b

proof end;

definition

let Omega, Omega2 be non empty set ;

let F be SigmaField of Omega;

let F2 be SigmaField of Omega2;

mode random_variable of F,F2 is F,F2 -random_variable-like Function of Omega,Omega2;

end;
let F be SigmaField of Omega;

let F2 be SigmaField of Omega2;

mode random_variable of F,F2 is F,F2 -random_variable-like Function of Omega,Omega2;

definition

let Omega, Omega2 be set ;

let F be SigmaField of Omega;

let F2 be SigmaField of Omega2;

{ M where M is Function of Omega,Omega2 : M is F,F2 -random_variable-like } is set ;

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

{ M where M is Function of Omega,Omega2 : M is F,F2 -random_variable-like } ;

coherence { M where M is Function of Omega,Omega2 : M is F,F2 -random_variable-like } ;

{ M where M is Function of Omega,Omega2 : M is F,F2 -random_variable-like } is set ;

:: 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) = { M where M is Function of Omega,Omega2 : M is F,F2 -random_variable-like } ;

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) = { M where M is Function of Omega,Omega2 : M is F,F2 -random_variable-like } ;

registration

let Omega, Omega2 be non empty set ;

let F be SigmaField of Omega;

let F2 be SigmaField of Omega2;

coherence

not set_of_random_variables_on (F,F2) is empty

end;
let F be SigmaField of Omega;

let F2 be SigmaField of Omega2;

coherence

not set_of_random_variables_on (F,F2) is empty

proof end;

registration

let Omega, Omega2 be non empty set ;

let F be SigmaField of Omega;

let F2 be SigmaField of Omega2;

coherence

set_of_random_variables_on (F,F2) is functional

end;
let F be SigmaField of Omega;

let F2 be SigmaField of Omega2;

coherence

set_of_random_variables_on (F,F2) is functional

proof 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 A1: X = set_of_random_variables_on (F,F2) ;

let k be Element of X;

coherence

k is Function of Omega,Omega2

end;
let F be SigmaField of Omega;

let F2 be SigmaField of Omega2;

let X be set ;

assume A1: X = set_of_random_variables_on (F,F2) ;

let k be Element of X;

coherence

k is Function of Omega,Omega2

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

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;

ex b_{1} being Function of Omega,REAL st

for w being Element of Omega holds b_{1} . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w

for b_{1}, b_{2} being Function of Omega,REAL st ( for w being Element of Omega holds b_{1} . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ) & ( for w being Element of Omega holds b_{2} . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ) holds

b_{1} = b_{2}

end;
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 for w being Element of Omega holds it . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w;

ex b

for w being Element of Omega holds b

proof end;

uniqueness for b

b

proof 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 b_{5} being Function of Omega,REAL holds

( b_{5} = ElementsOfPortfolioValueProb_fut (F,k) iff for w being Element of Omega holds b_{5} . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w );

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 b

( b

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 A1: X = set_of_random_variables_on (F,F2) ;

let G be sequence of X;

coherence

G . p is Function of Omega,Omega2

end;
let Omega, Omega2 be non empty set ;

let F be SigmaField of Omega;

let F2 be SigmaField of Omega2;

let X be set ;

assume A1: X = set_of_random_variables_on (F,F2) ;

let G be sequence of X;

coherence

G . p is Function of Omega,Omega2

proof 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 sequence of X holds Element_Of (F,F2,G,p) = G . p;

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 sequence of 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 sequence of X;

let phi be Real_Sequence;

ex b_{1} being Real_Sequence st

for n being Element of NAT holds b_{1} . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n)

for b_{1}, b_{2} being Real_Sequence st ( for n being Element of NAT holds b_{1} . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) & ( for n being Element of NAT holds b_{2} . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) holds

b_{1} = b_{2}

end;
let F be SigmaField of Omega;

let X be non empty set ;

let w be Element of Omega;

let G be sequence of 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 for n being Element of NAT holds it . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n);

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof 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 sequence of X

for phi, b_{7} being Real_Sequence holds

( b_{7} = ElementsOfPortfolioValue_fut (phi,F,w,G) iff for n being Element of NAT holds b_{7} . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) );

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 sequence of X

for phi, b

( b

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 sequence of X;

let w be Element of Omega;

(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . d is Real ;

(Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1) is Real ;

end;
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 sequence of X;

let w be Element of Omega;

func PortfolioValueFutExt (d,phi,F,G,w) -> Real equals :: FINANCE1:def 11

(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . d;

coherence (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . d;

(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . d is Real ;

func PortfolioValueFut (d,phi,F,G,w) -> 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);

(Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1) is Real ;

:: 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 sequence of X

for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . d;

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 sequence of 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 sequence of 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);

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 sequence of 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
end;

theorem Th3: :: FINANCE1:3

for k being Real holds

( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets )

( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets )

proof end;

theorem :: FINANCE1:7

for a, b being Real

for n being Nat holds (Partial_Intersection (half_open_sets (a,b))) . n is Element of Borel_Sets

for n being Nat holds (Partial_Intersection (half_open_sets (a,b))) . n is Element of Borel_Sets

proof 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 Sigma, Borel_Sets -random_variable-like holds

( ( for k being Real 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 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 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 holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) )

for Sigma being SigmaField of Omega

for X being Function of Omega,REAL st X is Sigma, Borel_Sets -random_variable-like holds

( ( for k being Real 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 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 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 holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) )

proof end;

theorem :: FINANCE1:10

for Omega being non empty set

for Sigma being SigmaField of Omega

for s being Real

for f being Function of Omega,REAL st f = Omega --> s holds

f is Sigma, Borel_Sets -random_variable-like

for Sigma being SigmaField of Omega

for s being Real

for f being Function of Omega,REAL st f = Omega --> s holds

f is Sigma, Borel_Sets -random_variable-like

proof 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))

for jpi being pricefunction

for d being Nat st d > 0 holds

BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d))

proof 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

for phi being Real_Sequence

for G being sequence of (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))

for F being SigmaField of Omega

for d being Nat st d > 0 holds

for r being Real

for phi being Real_Sequence

for G being sequence of (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 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 st r > - 1 holds

for phi being Real_Sequence

for jpi being pricefunction

for G being sequence of (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)))

for F being SigmaField of Omega

for d being Nat st d > 0 holds

for r being Real st r > - 1 holds

for phi being Real_Sequence

for jpi being pricefunction

for G being sequence of (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 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 st r > - 1 holds

for phi being Real_Sequence

for jpi being pricefunction

for G being sequence of (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)) } )

for F being SigmaField of Omega

for d being Nat st d > 0 holds

for r being Real st r > - 1 holds

for phi being Real_Sequence

for jpi being pricefunction

for G being sequence of (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 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 Sigma, Borel_Sets -random_variable-like holds

( f is [#] Sigma -measurable & f is Real-Valued-Random-Variable of Sigma )

for Sigma being SigmaField of Omega

for f being Function of Omega,REAL st f is Sigma, Borel_Sets -random_variable-like holds

( f is [#] Sigma -measurable & f is Real-Valued-Random-Variable of Sigma )

proof 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

for Sigma being SigmaField of Omega holds set_of_random_variables_on (Sigma,Borel_Sets) c= Real-Valued-Random-Variables-Set Sigma

proof end;

theorem :: FINANCE1:17

for Omega, Omega2 being non empty set

for F being SigmaField of Omega

for F2 being SigmaField of Omega2 holds Omega --> the Element of Omega2 is random_variable of F,F2 by LemmaExample;

for F being SigmaField of Omega

for F2 being SigmaField of Omega2 holds Omega --> the Element of Omega2 is random_variable of F,F2 by LemmaExample;