:: by Peter Jaeger

::

:: Received December 30, 2015

:: Copyright (c) 2015-2017 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

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

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

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

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;

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

for w being Element of Omega holds b_{1} . w = PortfolioValueFutExt (d,phi,F,G,w)

for b_{1}, b_{2} being Function of Omega,REAL st ( for w being Element of Omega holds b_{1} . w = PortfolioValueFutExt (d,phi,F,G,w) ) & ( for w being Element of Omega holds b_{2} . w = PortfolioValueFutExt (d,phi,F,G,w) ) 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 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 for w being Element of Omega holds it . w = PortfolioValueFutExt (d,phi,F,G,w);

ex b

for w being Element of Omega holds b

proof end;

uniqueness for b

b

proof 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_{7} being Function of Omega,REAL holds

( b_{7} = RVPortfolioValueFutExt (phi,F,G,d) iff for w being Element of Omega holds b_{7} . w = PortfolioValueFutExt (d,phi,F,G,w) );

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

( b

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

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;

coherence

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

compatibility

for b_{1} being Real holds

( b_{1} = PortfolioValueFut (d,phi,F,G,w) iff b_{1} = (Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . (d - 1) );

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: 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 redefine func PortfolioValueFut (d,phi,F,G,w) -> Real equals :: FINANCE3:def 2

(Partial_Sums ((RVPortfolioValueFutExt_El (phi,F,G,w)) ^\ 1)) . (d - 1);

coherence

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

compatibility

for b

( b

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

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

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;

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

for w being Element of Omega holds b_{1} . w = PortfolioValueFut ((d + 1),phi,F,G,w)

for b_{1}, b_{2} being Function of Omega,REAL st ( for w being Element of Omega holds b_{1} . w = PortfolioValueFut ((d + 1),phi,F,G,w) ) & ( for w being Element of Omega holds b_{2} . w = PortfolioValueFut ((d + 1),phi,F,G,w) ) 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 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 for w being Element of Omega holds it . w = PortfolioValueFut ((d + 1),phi,F,G,w);

ex b

for w being Element of Omega holds b

proof end;

uniqueness for b

b

proof 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_{7} being Function of Omega,REAL holds

( b_{7} = RVPortfolioValueFut (phi,F,G,d) iff for w being Element of Omega holds b_{7} . w = PortfolioValueFut ((d + 1),phi,F,G,w) );

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

( b

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

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;

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

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_random_variable_on Sigma,Sigma2

for Sigma being SigmaField of Omega

for Sigma2 being SigmaField of Omega2

for s being Element of Omega2 holds Omega --> s is_random_variable_on Sigma,Sigma2

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 Element of REAL holds RV - (Omega --> K) is random_variable of Sigma, Borel_Sets

for Sigma being SigmaField of Omega

for RV being random_variable of Sigma, Borel_Sets

for K being Element of 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;

coherence

( ( RV . w >= 0 implies RV . w is Element of REAL ) & ( not RV . w >= 0 implies 0 is Element of REAL ) );

consistency

for b_{1} being Element of REAL holds verum;

by NUMBERS:19;

end;
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 RV . w if RV . w >= 0

otherwise 0 ;

coherence

( ( RV . w >= 0 implies RV . w is Element of REAL ) & ( not RV . w >= 0 implies 0 is Element of REAL ) );

consistency

for b

by NUMBERS:19;

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

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 Element of REAL ;

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

for w being Element of Omega holds

( ( (RV - (Omega --> K)) . w >= 0 implies b_{1} . w = (RV - (Omega --> K)) . w ) & ( (RV - (Omega --> K)) . w < 0 implies b_{1} . w = 0 ) )

for b_{1}, b_{2} being Function of Omega,REAL st ( for w being Element of Omega holds

( ( (RV - (Omega --> K)) . w >= 0 implies b_{1} . w = (RV - (Omega --> K)) . w ) & ( (RV - (Omega --> K)) . w < 0 implies b_{1} . w = 0 ) ) ) & ( for w being Element of Omega holds

( ( (RV - (Omega --> K)) . w >= 0 implies b_{2} . w = (RV - (Omega --> K)) . w ) & ( (RV - (Omega --> K)) . w < 0 implies b_{2} . w = 0 ) ) ) holds

b_{1} = b_{2}

end;
let Sigma be SigmaField of Omega;

let RV be random_variable of Sigma, Borel_Sets ;

let K be Element of 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 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 ) );

ex b

for w being Element of Omega holds

( ( (RV - (Omega --> K)) . w >= 0 implies b

proof end;

uniqueness for b

( ( (RV - (Omega --> K)) . w >= 0 implies b

( ( (RV - (Omega --> K)) . w >= 0 implies b

b

proof 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 Element of REAL

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

( b_{5} = Call-Option (RV,K) iff for w being Element of Omega holds

( ( (RV - (Omega --> K)) . w >= 0 implies b_{5} . w = (RV - (Omega --> K)) . w ) & ( (RV - (Omega --> K)) . w < 0 implies b_{5} . w = 0 ) ) );

for Omega being non empty set

for Sigma being SigmaField of Omega

for RV being random_variable of Sigma, Borel_Sets

for K being Element of REAL

for b

( b

( ( (RV - (Omega --> K)) . w >= 0 implies b

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

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

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

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}

Intersection A1 = {1,2,3,4}

proof end;

theorem :: FINANCE3:16

theorem :: FINANCE3:17

theorem :: FINANCE3:18

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;

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

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

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

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

coherence

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

end;

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

{{},{1,2},{3,4},{1,2,3,4}};

correctness {{},{1,2},{3,4},{1,2,3,4}};

coherence

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

proof end;

:: deftheorem defines Special_SigmaField2 FINANCE3:def 7 :

Special_SigmaField2 = {{},{1,2},{3,4},{1,2,3,4}};

Special_SigmaField2 = {{},{1,2},{3,4},{1,2,3,4}};

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 )

( {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 Special_SigmaField3 & {} in Special_SigmaField3 & {1} in Special_SigmaField3 & {2} in Special_SigmaField3 & {3} in Special_SigmaField3 & {4} in Special_SigmaField3 ) by EnLm1, EnLm2, EnLm3, PROB_1:5, EnLm4, PROB_1:4, ENUMSET1:def 2;

( 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 Special_SigmaField3 & {} in Special_SigmaField3 & {1} in Special_SigmaField3 & {2} in Special_SigmaField3 & {3} in Special_SigmaField3 & {4} in Special_SigmaField3 ) 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

:: Construction of Filtration and Examples

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

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

ex b_{1} being ManySortedSigmaField of I,Sigma st

for s, t being Element of I st s <= t holds

b_{1} . s is Subset of (b_{1} . t)

end;
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 for s, t being Element of I st s <= t holds

it . s is Subset of (it . t);

ex b

for s, t being Element of I st s <= t holds

b

proof 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_{4} being ManySortedSigmaField of I,Sigma holds

( b_{4} is Filtration of I,Sigma iff for s, t being Element of I st s <= t holds

b_{4} . s is Subset of (b_{4} . t) );

for Omega being non empty set

for Sigma being SigmaField of Omega

for I being non empty real-membered set

for b

( b

b

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;

correctness

coherence

Filt . i is SigmaField of Omega;

by KOLMOG01:def 2;

end;
let Sigma be SigmaField of Omega;

let Filt be ManySortedSigmaField of I,Sigma;

let i be Element of I;

correctness

coherence

Filt . i is SigmaField of Omega;

by KOLMOG01:def 2;

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

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

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_{1} being Subset of (bool {1,2,3,4}) holds verum;

;

end;
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 Special_SigmaField1 if k = 1

otherwise Special_SigmaField2 ;

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

;

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

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

coherence

( ( k <= 2 implies Set1_of_SigmaField3 k is Subset of (bool {1,2,3,4}) ) & ( not k <= 2 implies Special_SigmaField3 is Subset of (bool {1,2,3,4}) ) );

consistency

for b_{1} being Subset of (bool {1,2,3,4}) holds verum;

;

end;
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 Special_SigmaField3 ;

correctness Set1_of_SigmaField3 k if k <= 2

otherwise Special_SigmaField3 ;

coherence

( ( k <= 2 implies Set1_of_SigmaField3 k is Subset of (bool {1,2,3,4}) ) & ( not k <= 2 implies Special_SigmaField3 is Subset of (bool {1,2,3,4}) ) );

consistency

for b

;

:: 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 = Special_SigmaField3 ) );

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

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 = Special_SigmaField3 )

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 = Special_SigmaField3 )

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 = Special_SigmaField3 )

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 Special_SigmaField3 ,Sigma2 )

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 Special_SigmaField3 ,Sigma2 )

proof end;

:: The first example of the existence of a random-variable depends

:: on a special underlying sigma-field and given Filtration

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

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

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

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.

:: The next statement is important for the usage of a probability measure

:: with Events depending on SigmaFields in a given filtration.

theorem :: FINANCE3:32

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

ex b_{1} 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_{1} . k = RV & RV is_random_variable_on Sigma,Sigma2 )

end;
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_random_variable_on Sigma,Sigma2 );

existence for k being Element of I ex RV being Function of Omega,Omega2 st

( it . k = RV & RV is_random_variable_on Sigma,Sigma2 );

ex b

for k being Element of I ex RV being Function of Omega,Omega2 st

( b

proof 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_{6} being Function of I,(set_of_random_variables_on (Sigma,Sigma2)) holds

( b_{6} is Stochastic_Process of I,Sigma,Sigma2 iff for k being Element of I ex RV being Function of Omega,Omega2 st

( b_{6} . k = RV & RV is_random_variable_on Sigma,Sigma2 ) );

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

( b

( b

:: Because adapted and predicted stochastic processes are very important for

:: Stochastic finance, we implement them now:

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

coherence

Stoch . k is random_variable of Sigma,Sigma2

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

coherence

Stoch . k is random_variable of Sigma,Sigma2

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

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;

ex b_{1} 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_random_variable_on El_Filtration (i,k),Sigma2

end;
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_random_variable_on El_Filtration (i,k),Sigma2;

existence ex k being Filtration of I,Sigma st

for i being Element of I holds RVProcess (Stoch,i) is_random_variable_on El_Filtration (i,k),Sigma2;

ex b

for i being Element of I holds RVProcess (Stoch,i) is_random_variable_on El_Filtration (i,k),Sigma2

proof 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_{7} being Function of I,(set_of_random_variables_on (Sigma,Sigma2)) holds

( b_{7} 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_random_variable_on El_Filtration (i,k),Sigma2 );

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

( b

for i being Element of I holds RVProcess (Stoch,i) is_random_variable_on El_Filtration (i,k),Sigma2 );

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;

ex b_{1} 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_random_variable_on El_Filtration (i,k),Sigma2

end;
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_random_variable_on El_Filtration (i,k),Sigma2;

existence 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_random_variable_on El_Filtration (i,k),Sigma2;

ex b

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_random_variable_on El_Filtration (i,k),Sigma2

proof 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_{8} being Function of J,(set_of_random_variables_on (Sigma,Sigma2)) holds

( b_{8} 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_random_variable_on El_Filtration (i,k),Sigma2 );

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

( b

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_random_variable_on El_Filtration (i,k),Sigma2 );

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;

end;
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_random_variable_on El_Filtration (i,MyFunc),Sigma2;

for i being Element of I holds RVProcess (Stoch,i) is_random_variable_on El_Filtration (i,MyFunc),Sigma2;

:: 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_random_variable_on El_Filtration (i,MyFunc),Sigma2 );

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_random_variable_on El_Filtration (i,MyFunc),Sigma2 );

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;

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;

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_{1} being Element of REAL holds verum;

;

coherence

( ( k = 3 implies k1 is Element of REAL ) & ( not k = 3 implies k2 is Element of REAL ) );

consistency

for b_{1} being Element of REAL holds verum;

;

end;
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 k1 if ( k = 1 or k = 2 )

otherwise k2;

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

;

func Set4_for_RandomVariable (k1,k2,k) -> Element of REAL equals :Def79: :: FINANCE3:def 19

k1 if k = 3

otherwise k2;

correctness k1 if k = 3

otherwise k2;

coherence

( ( k = 3 implies k1 is Element of REAL ) & ( not k = 3 implies k2 is Element of REAL ) );

consistency

for b

;

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

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

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;

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_{1} being Element of REAL holds verum;

;

end;
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 k2 if k = 2

otherwise Set4_for_RandomVariable (k3,k4,k);

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

;

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

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;

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_{1} being Element of REAL holds verum;

;

end;
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 k1 if k = 1

otherwise Set3_for_RandomVariable (k2,k3,k4,k);

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

;

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

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 )

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 = Special_SigmaField3 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_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets )

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 = Special_SigmaField3 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_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets )

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 = Special_SigmaField3 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_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets )

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 = Special_SigmaField3 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_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets )

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 = Special_SigmaField3 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_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets )

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 = Special_SigmaField3 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_random_variable_on El_Filtration (eli,MyFunc), Borel_Sets )

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 = Special_SigmaField3 holds

for Prob being Function of Sigma,REAL

for i being Element of I ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets

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 = Special_SigmaField3 holds

for Prob being Function of Sigma,REAL

for i being Element of I ex RV being Function of Omega,REAL st RV is_random_variable_on El_Filtration (i,MyFunc), Borel_Sets

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;

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_{1} being Element of set_of_random_variables_on (Sigma,Borel_Sets) holds verum;

end;
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 f2 if i = 2

otherwise f1;

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

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

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

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_{1} being Element of set_of_random_variables_on (Sigma,Borel_Sets) holds verum;

end;
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 FunctionRV1 (i,Sigma,f1,f2,f3) if ( i = 2 or i = 3 )

otherwise f3;

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

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

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 = Special_SigmaField3 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_random_variable_on Sigma, Borel_Sets & RV is_random_variable_on El_Filtration (k,MyFunc), Borel_Sets ) & 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 )

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 = Special_SigmaField3 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_random_variable_on Sigma, Borel_Sets & RV is_random_variable_on El_Filtration (k,MyFunc), Borel_Sets ) & 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;