:: Events of Borel Sets, Construction of Borel Sets and Random Variables for Stochastic Finance
:: by Peter Jaeger
::
:: Received July 10, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users

:: We start with some theorems which are necessary to prove, that IRRAT is an
:: Event of the Borel-Sets

theorem Ko1: :: FINANCE2:1

( 1 in REAL & - 1 in REAL )

proof end;

theorem Th5: :: FINANCE2:2

number_e in REAL \ RAT

proof end;

theorem Th6: :: FINANCE2:3

number_e in REAL \ INT

proof end;

theorem Th7: :: FINANCE2:4

number_e in REAL \ NAT

proof end;

registration

cluster REAL \ RAT -> non empty ;

coherence
not REAL \ RAT is empty by Th5;

cluster REAL \ INT -> non empty ;

coherence
not REAL \ INT is empty by Th6;

cluster REAL \ NAT -> non empty ;

coherence
not REAL \ NAT is empty by Th7;

end;

theorem Th1: :: FINANCE2:5

for k being Real holds {k} in Borel_Sets

proof end;

theorem :: FINANCE2:6

for k1, k2 being Real holds ].k1,k2.] is Event of Borel_Sets

proof end;

definition

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 } is Subset-Family of REAL

proof end;

end;

:: deftheorem defines Family_of_halflines2 FINANCE2:def 1 :
Family_of_halflines2 = { (right_closed_halfline r) where r is Element of REAL : verum } ;

theorem :: FINANCE2:7

for Exy being ExtReal holds {Exy} is Subset of ExtREAL by XXREAL_0:def 1, ZFMISC_1:31;

theorem :: FINANCE2:8

for Y being set
for k being Nat st Y = REAL \ {k} holds
Y is Event of Borel_Sets

proof end;

theorem :: FINANCE2:9

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

proof end;

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

proof end;

theorem :: FINANCE2:11

REAL is Event of 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 ZV5: :: FINANCE2:12

NAT is Event of Borel_Sets

proof end;

theorem :: FINANCE2:13

REAL \ NAT is Event of Borel_Sets

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

proof end;

theorem Th40: :: FINANCE2:15

INT is Event of Borel_Sets

proof end;

definition

let k be Nat;
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
ex b₁ being SetSequence of REAL st
for n being Nat holds b₁ . n = {((pm * k) * ((n + 1) "))}

proof end;

uniqueness
for b₁, b₂ being SetSequence of REAL st ( for n being Nat holds b₁ . n = {((pm * k) * ((n + 1) "))} ) & ( for n being Nat holds b₂ . n = {((pm * k) * ((n + 1) "))} ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines GoCross_Seq_REAL FINANCE2:def 2 :
for k being Nat
for pm being Element of REAL
for b₃ being SetSequence of REAL holds
( b₃ = GoCross_Seq_REAL (pm,k) iff for n being Nat holds b₃ . n = {((pm * k) * ((n + 1) "))} );

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 ;

proof end;

end;

registration

let k be Nat;
let pm be Element of REAL ;

cluster GoCross_Seq_REAL (pm,k) -> Borel_Sets -valued ;

coherence
GoCross_Seq_REAL (pm,k) is Borel_Sets -valued ;

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

proof end;

definition

let k be Nat;
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
ex b₁ being SetSequence of REAL st
( b₁ . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being SetSequence of REAL st b₁ . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) & b₂ . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines GoCross_Partial_Union FINANCE2:def 3 :
for k being Nat
for pm being Element of REAL
for b₃ being SetSequence of REAL holds
( b₃ = GoCross_Partial_Union (pm,k) iff ( b₃ . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds b₃ . (n + 1) = (b₃ . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) ) );

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 ;

proof end;

end;

registration

let k be Nat;
let pm be Element of REAL ;

cluster GoCross_Partial_Union (pm,k) -> Borel_Sets -valued ;

coherence
GoCross_Partial_Union (pm,k) is Borel_Sets -valued ;

end;

registration

let k be Nat;
let pm be Element of REAL ;

cluster GoCross_Partial_Union (pm,k) -> non-descending ;

coherence
GoCross_Partial_Union (pm,k) is non-descending

proof end;

end;

definition

let pm be Element of REAL ;

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
ex b₁ being SetSequence of REAL st
( b₁ . 0 = Union (GoCross_Partial_Union (pm,0)) & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) )

proof end;

uniqueness
for b₁, b₂ being SetSequence of REAL st b₁ . 0 = Union (GoCross_Partial_Union (pm,0)) & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) & b₂ . 0 = Union (GoCross_Partial_Union (pm,0)) & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines GoCross_Union FINANCE2:def 4 :
for pm being Element of REAL
for b₂ being SetSequence of REAL holds
( b₂ = GoCross_Union pm iff ( b₂ . 0 = Union (GoCross_Partial_Union (pm,0)) & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) ) );

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 ;

proof end;

end;

registration

let pm be Element of REAL ;

cluster GoCross_Union pm -> Borel_Sets -valued ;

coherence
GoCross_Union pm is Borel_Sets -valued ;

end;

registration

let pm be Element of REAL ;

cluster GoCross_Union pm -> non-descending ;

coherence
GoCross_Union pm is non-descending

proof end;

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

proof end;

theorem Th41: :: FINANCE2:18

RAT is Event of Borel_Sets

proof end;

theorem :: FINANCE2:19

REAL \ INT is Event of Borel_Sets

proof end;

theorem :: FINANCE2:20

REAL \ RAT is Event of Borel_Sets

proof end;

theorem :: FINANCE2:21

IRRAT is Event of Borel_Sets

proof end;

:: Since the Borel-Sets can be constructed by different sets of intervals,
:: we show, that other sets can do this.

theorem :: FINANCE2:22

Borel_Sets = sigma Family_of_halflines2

proof end;

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

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

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

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

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

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

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

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;

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
ex b₁ being Function of Omega,REAL st
for w being Element of Omega holds b₁ . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n)

proof end;

uniqueness
for b₁, b₂ being Function of Omega,REAL st ( for w being Element of Omega holds b₁ . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) & ( for w being Element of Omega holds b₂ . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) holds
b₁ = b₂

proof end;

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₇ being Function of Omega,REAL holds
( b₇ = RVElementsOfPortfolioValue_fut (phi,F,G,n) iff for w being Element of Omega holds b₇ . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) );

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

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;

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
ex b₁ being Real_Sequence st
for n being Nat holds b₁ . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for n being Nat holds b₁ . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w ) & ( for n being Nat holds b₂ . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w ) holds
b₁ = b₂

proof end;

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₇ being Real_Sequence holds
( b₇ = RVPortfolioValueFutExt_El (phi,F,G,w) iff for n being Nat holds b₇ . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w );

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;

:: 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
coherence
PortfolioValueFutExt (d,phi,F,G,w) is Real;
compatibility
for b₁ being Real holds
( b₁ = PortfolioValueFutExt (d,phi,F,G,w) iff b₁ = (Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . d );

proof end;

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;