:: by Peter Jaeger

::

:: Received July 10, 2014

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

registration

coherence

not REAL \ RAT is empty by Th5;

coherence

not REAL \ INT is empty by Th6;

coherence

not REAL \ NAT is empty by Th7;

end;
not REAL \ RAT is empty by Th5;

coherence

not REAL \ INT is empty by Th6;

coherence

not REAL \ NAT is empty by Th7;

definition

{ (right_closed_halfline r) where r is Element of REAL : verum } is Subset-Family of REAL
end;

func Family_of_halflines2 -> Subset-Family of REAL equals :: FINANCE2:def 1

{ (right_closed_halfline r) where r is Element of REAL : verum } ;

coherence { (right_closed_halfline r) where r is Element of REAL : verum } ;

{ (right_closed_halfline r) where r is Element of REAL : verum } is Subset-Family of REAL

proof end;

:: deftheorem defines Family_of_halflines2 FINANCE2:def 1 :

Family_of_halflines2 = { (right_closed_halfline r) where r is Element of REAL : verum } ;

Family_of_halflines2 = { (right_closed_halfline r) where r is Element of REAL : verum } ;

theorem :: FINANCE2:7

theorem :: FINANCE2:10

for A being SetSequence of NAT st ( for n being Nat holds A . n = {n} ) holds

for n being Nat holds (Partial_Union A) . n in Borel_Sets

for n being Nat holds (Partial_Union A) . n in Borel_Sets

proof end;

Q00: ex A1 being SetSequence of REAL st

for n being Nat holds A1 . n = {n}

proof end;

Q0: ex A being SetSequence of Borel_Sets st

for n being Nat holds A . n = {n}

proof end;

H2: ex A being SetSequence of REAL st

for n being Nat holds A . n = {(- n)}

proof end;

theorem ThA: :: FINANCE2:14

for AA being SetSequence of REAL ex A being SetSequence of REAL st

for n being Nat holds A . n = (Partial_Union AA) . n

for n being Nat holds A . n = (Partial_Union AA) . n

proof end;

definition

let k be Nat;

let pm be Element of REAL ;

ex b_{1} being SetSequence of REAL st

for n being Nat holds b_{1} . n = {((pm * k) * ((n + 1) "))}

for b_{1}, b_{2} being SetSequence of REAL st ( for n being Nat holds b_{1} . n = {((pm * k) * ((n + 1) "))} ) & ( for n being Nat holds b_{2} . n = {((pm * k) * ((n + 1) "))} ) holds

b_{1} = b_{2}

end;
let pm be Element of REAL ;

func GoCross_Seq_REAL (pm,k) -> SetSequence of REAL means :Def4: :: FINANCE2:def 2

for n being Nat holds it . n = {((pm * k) * ((n + 1) "))};

existence for n being Nat holds it . n = {((pm * k) * ((n + 1) "))};

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines GoCross_Seq_REAL FINANCE2:def 2 :

for k being Nat

for pm being Element of REAL

for b_{3} being SetSequence of REAL holds

( b_{3} = GoCross_Seq_REAL (pm,k) iff for n being Nat holds b_{3} . n = {((pm * k) * ((n + 1) "))} );

for k being Nat

for pm being Element of REAL

for b

( b

definition

let k be Nat;

let pm be Element of REAL ;

:: original: GoCross_Seq_REAL

redefine func GoCross_Seq_REAL (pm,k) -> SetSequence of Borel_Sets ;

correctness

coherence

GoCross_Seq_REAL (pm,k) is SetSequence of Borel_Sets ;

end;
let pm be Element of REAL ;

:: original: GoCross_Seq_REAL

redefine func GoCross_Seq_REAL (pm,k) -> SetSequence of Borel_Sets ;

correctness

coherence

GoCross_Seq_REAL (pm,k) is SetSequence of Borel_Sets ;

proof end;

registration
end;

theorem :: FINANCE2:16

for pm being Element of REAL

for k being Nat st k > 0 & pm <> 0 holds

GoCross_Seq_REAL (pm,k) is one-to-one

for k being Nat st k > 0 & pm <> 0 holds

GoCross_Seq_REAL (pm,k) is one-to-one

proof end;

definition

let k be Nat;

let pm be Element of REAL ;

ex b_{1} being SetSequence of REAL st

( b_{1} . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) )

for b_{1}, b_{2} being SetSequence of REAL st b_{1} . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) & b_{2} . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) holds

b_{1} = b_{2}

end;
let pm be Element of REAL ;

func GoCross_Partial_Union (pm,k) -> SetSequence of REAL means :Def5: :: FINANCE2:def 3

( it . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds it . (n + 1) = (it . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) );

existence ( it . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds it . (n + 1) = (it . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines GoCross_Partial_Union FINANCE2:def 3 :

for k being Nat

for pm being Element of REAL

for b_{3} being SetSequence of REAL holds

( b_{3} = GoCross_Partial_Union (pm,k) iff ( b_{3} . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds b_{3} . (n + 1) = (b_{3} . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) ) );

for k being Nat

for pm being Element of REAL

for b

( b

definition

let k be Nat;

let pm be Element of REAL ;

:: original: GoCross_Partial_Union

redefine func GoCross_Partial_Union (pm,k) -> SetSequence of Borel_Sets ;

correctness

coherence

GoCross_Partial_Union (pm,k) is SetSequence of Borel_Sets ;

end;
let pm be Element of REAL ;

:: original: GoCross_Partial_Union

redefine func GoCross_Partial_Union (pm,k) -> SetSequence of Borel_Sets ;

correctness

coherence

GoCross_Partial_Union (pm,k) is SetSequence of Borel_Sets ;

proof end;

registration

let k be Nat;

let pm be Element of REAL ;

coherence

GoCross_Partial_Union (pm,k) is Borel_Sets -valued ;

end;
let pm be Element of REAL ;

coherence

GoCross_Partial_Union (pm,k) is Borel_Sets -valued ;

registration

let k be Nat;

let pm be Element of REAL ;

coherence

GoCross_Partial_Union (pm,k) is non-descending

end;
let pm be Element of REAL ;

coherence

GoCross_Partial_Union (pm,k) is non-descending

proof end;

definition

let pm be Element of REAL ;

ex b_{1} being SetSequence of REAL st

( b_{1} . 0 = Union (GoCross_Partial_Union (pm,0)) & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) )

for b_{1}, b_{2} being SetSequence of REAL st b_{1} . 0 = Union (GoCross_Partial_Union (pm,0)) & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) & b_{2} . 0 = Union (GoCross_Partial_Union (pm,0)) & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) holds

b_{1} = b_{2}

end;
func GoCross_Union pm -> SetSequence of REAL means :Def6: :: FINANCE2:def 4

( it . 0 = Union (GoCross_Partial_Union (pm,0)) & ( for n being Nat holds it . (n + 1) = (it . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) );

existence ( it . 0 = Union (GoCross_Partial_Union (pm,0)) & ( for n being Nat holds it . (n + 1) = (it . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines GoCross_Union FINANCE2:def 4 :

for pm being Element of REAL

for b_{2} being SetSequence of REAL holds

( b_{2} = GoCross_Union pm iff ( b_{2} . 0 = Union (GoCross_Partial_Union (pm,0)) & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) ) );

for pm being Element of REAL

for b

( b

definition

let pm be Element of REAL ;

:: original: GoCross_Union

redefine func GoCross_Union pm -> SetSequence of Borel_Sets ;

correctness

coherence

GoCross_Union pm is SetSequence of Borel_Sets ;

end;
:: original: GoCross_Union

redefine func GoCross_Union pm -> SetSequence of Borel_Sets ;

correctness

coherence

GoCross_Union pm is SetSequence of Borel_Sets ;

proof end;

registration
end;

theorem Th3: :: FINANCE2:17

for mym, myp being Element of REAL st mym = 1 & myp = - 1 holds

(Union (GoCross_Union mym)) \/ (Union (GoCross_Union myp)) = RAT

(Union (GoCross_Union mym)) \/ (Union (GoCross_Union myp)) = RAT

proof end;

:: Since the Borel-Sets can be constructed by different sets of intervals,

:: we show, that other sets can do this.

:: we show, that other sets can do this.

theorem :: FINANCE2:23

for Omega being non empty set

for Sigma being SigmaField of Omega

for X, Y being random_variable of Sigma, Borel_Sets holds X + Y is random_variable of Sigma, Borel_Sets

for Sigma being SigmaField of Omega

for X, Y being random_variable of Sigma, Borel_Sets holds X + Y is random_variable of Sigma, Borel_Sets

proof end;

theorem :: FINANCE2:24

for Omega being non empty set

for Sigma being SigmaField of Omega

for X, Y being random_variable of Sigma, Borel_Sets holds X - Y is random_variable of Sigma, Borel_Sets

for Sigma being SigmaField of Omega

for X, Y being random_variable of Sigma, Borel_Sets holds X - Y is random_variable of Sigma, Borel_Sets

proof end;

theorem :: FINANCE2:25

for Omega being non empty set

for Sigma being SigmaField of Omega

for X, Y being random_variable of Sigma, Borel_Sets holds X (#) Y is random_variable of Sigma, Borel_Sets

for Sigma being SigmaField of Omega

for X, Y being random_variable of Sigma, Borel_Sets holds X (#) Y is random_variable of Sigma, Borel_Sets

proof end;

theorem Th8: :: FINANCE2:26

for Omega being non empty set

for Sigma being SigmaField of Omega

for r being Real

for X being random_variable of Sigma, Borel_Sets holds r (#) X is random_variable of Sigma, Borel_Sets

for Sigma being SigmaField of Omega

for r being Real

for X being random_variable of Sigma, Borel_Sets holds r (#) X is random_variable of Sigma, Borel_Sets

proof end;

theorem T: :: FINANCE2:27

for Omega, Omega2 being non empty set

for F being SigmaField of Omega

for F2 being SigmaField of Omega2

for k being Element of set_of_random_variables_on (F,F2) holds Change_Element_to_Func (F,F2,k) is random_variable of F,F2

for F being SigmaField of Omega

for F2 being SigmaField of Omega2

for k being Element of set_of_random_variables_on (F,F2) holds Change_Element_to_Func (F,F2,k) is random_variable of F,F2

proof end;

theorem T1: :: FINANCE2:28

for Omega being non empty set

for F being SigmaField of Omega

for k being Element of set_of_random_variables_on (F,Borel_Sets) holds ElementsOfPortfolioValueProb_fut (F,k) is random_variable of F, Borel_Sets

for F being SigmaField of Omega

for k being Element of set_of_random_variables_on (F,Borel_Sets) holds ElementsOfPortfolioValueProb_fut (F,k) is random_variable of F, Borel_Sets

proof end;

theorem :: FINANCE2:29

for p being Nat

for Omega, Omega2 being non empty set

for F being SigmaField of Omega

for F2 being SigmaField of Omega2

for G being sequence of (set_of_random_variables_on (F,F2)) holds Element_Of (F,F2,G,p) is random_variable of F,F2

for Omega, Omega2 being non empty set

for F being SigmaField of Omega

for F2 being SigmaField of Omega2

for G being sequence of (set_of_random_variables_on (F,F2)) holds Element_Of (F,F2,G,p) is random_variable of F,F2

proof end;

definition

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 phi be Real_Sequence;

let n be Nat;

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

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

for b_{1}, b_{2} being Function of Omega,REAL st ( for w being Element of Omega holds b_{1} . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) & ( for w being Element of Omega holds b_{2} . w = ((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 G be sequence of X;

let phi be Real_Sequence;

let n be Nat;

func RVElementsOfPortfolioValue_fut (phi,F,G,n) -> Function of Omega,REAL means :Def5000: :: FINANCE2:def 5

for w being Element of Omega holds it . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n);

existence for w being Element of Omega holds it . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n);

ex b

for w being Element of Omega holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5000 defines RVElementsOfPortfolioValue_fut FINANCE2:def 5 :

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 phi being Real_Sequence

for n being Nat

for b_{7} being Function of Omega,REAL holds

( b_{7} = RVElementsOfPortfolioValue_fut (phi,F,G,n) iff for w being Element of Omega holds b_{7} . w = ((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 G being sequence of X

for phi being Real_Sequence

for n being Nat

for b

( b

theorem :: FINANCE2:30

for Omega being non empty set

for F being SigmaField of Omega

for G being sequence of (set_of_random_variables_on (F,Borel_Sets))

for phi being Real_Sequence

for n being Nat holds RVElementsOfPortfolioValue_fut (phi,F,G,n) is random_variable of F, Borel_Sets

for F being SigmaField of Omega

for G being sequence of (set_of_random_variables_on (F,Borel_Sets))

for phi being Real_Sequence

for n being Nat holds RVElementsOfPortfolioValue_fut (phi,F,G,n) is random_variable of F, Borel_Sets

proof end;

definition

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;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w ) & ( for n being Nat holds b_{2} . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w ) holds

b_{1} = b_{2}

end;
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 RVPortfolioValueFutExt_El (phi,F,G,w) -> Real_Sequence means :Def5001: :: FINANCE2:def 6

for n being Nat holds it . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w;

existence for n being Nat holds it . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5001 defines RVPortfolioValueFutExt_El FINANCE2:def 6 :

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

for b_{7} being Real_Sequence holds

( b_{7} = RVPortfolioValueFutExt_El (phi,F,G,w) iff for n being Nat holds b_{7} . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w );

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

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

coherence

PortfolioValueFutExt (d,phi,F,G,w) is Real;

compatibility

for b_{1} being Real holds

( b_{1} = PortfolioValueFutExt (d,phi,F,G,w) iff b_{1} = (Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . d );

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;

:: original: PortfolioValueFutExt

redefine func PortfolioValueFutExt (d,phi,F,G,w) -> Real equals :: FINANCE2:def 7

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

correctness redefine func PortfolioValueFutExt (d,phi,F,G,w) -> Real equals :: FINANCE2:def 7

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

coherence

PortfolioValueFutExt (d,phi,F,G,w) is Real;

compatibility

for b

( b

proof end;

:: deftheorem defines PortfolioValueFutExt FINANCE2:def 7 :

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

:: Event of the Borel-Sets