FINANCE3: Modelling Real World Using Stochastic Processes and Filtration

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

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 ;

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

proof end;

proof end;

end;

:: deftheorem Def2 defines RVPortfolioValueFutExt FINANCE3:def 1 :

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

proof end;

end;

:: deftheorem defines PortfolioValueFut FINANCE3:def 2 :

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

proof end;

proof end;

end;

:: deftheorem Def4 defines RVPortfolioValueFut FINANCE3:def 3 :

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 by NUMBERS:19;

end;

:: deftheorem Def89 defines SetForCall-Option FINANCE3:def 4 :

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

proof end;

proof end;

end;

:: deftheorem defines Call-Option FINANCE3:def 5 :

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

proof end;

end;

:: deftheorem defines Special_SigmaField1 FINANCE3:def 6 :

definition

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

proof end;

end;

:: deftheorem defines Special_SigmaField2 FINANCE3:def 7 :

definition

end;

:: deftheorem FINANCE3:def 8 :

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

proof end;

end;

:: deftheorem Def2000 defines Filtration FINANCE3:def 9 :

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 by KOLMOG01:def 2;

end;

:: deftheorem defines El_Filtration FINANCE3:def 10 :

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 ;

end;

:: deftheorem Def8 defines Set1_of_SigmaField3 FINANCE3:def 11 :

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

end;

:: deftheorem Def9 defines Set2_of_SigmaField3 FINANCE3:def 12 :

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

proof end;

end;

:: deftheorem Def30000 defines Stochastic_Process FINANCE3:def 13 :

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

proof end;

end;

:: deftheorem defines RVProcess FINANCE3:def 14 :

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 ;

proof end;

end;

:: deftheorem Def30002 defines Adapted_Stochastic_Process FINANCE3:def 15 :

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 ;

proof end;

end;

:: deftheorem defines Predictable_Stochastic_Process FINANCE3:def 16 :

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 :

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;

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

end;

:: deftheorem defines Set1_for_RandomVariable FINANCE3:def 18 :

:: deftheorem Def79 defines Set4_for_RandomVariable FINANCE3:def 19 :

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

end;

:: deftheorem Def78 defines Set3_for_RandomVariable FINANCE3:def 20 :

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

end;

:: deftheorem Def77 defines Set2_for_RandomVariable FINANCE3:def 21 :

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;

proof end;

end;

:: deftheorem Def1211 defines FunctionRV1 FINANCE3:def 22 :

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;

proof end;

end;

:: deftheorem Def1212 defines FunctionRV2 FINANCE3:def 23 :

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;