:: Modelling Real World Using Stochastic Processes and Filtration
:: by Peter Jaeger
::
:: Received December 30, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

Lemacik: for a, b, c being set st ( a = 1 or a = 2 or a = 3 or a = 4 ) & ( b = 1 or b = 2 or b = 3 or b = 4 ) & ( c = 1 or c = 2 or c = 3 or c = 4 ) holds
{a,b,c} c= {1,2,3,4}

proof end;

Lemacik2: for a, b being set st ( a = 1 or a = 2 or a = 3 or a = 4 ) & ( b = 1 or b = 2 or b = 3 or b = 4 ) holds
{a,b} c= {1,2,3,4}

proof end;

Lemacik3: for a being set st ( a = 1 or a = 2 or a = 3 or a = 4 ) holds
{a} c= {1,2,3,4}

proof end;

The1: for A1 being SetSequence of {1,2,3,4} st ex n being Nat st A1 . n = {} holds
Intersection A1 = {}

proof end;

EnLm1: {1} c= {1,2,3,4}
by Lemacik3;

EnLm2: {2} c= {1,2,3,4}
by Lemacik3;

EnLm3: {3} c= {1,2,3,4}
by Lemacik3;

EnLm4: {4} c= {1,2,3,4}
by Lemacik3;

theorem :: FINANCE3:1

for a, b being object st a <> b holds
{a} c< {a,b} by ZFMISC_1:7, ZFMISC_1:20;

Lm1: {3,4} c= {1,2,3,4}
by Lemacik2;

Lm2: {1,2} c= {1,2,3,4}
by Lemacik2;

Lm3: {1,2} /\ {3,4} = {}

proof end;

Lem1: {1,2,3,4} \ {1,2} = {3,4}

proof end;

Lem2: {1,2,3,4} \ {3,4} = {1,2}

proof end;

B13: {1,3} in bool {1,2,3,4}

proof end;

B14: {1,4} in bool {1,2,3,4}

proof end;

B124: {1,2,4} in bool {1,2,3,4}

proof end;

B134: {1,3,4} in bool {1,2,3,4}

proof end;

B234: {2,3,4} in bool {1,2,3,4}

proof end;

B123: {1,2,3} in bool {1,2,3,4}

proof end;

B23: {2,3} in bool {1,2,3,4}

proof end;

B24: {2,4} in bool {1,2,3,4}

proof end;

B25: {1,2} in bool {1,2,3,4}

proof end;

B26: {3,4} in bool {1,2,3,4}

proof end;

WW1: {1,2,3} <> {3,4}

proof end;

The0: {{},{1,2},{3,4},{1,2,3,4}} <> bool {1,2,3,4}

proof end;

set Omega3 = {1,2,3};

set Omega4 = {1,2,3,4};

ATh102: {1,2,3} c< {1,2,3,4}

proof end;

set Omega2 = {1,2};

ATh101: {1,2} c< {1,2,3}

proof end;

registration

let I be non empty Subset of NAT;

cluster In (I,(bool REAL)) -> non empty ;

coherence
not In (I,(bool REAL)) is empty

proof end;

end;

theorem :: FINANCE3:2

for T being Nat holds { w where w is Element of NAT : ( w > 0 & w <= T ) } c= { w where w is Element of NAT : w <= T }

proof end;

theorem :: FINANCE3:3

for T being Nat holds { w where w is Element of NAT : w <= T } is non empty Subset of NAT

proof end;

theorem :: FINANCE3:4

for T being Nat st T > 0 holds
{ w where w is Element of NAT : ( w > 0 & w <= T ) } is non empty Subset of NAT

proof end;

:: Special Random-Variables

theorem :: FINANCE3:5

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))} is Event of Borel_Sets by FINANCE2:5;

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) -> Element of REAL ;
coherence
PortfolioValueFutExt (d,phi,F,G,w) is Element of REAL ;

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 d be Nat;

func RVPortfolioValueFutExt (phi,F,G,d) -> Function of Omega,REAL means :Def2: :: FINANCE3:def 1
for w being Element of Omega holds it . w = PortfolioValueFutExt (d,phi,F,G,w);

existence
ex b₁ being Function of Omega,REAL st
for w being Element of Omega holds b₁ . w = PortfolioValueFutExt (d,phi,F,G,w)

proof end;

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

proof end;

end;

:: deftheorem Def2 defines RVPortfolioValueFutExt FINANCE3:def 1 :
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 d being Nat
for b₇ being Function of Omega,REAL holds
( b₇ = RVPortfolioValueFutExt (phi,F,G,d) iff for w being Element of Omega holds b₇ . w = PortfolioValueFutExt (d,phi,F,G,w) );

theorem :: FINANCE3:6

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 d being Nat holds RVPortfolioValueFutExt (phi,F,G,d) is random_variable of F, Borel_Sets

proof end;

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: PortfolioValueFut
redefine func PortfolioValueFut (d,phi,F,G,w) -> Real equals :: FINANCE3:def 2
(Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . (d - 1);

correctness
coherence
PortfolioValueFut (d,phi,F,G,w) is Real;
compatibility
for b₁ being Real holds
( b₁ = PortfolioValueFut (d,phi,F,G,w) iff b₁ = (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . (d - 1) );

proof end;

end;

:: deftheorem defines PortfolioValueFut FINANCE3:def 2 :
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 ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . (d - 1);

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: PortfolioValueFut
redefine func PortfolioValueFut (d,phi,F,G,w) -> Element of REAL ;
coherence
PortfolioValueFut (d,phi,F,G,w) is Element of REAL by XREAL_0:def 1;

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 d be Nat;

func RVPortfolioValueFut (phi,F,G,d) -> Function of Omega,REAL means :Def4: :: FINANCE3:def 3
for w being Element of Omega holds it . w = PortfolioValueFut ((d + 1),phi,F,G,w);

existence
ex b₁ being Function of Omega,REAL st
for w being Element of Omega holds b₁ . w = PortfolioValueFut ((d + 1),phi,F,G,w)

proof end;

uniqueness
for b₁, b₂ being Function of Omega,REAL st ( for w being Element of Omega holds b₁ . w = PortfolioValueFut ((d + 1),phi,F,G,w) ) & ( for w being Element of Omega holds b₂ . w = PortfolioValueFut ((d + 1),phi,F,G,w) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines RVPortfolioValueFut FINANCE3:def 3 :
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 d being Nat
for b₇ being Function of Omega,REAL holds
( b₇ = RVPortfolioValueFut (phi,F,G,d) iff for w being Element of Omega holds b₇ . w = PortfolioValueFut ((d + 1),phi,F,G,w) );

theorem :: FINANCE3:7

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 d being Nat holds RVPortfolioValueFut (phi,F,G,d) is random_variable of F, Borel_Sets

proof end;

theorem :: FINANCE3:8

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 + 1),phi,F,G,w) = (RVPortfolioValueFut (phi,F,G,d)) . w & {(PortfolioValueFut ((d + 1),phi,F,G,w))} is Event of Borel_Sets ) by Def4, FINANCE2:5;

theorem :: FINANCE3:9

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 d being Nat holds RVPortfolioValueFutExt (phi,F,G,(d + 1)) = (RVPortfolioValueFut (phi,F,G,d)) + (RVElementsOfPortfolioValue_fut (phi,F,G,0))

proof end;

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

theorem 1A5: :: FINANCE3:10

for Omega, Omega2 being non empty set
for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for s being Element of Omega2 holds Omega --> s is Sigma,Sigma2 -random_variable-like

proof end;

theorem :: FINANCE3:11

for Omega being non empty set
for Sigma being SigmaField of Omega
for RV being random_variable of Sigma, Borel_Sets
for K being Real holds RV - (Omega --> K) is random_variable of Sigma, Borel_Sets

proof end;

definition

let Omega be non empty set ;
let RV be Function of Omega,REAL;
let w be Element of Omega;

func SetForCall-Option (RV,w) -> Element of REAL equals :Def89: :: FINANCE3:def 4
RV . w if RV . w >= 0
otherwise 0 ;

correctness
coherence
( ( RV . w >= 0 implies RV . w is Element of REAL ) & ( not RV . w >= 0 implies 0 is Element of REAL ) );
consistency
for b₁ being Element of REAL holds verum;
by NUMBERS:19;

end;

:: deftheorem Def89 defines SetForCall-Option FINANCE3:def 4 :
for Omega being non empty set
for RV being Function of Omega,REAL
for w being Element of Omega holds
( ( RV . w >= 0 implies SetForCall-Option (RV,w) = RV . w ) & ( not RV . w >= 0 implies SetForCall-Option (RV,w) = 0 ) );

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let RV be random_variable of Sigma, Borel_Sets ;
let K be Real;

func Call-Option (RV,K) -> Function of Omega,REAL means :: FINANCE3:def 5
for w being Element of Omega holds
( ( (RV - (Omega --> K)) . w >= 0 implies it . w = (RV - (Omega --> K)) . w ) & ( (RV - (Omega --> K)) . w < 0 implies it . w = 0 ) );

existence
ex b₁ being Function of Omega,REAL st
for w being Element of Omega holds
( ( (RV - (Omega --> K)) . w >= 0 implies b₁ . w = (RV - (Omega --> K)) . w ) & ( (RV - (Omega --> K)) . w < 0 implies b₁ . w = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Function of Omega,REAL st ( for w being Element of Omega holds
( ( (RV - (Omega --> K)) . w >= 0 implies b₁ . w = (RV - (Omega --> K)) . w ) & ( (RV - (Omega --> K)) . w < 0 implies b₁ . w = 0 ) ) ) & ( for w being Element of Omega holds
( ( (RV - (Omega --> K)) . w >= 0 implies b₂ . w = (RV - (Omega --> K)) . w ) & ( (RV - (Omega --> K)) . w < 0 implies b₂ . w = 0 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines Call-Option FINANCE3:def 5 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for RV being random_variable of Sigma, Borel_Sets
for K being Real
for b₅ being Function of Omega,REAL holds
( b₅ = Call-Option (RV,K) iff for w being Element of Omega holds
( ( (RV - (Omega --> K)) . w >= 0 implies b₅ . w = (RV - (Omega --> K)) . w ) & ( (RV - (Omega --> K)) . w < 0 implies b₅ . w = 0 ) ) );

:: Special sigma-Fields

theorem SuperLemma1: :: FINANCE3:12

for A1 being SetSequence of {1,2,3,4}
for w being Real st ( w = 1 or w = 3 ) & ( for n being Nat holds
( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} ) ) holds
{w} <> Intersection A1

proof end;

theorem SuperLemma2: :: FINANCE3:13

for A1 being SetSequence of {1,2,3,4}
for w being Real st ( w = 2 or w = 4 ) & ( for n being Nat holds
( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} ) ) holds
{w} <> Intersection A1

proof end;

theorem :: FINANCE3:14

for MySigmaField, A1, A2 being set st MySigmaField = {{},{1,2,3,4}} & A1 in MySigmaField & A2 in MySigmaField holds
A1 /\ A2 in MySigmaField

proof end;

theorem Lm700000: :: FINANCE3:15

for A1 being SetSequence of {1,2,3,4} st ( for n, k being Nat holds not (A1 . n) /\ (A1 . k) = {} ) & rng A1 c= {{},{1,2},{3,4},{1,2,3,4}} & not Intersection A1 = {} & not Intersection A1 = {1,2} & not Intersection A1 = {3,4} holds
Intersection A1 = {1,2,3,4}

proof end;

theorem :: FINANCE3:16

for A1 being SetSequence of {1,2,3,4}
for MyOmega being set st MyOmega = {{},{1,2},{3,4},{1,2,3,4}} & Intersection A1 = {1,2,3,4} holds
Intersection A1 in MyOmega by ENUMSET1:def 2;

theorem :: FINANCE3:17

for A1 being SetSequence of {1,2,3,4}
for MyOmega being set st MyOmega = {{},{1,2},{3,4},{1,2,3,4}} & Intersection A1 = {3,4} holds
Intersection A1 in MyOmega by ENUMSET1:def 2;

theorem :: FINANCE3:18

for A1 being SetSequence of {1,2,3,4}
for MyOmega being set st MyOmega = {{},{1,2},{3,4},{1,2,3,4}} & Intersection A1 = {1,2} holds
Intersection A1 in MyOmega by ENUMSET1:def 2;

theorem :: FINANCE3:19

for A1 being SetSequence of {1,2,3,4}
for MyOmega being set st MyOmega = {{},{1,2},{3,4},{1,2,3,4}} & Intersection A1 = {} holds
Intersection A1 in MyOmega by ENUMSET1:def 2;

theorem Lm8: :: FINANCE3:20

for MyOmega being set
for A1 being SetSequence of {1,2,3,4} st rng A1 c= MyOmega & MyOmega = {{},{1,2},{3,4},{1,2,3,4}} holds
Intersection A1 in MyOmega

proof end;

theorem Lm9: :: FINANCE3:21

for MySigmaField, MySet being set
for A1 being SetSequence of MySet st MySet = {1,2,3,4} & rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} & Intersection A1 <> {} holds
Intersection A1 in MySigmaField

proof end;

theorem :: FINANCE3:22

for MySigmaField, MySet being set
for A1 being SetSequence of MySet st MySet = {1,2,3,4} & rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} holds
for k1, k2 being Nat holds (A1 . k1) /\ (A1 . k2) in MySigmaField

proof end;

definition

func Special_SigmaField1 -> SigmaField of {1,2,3,4} equals :: FINANCE3:def 6
{{},{1,2,3,4}};

correctness
coherence
{{},{1,2,3,4}} is SigmaField of {1,2,3,4};

proof end;

end;

:: deftheorem defines Special_SigmaField1 FINANCE3:def 6 :
Special_SigmaField1 = {{},{1,2,3,4}};

definition

func Special_SigmaField2 -> SigmaField of {1,2,3,4} equals :: FINANCE3:def 7
{{},{1,2},{3,4},{1,2,3,4}};

correctness
coherence
{{},{1,2},{3,4},{1,2,3,4}} is SigmaField of {1,2,3,4};

proof end;

end;

:: deftheorem defines Special_SigmaField2 FINANCE3:def 7 :
Special_SigmaField2 = {{},{1,2},{3,4},{1,2,3,4}};

definition

end;

:: deftheorem FINANCE3:def 8 :
canceled;

theorem :: FINANCE3:23

for Omega being set st Omega = {1,2,3,4} holds
( {1} c= Omega & {2} c= Omega & {3} c= Omega & {4} c= Omega & {1,2} c= Omega & {3,4} c= Omega & {} c= Omega & Omega c= Omega )

proof end;

theorem :: FINANCE3:24

for Omega being set st Omega = {1,2,3,4} holds
( Omega in Special_SigmaField1 & {} in Special_SigmaField1 & {1,2} in Special_SigmaField2 & {3,4} in Special_SigmaField2 & Omega in Special_SigmaField2 & {} in Special_SigmaField2 & Omega in Trivial-SigmaField {1,2,3,4} & {} in Trivial-SigmaField {1,2,3,4} & {1} in Trivial-SigmaField {1,2,3,4} & {2} in Trivial-SigmaField {1,2,3,4} & {3} in Trivial-SigmaField {1,2,3,4} & {4} in Trivial-SigmaField {1,2,3,4} ) by EnLm1, EnLm2, EnLm3, PROB_1:5, EnLm4, PROB_1:4, ENUMSET1:def 2;

XX1: {{},{1,2,3,4}} c< {{},{1,2},{3,4},{1,2,3,4}}

proof end;

XX2: {{},{1,2},{3,4},{1,2,3,4}} c< bool {1,2,3,4}

proof end;

theorem :: FINANCE3:25

( Special_SigmaField1 c< Special_SigmaField2 & Special_SigmaField2 c< Trivial-SigmaField {1,2,3,4} ) by XX1, XX2;

:: Construction of Filtration and Examples

theorem :: FINANCE3:26

ex Omega being non empty set ex F1, F2, F3 being SigmaField of Omega st
( F1 c< F2 & F2 c< F3 )

proof end;

theorem :: FINANCE3:27

ex Omega1, Omega2, Omega3, Omega4 being non empty set st
( Omega1 c< Omega2 & Omega2 c< Omega3 & Omega3 c< Omega4 & ex F1 being SigmaField of Omega1 ex F2 being SigmaField of Omega2 ex F3 being SigmaField of Omega3 ex F4 being SigmaField of Omega4 st
( F1 c= F2 & F2 c= F3 & F3 c= F4 ) )

proof end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let I be non empty real-membered set ;

mode Filtration of I,Sigma -> ManySortedSigmaField of I,Sigma means :Def2000: :: FINANCE3:def 9
for s, t being Element of I st s <= t holds
it . s is Subset of (it . t);

existence
ex b₁ being ManySortedSigmaField of I,Sigma st
for s, t being Element of I st s <= t holds
b₁ . s is Subset of (b₁ . t)

proof end;

end;

:: deftheorem Def2000 defines Filtration FINANCE3:def 9 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for I being non empty real-membered set
for b₄ being ManySortedSigmaField of I,Sigma holds
( b₄ is Filtration of I,Sigma iff for s, t being Element of I st s <= t holds
b₄ . s is Subset of (b₄ . t) );

definition

let I, Omega be non empty set ;
let Sigma be SigmaField of Omega;
let Filt be ManySortedSigmaField of I,Sigma;
let i be Element of I;

func El_Filtration (i,Filt) -> SigmaField of Omega equals :: FINANCE3:def 10
Filt . i;

correctness
coherence
Filt . i is SigmaField of Omega;
by KOLMOG01:def 2;

end;

:: deftheorem defines El_Filtration FINANCE3:def 10 :
for I, Omega being non empty set
for Sigma being SigmaField of Omega
for Filt being ManySortedSigmaField of I,Sigma
for i being Element of I holds El_Filtration (i,Filt) = Filt . i;

definition

let k be Element of {1,2,3};

func Set1_of_SigmaField3 k -> Subset of (bool {1,2,3,4}) equals :Def8: :: FINANCE3:def 11
Special_SigmaField1 if k = 1
otherwise Special_SigmaField2 ;

correctness
coherence
( ( k = 1 implies Special_SigmaField1 is Subset of (bool {1,2,3,4}) ) & ( not k = 1 implies Special_SigmaField2 is Subset of (bool {1,2,3,4}) ) );
consistency
for b₁ being Subset of (bool {1,2,3,4}) holds verum;
;

end;

:: deftheorem Def8 defines Set1_of_SigmaField3 FINANCE3:def 11 :
for k being Element of {1,2,3} holds
( ( k = 1 implies Set1_of_SigmaField3 k = Special_SigmaField1 ) & ( not k = 1 implies Set1_of_SigmaField3 k = Special_SigmaField2 ) );

definition

let k be Element of {1,2,3};

func Set2_of_SigmaField3 k -> Subset of (bool {1,2,3,4}) equals :Def9: :: FINANCE3:def 12
Set1_of_SigmaField3 k if k <= 2
otherwise Trivial-SigmaField {1,2,3,4};

correctness
coherence
( ( k <= 2 implies Set1_of_SigmaField3 k is Subset of (bool {1,2,3,4}) ) & ( not k <= 2 implies Trivial-SigmaField {1,2,3,4} is Subset of (bool {1,2,3,4}) ) );
consistency
for b₁ being Subset of (bool {1,2,3,4}) holds verum;
;

end;

:: deftheorem Def9 defines Set2_of_SigmaField3 FINANCE3:def 12 :
for k being Element of {1,2,3} holds
( ( k <= 2 implies Set2_of_SigmaField3 k = Set1_of_SigmaField3 k ) & ( not k <= 2 implies Set2_of_SigmaField3 k = Trivial-SigmaField {1,2,3,4} ) );

Th3: for Sigma being SigmaField of {1,2,3,4}
for I being set st I = {1,2,3} & Sigma = bool {1,2,3,4} holds
ex MyFunc being ManySortedSigmaField of I,Sigma st
( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} )

proof end;

theorem MyNeed: :: FINANCE3:28

for Omega being non empty set
for Sigma being SigmaField of Omega
for I being non empty real-membered set st I = {1,2,3} & Sigma = bool {1,2,3,4} & Omega = {1,2,3,4} holds
ex MyFunc being Filtration of I,Sigma st
( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} )

proof end;

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

Lm2A: for Omega being non empty set
for Sigma4 being SigmaField of Omega
for Sigma5 being SigmaField of {1} holds Omega --> 1 is random_variable of Sigma4,Sigma5

proof end;

theorem THJ1: :: FINANCE3:29

for Omega being non empty set
for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of {1} st Omega = {1,2,3,4} holds
ex X1 being Function of Omega,{1} st
( X1 is random_variable of Special_SigmaField1 ,Sigma2 & X1 is random_variable of Special_SigmaField2 ,Sigma2 & X1 is random_variable of Trivial-SigmaField {1,2,3,4},Sigma2 )

proof end;

:: The first example of the existence of a random-variable depends
:: on a special underlying sigma-field and given Filtration

theorem :: FINANCE3:30

ex Omega, Omega2 being non empty set ex Sigma being SigmaField of Omega ex Sigma2 being SigmaField of Omega2 ex I being non empty real-membered set ex Q being Filtration of I,Sigma ex rv being Function of Omega,Omega2 st
for i being Element of I holds rv is random_variable of El_Filtration (i,Q),Sigma2

proof end;

:: Next theorem gives also the existence of random_variables
:: depending on arbitrary sigma-fields and filtrations

theorem :: FINANCE3:31

for Omega, Omega2 being non empty set
for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for I being non empty real-membered set
for Q being ManySortedSigmaField of I,Sigma ex rv being Function of Omega,Omega2 st
for i being Element of I holds rv is random_variable of El_Filtration (i,Q),Sigma2

proof end;

:: Stochastic Process: adapted and predictable
:: The next statement is important for the usage of a probability measure
:: with Events depending on SigmaFields in a given filtration.

theorem :: FINANCE3:32

for Omega being non empty set
for Sigma, Sigma2 being SigmaField of Omega st Sigma2 c= Sigma holds
for E2 being Event of Sigma2 holds E2 is Event of Sigma ;

:: Next we define the stochastic process

definition

let Omega, Omega2 be non empty set ;
let Sigma be SigmaField of Omega;
let Sigma2 be SigmaField of Omega2;
let I be non empty real-membered set ;

mode Stochastic_Process of I,Sigma,Sigma2 -> Function of I,(set_of_random_variables_on (Sigma,Sigma2)) means :Def30000: :: FINANCE3:def 13
for k being Element of I ex RV being Function of Omega,Omega2 st
( it . k = RV & RV is Sigma,Sigma2 -random_variable-like );

existence
ex b₁ being Function of I,(set_of_random_variables_on (Sigma,Sigma2)) st
for k being Element of I ex RV being Function of Omega,Omega2 st
( b₁ . k = RV & RV is Sigma,Sigma2 -random_variable-like )

proof end;

end;

:: deftheorem Def30000 defines Stochastic_Process FINANCE3:def 13 :
for Omega, Omega2 being non empty set
for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for I being non empty real-membered set
for b₆ being Function of I,(set_of_random_variables_on (Sigma,Sigma2)) holds
( b₆ is Stochastic_Process of I,Sigma,Sigma2 iff for k being Element of I ex RV being Function of Omega,Omega2 st
( b₆ . k = RV & RV is Sigma,Sigma2 -random_variable-like ) );

:: Because adapted and predicted stochastic processes are very important for
:: Stochastic finance, we implement them now:

definition

let Omega, Omega2 be non empty set ;
let Sigma be SigmaField of Omega;
let Sigma2 be SigmaField of Omega2;
let I be non empty real-membered set ;
let Stoch be Stochastic_Process of I,Sigma,Sigma2;
let k be Element of I;

func RVProcess (Stoch,k) -> random_variable of Sigma,Sigma2 equals :: FINANCE3:def 14
Stoch . k;

coherence
Stoch . k is random_variable of Sigma,Sigma2

proof end;

end;

:: deftheorem defines RVProcess FINANCE3:def 14 :
for Omega, Omega2 being non empty set
for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for I being non empty real-membered set
for Stoch being Stochastic_Process of I,Sigma,Sigma2
for k being Element of I holds RVProcess (Stoch,k) = Stoch . k;

definition

let Omega, Omega2 be non empty set ;
let Sigma be SigmaField of Omega;
let Sigma2 be SigmaField of Omega2;
let I be non empty real-membered set ;
let Stoch be Stochastic_Process of I,Sigma,Sigma2;

mode Adapted_Stochastic_Process of Stoch -> Function of I,(set_of_random_variables_on (Sigma,Sigma2)) means :Def30002: :: FINANCE3:def 15
ex k being Filtration of I,Sigma st
for i being Element of I holds RVProcess (Stoch,i) is El_Filtration (i,k),Sigma2 -random_variable-like ;

existence
ex b₁ being Function of I,(set_of_random_variables_on (Sigma,Sigma2)) ex k being Filtration of I,Sigma st
for i being Element of I holds RVProcess (Stoch,i) is El_Filtration (i,k),Sigma2 -random_variable-like

proof end;

end;

:: deftheorem Def30002 defines Adapted_Stochastic_Process FINANCE3:def 15 :
for Omega, Omega2 being non empty set
for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for I being non empty real-membered set
for Stoch being Stochastic_Process of I,Sigma,Sigma2
for b₇ being Function of I,(set_of_random_variables_on (Sigma,Sigma2)) holds
( b₇ is Adapted_Stochastic_Process of Stoch iff ex k being Filtration of I,Sigma st
for i being Element of I holds RVProcess (Stoch,i) is El_Filtration (i,k),Sigma2 -random_variable-like );

definition

let Omega, Omega2 be non empty set ;
let Sigma be SigmaField of Omega;
let Sigma2 be SigmaField of Omega2;
let I, J be non empty Subset of NAT;
let Stoch be Stochastic_Process of In (J,(bool REAL)),Sigma,Sigma2;

mode Predictable_Stochastic_Process of I,J,Sigma,Sigma2,Stoch -> Function of J,(set_of_random_variables_on (Sigma,Sigma2)) means :: FINANCE3:def 16
ex k being Filtration of In (I,(bool REAL)),Sigma st
for j being Element of In (J,(bool REAL))
for i being Element of In (I,(bool REAL)) st j - 1 = i holds
RVProcess (Stoch,j) is El_Filtration (i,k),Sigma2 -random_variable-like ;

existence
ex b₁ being Function of J,(set_of_random_variables_on (Sigma,Sigma2)) ex k being Filtration of In (I,(bool REAL)),Sigma st
for j being Element of In (J,(bool REAL))
for i being Element of In (I,(bool REAL)) st j - 1 = i holds
RVProcess (Stoch,j) is El_Filtration (i,k),Sigma2 -random_variable-like

proof end;

end;

:: deftheorem defines Predictable_Stochastic_Process FINANCE3:def 16 :
for Omega, Omega2 being non empty set
for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for I, J being non empty Subset of NAT
for Stoch being Stochastic_Process of In (J,(bool REAL)),Sigma,Sigma2
for b₈ being Function of J,(set_of_random_variables_on (Sigma,Sigma2)) holds
( b₈ is Predictable_Stochastic_Process of I,J,Sigma,Sigma2,Stoch iff ex k being Filtration of In (I,(bool REAL)),Sigma st
for j being Element of In (J,(bool REAL))
for i being Element of In (I,(bool REAL)) st j - 1 = i holds
RVProcess (Stoch,j) is El_Filtration (i,k),Sigma2 -random_variable-like );

definition

let Omega, Omega2 be non empty set ;
let Sigma be SigmaField of Omega;
let Sigma2 be SigmaField of Omega2;
let I be non empty real-membered set ;
let MyFunc be ManySortedSigmaField of I,Sigma;
let Stoch be Stochastic_Process of I,Sigma,Sigma2;

attr Stoch is MyFunc -stoch_proc_wrt_to_Filtration means :: FINANCE3:def 17
for i being Element of I holds RVProcess (Stoch,i) is El_Filtration (i,MyFunc),Sigma2 -random_variable-like ;

end;

:: deftheorem defines -stoch_proc_wrt_to_Filtration FINANCE3:def 17 :
for Omega, Omega2 being non empty set
for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for I being non empty real-membered set
for MyFunc being ManySortedSigmaField of I,Sigma
for Stoch being Stochastic_Process of I,Sigma,Sigma2 holds
( Stoch is MyFunc -stoch_proc_wrt_to_Filtration iff for i being Element of I holds RVProcess (Stoch,i) is El_Filtration (i,MyFunc),Sigma2 -random_variable-like );

theorem :: FINANCE3:33

for Omega, Omega2 being non empty set
for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for I being non empty real-membered set
for MyFunc being Filtration of I,Sigma
for Stoch being Stochastic_Process of I,Sigma,Sigma2 st Stoch is MyFunc -stoch_proc_wrt_to_Filtration holds
Stoch is Adapted_Stochastic_Process of Stoch by Def30002;

:: Example for a Stochastic Process

definition

let k1, k2 be Element of REAL ;
let Omega be non empty set ;
let k be Element of Omega;

func Set1_for_RandomVariable (k1,k2,k) -> Element of REAL equals :: FINANCE3:def 18
k1 if ( k = 1 or k = 2 )
otherwise k2;

correctness
coherence
( ( ( k = 1 or k = 2 ) implies k1 is Element of REAL ) & ( k = 1 or k = 2 or k2 is Element of REAL ) );
consistency
for b₁ being Element of REAL holds verum;
;

func Set4_for_RandomVariable (k1,k2,k) -> Element of REAL equals :Def79: :: FINANCE3:def 19
k1 if k = 3
otherwise k2;

correctness
coherence
( ( k = 3 implies k1 is Element of REAL ) & ( not k = 3 implies k2 is Element of REAL ) );
consistency
for b₁ being Element of REAL holds verum;
;

end;

:: deftheorem defines Set1_for_RandomVariable FINANCE3:def 18 :
for k1, k2 being Element of REAL
for Omega being non empty set
for k being Element of Omega holds
( ( ( k = 1 or k = 2 ) implies Set1_for_RandomVariable (k1,k2,k) = k1 ) & ( k = 1 or k = 2 or Set1_for_RandomVariable (k1,k2,k) = k2 ) );

:: deftheorem Def79 defines Set4_for_RandomVariable FINANCE3:def 19 :
for k1, k2 being Element of REAL
for Omega being non empty set
for k being Element of Omega holds
( ( k = 3 implies Set4_for_RandomVariable (k1,k2,k) = k1 ) & ( not k = 3 implies Set4_for_RandomVariable (k1,k2,k) = k2 ) );

definition

let k2, k3, k4 be Element of REAL ;
let Omega be non empty set ;
let k be Element of Omega;

func Set3_for_RandomVariable (k2,k3,k4,k) -> Element of REAL equals :Def78: :: FINANCE3:def 20
k2 if k = 2
otherwise Set4_for_RandomVariable (k3,k4,k);

correctness
coherence
( ( k = 2 implies k2 is Element of REAL ) & ( not k = 2 implies Set4_for_RandomVariable (k3,k4,k) is Element of REAL ) );
consistency
for b₁ being Element of REAL holds verum;
;

end;

:: deftheorem Def78 defines Set3_for_RandomVariable FINANCE3:def 20 :
for k2, k3, k4 being Element of REAL
for Omega being non empty set
for k being Element of Omega holds
( ( k = 2 implies Set3_for_RandomVariable (k2,k3,k4,k) = k2 ) & ( not k = 2 implies Set3_for_RandomVariable (k2,k3,k4,k) = Set4_for_RandomVariable (k3,k4,k) ) );

definition

let k1, k2, k3, k4 be Element of REAL ;
let Omega be non empty set ;
let k be Element of Omega;

func Set2_for_RandomVariable (k1,k2,k3,k4,k) -> Element of REAL equals :Def77: :: FINANCE3:def 21
k1 if k = 1
otherwise Set3_for_RandomVariable (k2,k3,k4,k);

correctness
coherence
( ( k = 1 implies k1 is Element of REAL ) & ( not k = 1 implies Set3_for_RandomVariable (k2,k3,k4,k) is Element of REAL ) );
consistency
for b₁ being Element of REAL holds verum;
;

end;

:: deftheorem Def77 defines Set2_for_RandomVariable FINANCE3:def 21 :
for k1, k2, k3, k4 being Element of REAL
for Omega being non empty set
for k being Element of Omega holds
( ( k = 1 implies Set2_for_RandomVariable (k1,k2,k3,k4,k) = k1 ) & ( not k = 1 implies Set2_for_RandomVariable (k1,k2,k3,k4,k) = Set3_for_RandomVariable (k2,k3,k4,k) ) );

theorem MYF30: :: FINANCE3:34

for k1, k2, k3, k4 being Element of REAL
for Omega being set st Omega = {1,2,3,4} holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 )

proof end;

theorem MyFunc5: :: FINANCE3:35

for k1, k2, k3, k4 being Element of REAL
for Omega being non empty set st Omega = {1,2,3,4} holds
for Sigma being SigmaField of Omega
for I being non empty real-membered set
for MyFunc being ManySortedSigmaField of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} holds
for eli being Element of I st eli = 3 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k2 & f . 3 = k3 & f . 4 = k4 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )

proof end;

theorem MyFunc6: :: FINANCE3:36

for k1, k2 being Element of REAL
for Omega being non empty set st Omega = {1,2,3,4} holds
for Sigma being SigmaField of Omega
for I being non empty real-membered set
for MyFunc being ManySortedSigmaField of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} holds
for eli being Element of I st eli = 2 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k1 & f . 3 = k2 & f . 4 = k2 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )

proof end;

theorem MyFunc7: :: FINANCE3:37

for k1 being Element of REAL
for Omega being non empty set st Omega = {1,2,3,4} holds
for Sigma being SigmaField of Omega
for I being non empty real-membered set
for MyFunc being ManySortedSigmaField of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} holds
for eli being Element of I st eli = 1 holds
ex f being Function of Omega,REAL st
( f . 1 = k1 & f . 2 = k1 & f . 3 = k1 & f . 4 = k1 & f is El_Filtration (eli,MyFunc), Borel_Sets -random_variable-like )

proof end;

theorem :: FINANCE3:38

for Omega being non empty set st Omega = {1,2,3,4} holds
for Sigma being SigmaField of Omega
for I being non empty real-membered set st I = {1,2,3} & Sigma = bool {1,2,3,4} holds
for MyFunc being ManySortedSigmaField of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} holds
for Prob being Function of Sigma,REAL
for i being Element of I ex RV being Function of Omega,REAL st RV is El_Filtration (i,MyFunc), Borel_Sets -random_variable-like

proof end;

definition

let I be non empty real-membered set ;
assume A0000: I = {1,2,3} ;
let i be Element of I;
assume MyI: ( i = 2 or i = 3 ) ;
let Omega be non empty set ;
assume A000: Omega = {1,2,3,4} ;
let Sigma be SigmaField of Omega;
assume A00: Sigma = bool Omega ;
let f1 be Function of Omega,REAL;
assume A0: ( f1 . 1 = 60 & f1 . 2 = 80 & f1 . 3 = 100 & f1 . 4 = 120 ) ;
let f2 be Function of Omega,REAL;
assume A1: ( f2 . 1 = 80 & f2 . 2 = 80 & f2 . 3 = 120 & f2 . 4 = 120 ) ;
let f3 be Function of Omega,REAL;

func FunctionRV1 (i,Sigma,f1,f2,f3) -> Element of set_of_random_variables_on (Sigma,Borel_Sets) equals :Def1211: :: FINANCE3:def 22
f2 if i = 2
otherwise f1;

correctness
coherence
( ( i = 2 implies f2 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( not i = 2 implies f1 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) );
consistency
for b₁ being Element of set_of_random_variables_on (Sigma,Borel_Sets) holds verum;

proof end;

end;

:: deftheorem Def1211 defines FunctionRV1 FINANCE3:def 22 :
for I being non empty real-membered set st I = {1,2,3} holds
for i being Element of I st ( i = 2 or i = 3 ) holds
for Omega being non empty set st Omega = {1,2,3,4} holds
for Sigma being SigmaField of Omega st Sigma = bool Omega holds
for f1 being Function of Omega,REAL st f1 . 1 = 60 & f1 . 2 = 80 & f1 . 3 = 100 & f1 . 4 = 120 holds
for f2 being Function of Omega,REAL st f2 . 1 = 80 & f2 . 2 = 80 & f2 . 3 = 120 & f2 . 4 = 120 holds
for f3 being Function of Omega,REAL holds
( ( i = 2 implies FunctionRV1 (i,Sigma,f1,f2,f3) = f2 ) & ( not i = 2 implies FunctionRV1 (i,Sigma,f1,f2,f3) = f1 ) );

definition

let I be non empty real-membered set ;
assume A0000: I = {1,2,3} ;
let i be Element of I;
let Omega be non empty set ;
assume A000: Omega = {1,2,3,4} ;
let Sigma be SigmaField of Omega;
assume A00: Sigma = bool Omega ;
let f1, f2 be Function of Omega,REAL;
let f3 be Function of Omega,REAL;
assume A2: ( f3 . 1 = 100 & f3 . 2 = 100 & f3 . 3 = 100 & f3 . 4 = 100 ) ;

func FunctionRV2 (i,Sigma,f1,f2,f3) -> Element of set_of_random_variables_on (Sigma,Borel_Sets) equals :Def1212: :: FINANCE3:def 23
FunctionRV1 (i,Sigma,f1,f2,f3) if ( i = 2 or i = 3 )
otherwise f3;

correctness
coherence
( ( ( i = 2 or i = 3 ) implies FunctionRV1 (i,Sigma,f1,f2,f3) is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) & ( i = 2 or i = 3 or f3 is Element of set_of_random_variables_on (Sigma,Borel_Sets) ) );
consistency
for b₁ being Element of set_of_random_variables_on (Sigma,Borel_Sets) holds verum;

proof end;

end;

:: deftheorem Def1212 defines FunctionRV2 FINANCE3:def 23 :
for I being non empty real-membered set st I = {1,2,3} holds
for i being Element of I
for Omega being non empty set st Omega = {1,2,3,4} holds
for Sigma being SigmaField of Omega st Sigma = bool Omega holds
for f1, f2, f3 being Function of Omega,REAL st f3 . 1 = 100 & f3 . 2 = 100 & f3 . 3 = 100 & f3 . 4 = 100 holds
( ( ( i = 2 or i = 3 ) implies FunctionRV2 (i,Sigma,f1,f2,f3) = FunctionRV1 (i,Sigma,f1,f2,f3) ) & ( i = 2 or i = 3 or FunctionRV2 (i,Sigma,f1,f2,f3) = f3 ) );

theorem :: FINANCE3:39

for Omega, Omega2 being non empty set st Omega = {1,2,3,4} holds
for Sigma being SigmaField of Omega
for I being non empty real-membered set st I = {1,2,3} & Sigma = bool {1,2,3,4} holds
for MyFunc being Filtration of I,Sigma st MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} holds
ex Stoch being Stochastic_Process of I,Sigma, Borel_Sets st
( ( for k being Element of I holds
( ex RV being Function of Omega,REAL st
( Stoch . k = RV & RV is Sigma, Borel_Sets -random_variable-like & RV is El_Filtration (k,MyFunc), Borel_Sets -random_variable-like ) & ex f being Function of Omega,REAL st
( k = 1 implies ( f . 1 = 100 & f . 2 = 100 & f . 3 = 100 & f . 4 = 100 & Stoch . k = f ) ) & ex f being Function of Omega,REAL st
( k = 2 implies ( f . 1 = 80 & f . 2 = 80 & f . 3 = 120 & f . 4 = 120 & Stoch . k = f ) ) & ex f being Function of Omega,REAL st
( k = 3 implies ( f . 1 = 60 & f . 2 = 80 & f . 3 = 100 & f . 4 = 120 & Stoch . k = f ) ) & Stoch is MyFunc -stoch_proc_wrt_to_Filtration ) ) & Stoch is Adapted_Stochastic_Process of Stoch )

proof end;