FINANCE2: Events of Borel Sets, Construction of Borel Sets and Random Variables for Stochastic Finance

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

cluster REAL \ INT -> non empty ;

coherence by Th6;

cluster REAL \ NAT -> non empty ;

coherence 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

proof end;

end;

:: deftheorem defines Family_of_halflines2 FINANCE2:def 1 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines GoCross_Seq_REAL FINANCE2:def 2 :

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

proof end;

end;

registration

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

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

coherence ;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines GoCross_Partial_Union FINANCE2:def 3 :

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

proof end;

end;

registration

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

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

coherence ;

end;

registration

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

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

coherence

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines GoCross_Union FINANCE2:def 4 :

definition

let pm be Element of REAL ;
:: original: GoCross_Union
redefine func GoCross_Union pm -> SetSequence of Borel_Sets ;
correctness

proof end;

end;

registration

let pm be Element of REAL ;

cluster GoCross_Union pm -> Borel_Sets -valued ;

coherence ;

end;

registration

let pm be Element of REAL ;

cluster GoCross_Union pm -> non-descending ;

coherence

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5000 defines RVElementsOfPortfolioValue_fut FINANCE2:def 5 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5001 defines RVPortfolioValueFutExt_El FINANCE2:def 6 :

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

proof end;

end;

:: deftheorem defines PortfolioValueFutExt FINANCE2:def 7 :