:: Elementary Introduction to Stochastic Finance in Discrete Time
:: by Peter Jaeger
::
:: Received March 22, 2011
:: Copyright (c) 2011-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINANCE1, NUMBERS, XBOOLE_0, PROB_1, SUBSET_1, FUNCT_1, TARSKI,
RELAT_1, CARD_1, ARYTM_1, CARD_3, PROB_3, NAT_1, ARYTM_3, XXREAL_0,
SERIES_1, EQREL_1, SEQ_1, XXREAL_1, MESFUNC1, RANDOM_1, RANDOM_2,
FUNCOP_1, VALUED_1, FUNCT_7, REAL_1, RANDOM_3;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, XXREAL_0, NAT_1,
XREAL_0, NUMBERS, FUNCT_1, RELSET_1, FUNCT_2, PROB_3, SERIES_1, PROB_1,
MEASURE6, SEQ_1, MESFUNC1, MESFUNC6, RANDOM_1, XXREAL_1, RCOMP_1,
FUNCOP_1, VALUED_1, RANDOM_2;
constructors REAL_1, PROB_3, SERIES_1, BINOP_2, RELSET_1, MEASURE6, RCOMP_1,
MESFUNC1, MESFUNC6, RANDOM_2;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0,
MEMBERED, PROB_1, VALUED_0, XXREAL_0, NAT_1, XCMPLX_0, VALUED_1, FUNCT_2;
requirements SUBSET, NUMERALS, BOOLE, ARITHM, REAL;
definitions TARSKI, FUNCT_1, FUNCT_2;
equalities XXREAL_0, PROB_1, SUBSET_1;
expansions FUNCT_2;
theorems SERIES_1, PROB_1, PROB_3, XBOOLE_0, NAT_1, FUNCT_2, XXREAL_0,
ORDINAL1, TARSKI, XREAL_1, XXREAL_1, MESFUNC1, FINSUB_1, MESFUNC6,
XREAL_0, RANDOM_1, RANDOM_2, FUNCOP_1, VALUED_1, FRECHET, XBOOLE_1,
FUNCT_1;
schemes NAT_1, FUNCT_2, RECDEF_1;
begin
reserve Omega, Omega2 for non empty set;
reserve Sigma, F for SigmaField of Omega;
reserve Sigma2, F2 for SigmaField of Omega2;
notation
let a,r be Real;
synonym halfline_fin(a,r) for [.a,r.[;
end;
definition
let a,r be Real;
redefine func halfline_fin(a,r) -> Subset of REAL; :: redefines halfline_fin (FINANCE1, synonym) → [. (XXREAL_1, definition)
coherence
proof
halfline_fin(a,r) = [.a,r.[;
hence thesis;
end;
end;
theorem
for k being Real holds REAL \ [.k,+infty.[ = ].-infty,k.[
proof
let k be Real;
A1: k in REAL by XREAL_0:def 1;
for x being object holds x in REAL \ [.k,+infty.[ iff x in ].-infty,k.[
proof
let x be object;
hereby assume A2: x in REAL \ [.k,+infty.[;
A3: x in ].-infty,+infty.[ & not x in [.k,+infty.[
by A2,XBOOLE_0:def 5,XXREAL_1:224;
consider y being Element of REAL such that A4:x=y by A2;
y in ].-infty,+infty.[ & not y>= k by A4,A3,XXREAL_1:236;
hence x in ].-infty,k.[ by A4,XXREAL_1:233;
end;
assume A5: x in ].-infty,k.[; then
k in REAL & x in ].-infty,k.[ &
x in {a where a is Element of ExtREAL:
-infty < a & a < k} by XREAL_0:def 1,XXREAL_1:def 4; then
consider a being Element of ExtREAL such that
A6: a=x & -infty < a & a < k;
consider y being Element of ExtREAL such that A7: x=y by A6;
reconsider y as Element of REAL by A1,A6,A7,XXREAL_0:47;
y < k by A5,A7,XXREAL_1:233;
then y in REAL & not y in [.k,+infty.[ by XXREAL_1:236;
hence thesis by A7,XBOOLE_0:def 5;
end;
hence thesis by TARSKI:2;
end;
theorem Th2:
for k being Real holds REAL \ ].-infty,k.[ = [.k,+infty.[
proof
let k be Real;
A1: k in REAL by XREAL_0:def 1;
for x being object holds x in REAL \ ].-infty,k.[ iff x in [.k,+infty.[
proof
let x be object;
hereby assume A2: x in REAL \ ].-infty,k.[;
A3: x in ].-infty,+infty.[ & not x in ].-infty,k.[
by A2,XBOOLE_0:def 5,XXREAL_1:224;
consider y being Element of REAL such that A4:x=y by A2;
A5: y in ].-infty,+infty.[ & not y< k by A4,A3,XXREAL_1:233;
thus x in [.k,+infty.[ by A5,A4,XXREAL_1:236;
end;
assume A6: x in [.k,+infty.[;
then k in REAL & x in [.k,+infty.[ &
x in {a where a is Element of ExtREAL:
k <= a & a < +infty} by XREAL_0:def 1,XXREAL_1:def 2; then
consider a being Element of ExtREAL such that
A7: a=x & k <= a & a < +infty;
consider y being Element of ExtREAL such that A8: x=y by A7;
reconsider y as Element of REAL by A7,A8,A1,XXREAL_0:46;
y >= k by A6,A8,XXREAL_1:236; then
y in REAL & not y in ].-infty,k.[ by XXREAL_1:233;
hence thesis by A8,XBOOLE_0:def 5;
end;
hence thesis by TARSKI:2;
end;
definition
let a,b be Real;
func half_open_sets(a,b) -> SetSequence of REAL means :Def1:
it.0 = halfline_fin(a,b+1) &
for n being Nat holds it.(n+1) = halfline_fin(a,b+1/(n+1));
existence
proof
defpred P[set,set,set] means for x,y being Subset of REAL,s being Nat holds
s = $1 & x = $2 & y = $3 implies y = halfline_fin(a,b+1/(s+1));
A1: for n being Nat for x being Subset of REAL
ex y being Subset of REAL st P[n,x,y]
proof
let n be Nat;
let x be Subset of REAL;
take halfline_fin(a,b+1/(n+1));
thus thesis;
end;
consider F being SetSequence of REAL such that
A2: F.0 = halfline_fin(a,b+1) and
A3: for n being Nat holds P[n,F.n,F.(n+1)] from RECDEF_1:sch 2(A1);
take F;
thus F.0 = halfline_fin(a,b+1) by A2;
let n be Nat;
reconsider n as Element of NAT by ORDINAL1:def 12;
P[n,F.n,F.(n+1)] by A3;
hence thesis;
end;
uniqueness
proof
let S1,S2 be SetSequence of REAL such that
A4: S1.0 = halfline_fin(a,b+1) & for n being Nat holds
S1.(n+1) = halfline_fin(a,b+1/(n+1)) and
A5: S2.0 = halfline_fin(a,b+1) & for n being Nat holds
S2.(n+1) = halfline_fin(a,b+1/(n+1));
defpred P[object] means S1.$1 = S2.$1;
for n being object holds n in NAT implies P[n]
proof
let n be object;
assume n in NAT;
then reconsider n as Element of NAT;
A6: P[0] by A4,A5;
A7: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume S1.k = S2.k;
thus S1.(k+1) = halfline_fin(a,b+1/(k+1)) by A4
.= S2.(k+1) by A5;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A6,A7);
then S1.n = S2.n;
hence thesis;
end;
hence thesis;
end;
end;
definition
mode pricefunction -> Real_Sequence means :Def2:
it.0 = 1 & for n being Element of NAT holds it.n >= 0;
existence
proof
reconsider j = 1 as Element of REAL by XREAL_0:def 1;
take NAT --> j;
thus thesis by FUNCOP_1:7;
end;
end;
notation
let phi,jpi be Real_Sequence;
synonym ElementsOfBuyPortfolio(phi,jpi) for phi (#) jpi;
end;
definition
let phi,jpi be Real_Sequence;
redefine func ElementsOfBuyPortfolio(phi,jpi) -> Real_Sequence; :: redefines ElementsOfBuyPortfolio (FINANCE1, synonym) → (#) (VALUED_1, definition)
coherence
proof
ElementsOfBuyPortfolio(phi,jpi) = phi (#) jpi;
hence thesis;
end;
end;
definition
let d be Nat;
let phi,jpi be Real_Sequence;
func BuyPortfolioExt(phi,jpi,d) -> Real equals
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).d;
coherence;
func BuyPortfolio(phi,jpi,d) -> Real equals
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)^\1).(d-1);
coherence;
end;
definition
let Omega, Omega2 be set;
let Sigma be SigmaField of Omega;
let Sigma2 be SigmaField of Omega2;
let X be Function of Omega, Omega2;
attr X is (Sigma,Sigma2)-random_variable-like means
for x being set st x in Sigma2 holds X"x in Sigma;
end;
Lm1:
for Omega, Omega2 be non empty set,
F be Function of Omega, Omega2,
y be non empty set holds
{z where z is Element of Omega: F.z is Element of y} = F"y
proof
let Omega, Omega2 be non empty set,
F be Function of Omega, Omega2,
y be non empty set;
set D = {z where z is Element of Omega: F.z is Element of y};
for x be object holds x in D iff x in F"y
proof
let x be object;
hereby assume x in D; then
consider z be Element of Omega such that
A1: x = z & F.z is Element of y;
z in Omega; then
A2: z in dom F by FUNCT_2:def 1;
F.z in y by A1; then
z in F"y by FUNCT_1:def 7,A2;
hence x in F"y by A1;
end;
assume x in F"y; then
A3: x in dom F & F.x in y by FUNCT_1:def 7;
thus x in D by A3;
end;
hence thesis by TARSKI:2;
end;
LemmaExample:
for f being Function of Omega, Omega2 st
f = Omega --> the Element of Omega2 holds
f is (F,F2)-random_variable-like
proof
set k = the Element of Omega2;
set z = Omega --> k;
for x being Element of F2 holds z"x in F
proof
let x be Element of F2;
set K=z"x;
A2: dom z = Omega by FUNCT_2:def 1;
per cases;
suppose A3: k in x;
for s being object holds s in K iff s in Omega
proof
let s be object;
thus s in K implies s in Omega;
assume s in Omega; then
s in Omega & z.s in x by A3,FUNCOP_1:7;
hence thesis by A2,FUNCT_1:def 7;
end; then
K = Omega by TARSKI:2; then
K is Element of F by PROB_1:23;
hence thesis;
end;
suppose A4: not k in x;
for r being object holds not r in K
proof
let r be object;
assume r in K; then
r in dom z & z.r in x by FUNCT_1:def 7;
hence thesis by A4,FUNCOP_1:7;
end;
then K={} by XBOOLE_0:def 1;
hence thesis by PROB_1:4;
end;
end;
hence thesis;
end;
registration
let Omega1, Omega2 be non empty set;
let S1 be SigmaField of Omega1;
let S2 be SigmaField of Omega2;
cluster (S1,S2)-random_variable-like for Function of Omega1, Omega2;
existence
proof
set f = Omega1 --> the Element of Omega2;
reconsider f as Function of Omega1, Omega2;
take f;
thus thesis by LemmaExample;
end;
end;
definition
let Omega, Omega2 be non empty set;
let F be SigmaField of Omega;
let F2 be SigmaField of Omega2;
mode random_variable of F, F2 is
(F,F2)-random_variable-like Function of Omega, Omega2;
end;
definition
let Omega, Omega2 be set;
let F be SigmaField of Omega;
let F2 be SigmaField of Omega2;
func set_of_random_variables_on (F,F2) -> set equals
{ M where M is Function of Omega, Omega2:
M is (F,F2)-random_variable-like };
coherence;
end;
registration
let Omega,Omega2,F,F2;
cluster set_of_random_variables_on(F,F2) -> non empty;
coherence
proof
set X = set_of_random_variables_on(F,F2);
ex z being Function of Omega,Omega2 st z is (F,F2)-random_variable-like
proof
set k = the Element of Omega2;
set z = Omega --> k;
A1: z is (F,F2)-random_variable-like iff
(for x being set st x in F2 holds z"x in F);
for x being Element of F2 holds z"x in F
proof
let x be Element of F2;
set K=z"x;
A2: dom z = Omega by FUNCT_2:def 1;
per cases;
suppose A3: k in x;
for s being object holds s in K iff s in Omega
proof
let s be object;
thus s in K implies s in Omega;
assume s in Omega; then
s in Omega & z.s in x by A3,FUNCOP_1:7;
hence thesis by A2,FUNCT_1:def 7;
end; then
K = Omega by TARSKI:2; then
K is Element of F by PROB_1:23;
hence thesis;
end;
suppose A4: not k in x;
for r being object holds not r in K
proof
let r be object;
assume r in K; then
r in dom z & z.r in x by FUNCT_1:def 7;
hence thesis by A4,FUNCOP_1:7;
end;
then K={} by XBOOLE_0:def 1;
hence thesis by PROB_1:4;
end;
end;
hence thesis by A1;
end;
then consider z being Function of Omega,Omega2 such that
A5: z is (F,F2)-random_variable-like;
z in X by A5;
hence thesis;
end;
end;
registration
let Omega,Omega2,F,F2;
cluster set_of_random_variables_on(F,F2) -> functional;
coherence
proof
let x be object;
assume x in set_of_random_variables_on(F,F2);
then consider z being Function of Omega,Omega2 such that
A5: z = x & z is (F,F2)-random_variable-like;
x is Function by A5;
hence thesis;
end;
end;
definition
let Omega, Omega2 be non empty set;
let F be SigmaField of Omega;
let F2 be SigmaField of Omega2;
let X be set such that
A1:X = set_of_random_variables_on(F,F2);
let k be Element of X;
func Change_Element_to_Func(F,F2,k) -> Function of Omega,Omega2 equals
:Def7:
k;
coherence
proof
k in X by A1; then
ex f being Function of Omega,Omega2 st f=k &
f is (F,F2)-random_variable-like by A1;
hence thesis;
end;
end;
definition
let Omega be non empty set;
let F be SigmaField of Omega;
let X be non empty set;
let k be Element of X;
func ElementsOfPortfolioValueProb_fut(F,k) -> Function of Omega,REAL means
:Def8:
for w being Element of Omega holds
it.w = Change_Element_to_Func(F,Borel_Sets,k).w;
existence
proof
deffunc U(Element of Omega) = Change_Element_to_Func(F,Borel_Sets,k).$1;
ex f being Function of Omega,REAL st
for d be Element of Omega holds f.d = U(d) from FUNCT_2:sch 4;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of Omega,REAL;
assume that
A1: for w being Element of Omega holds
f1.w = Change_Element_to_Func(F,Borel_Sets,k).w and
A2: for w being Element of Omega holds
f2.w = Change_Element_to_Func(F,Borel_Sets,k).w;
let w be Element of Omega;
f1.w = Change_Element_to_Func(F,Borel_Sets,k).w &
f2.w = Change_Element_to_Func(F,Borel_Sets,k).w by A1,A2;
hence thesis;
end;
end;
definition
let p be Nat;
let Omega, Omega2 be non empty set;
let F be SigmaField of Omega;
let F2 be SigmaField of Omega2;
let X be set such that
A1: X = set_of_random_variables_on(F,F2);
let G be sequence of X;
func Element_Of(F,F2,G,p) -> Function of Omega,Omega2 equals :Def9:
G.p;
coherence
proof
reconsider p as Element of NAT by ORDINAL1:def 12;
G.p in {f where f is Function of Omega,Omega2:
f is (F,F2)-random_variable-like} by A1;
then ex f being Function of Omega,Omega2 st
f=G.p & f is (F,F2)-random_variable-like;
hence thesis;
end;
end;
definition
let Omega be non empty set;
let F be SigmaField of Omega;
let X be non empty set;
let w be Element of Omega;
let G be sequence of X;
let phi be Real_Sequence;
func ElementsOfPortfolioValue_fut(phi,F,w,G) -> Real_Sequence means
:Def10:
for n being Element of NAT holds
it.n = ElementsOfPortfolioValueProb_fut(F,G.n).w * phi.n;
existence
proof
deffunc U(Element of NAT) =
In(ElementsOfPortfolioValueProb_fut(F,G.$1).w * phi.$1,REAL);
consider f being Real_Sequence such that
A1: for d be Element of NAT holds f.d = U(d) from FUNCT_2:sch 4;
take f;
let n be Element of NAT;
f.n = U(n) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Real_Sequence;
assume that
A2: for d being Element of NAT holds f1.d =
ElementsOfPortfolioValueProb_fut(F,G.d).w * phi.d and
A3: for d being Element of NAT holds f2.d =
ElementsOfPortfolioValueProb_fut(F,G.d).w * phi.d;
let d be Element of NAT;
f1.d = ElementsOfPortfolioValueProb_fut(F,G.d).w * phi.d &
f2.d = ElementsOfPortfolioValueProb_fut(F,G.d).w * phi.d by A2,A3;
hence thesis;
end;
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;
func PortfolioValueFutExt(d,phi,F,G,w) -> Real equals
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).d;
coherence;
func PortfolioValueFut(d,phi,F,G,w) -> Real equals
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).(d-1);
coherence;
end;
registration
cluster non empty for Element of Borel_Sets;
existence
proof
consider m being Real such that A1: m>-infty;
set L = halfline(m);
set LL = Family_of_halflines;
A2: L is non empty by A1,XXREAL_1:33;
m in REAL by XREAL_0:def 1; then
A3: L in LL;
Family_of_halflines is Subset of Borel_Sets by PROB_1:def 9;
hence thesis by A3,A2;
end;
end;
theorem Th3:
for k being Real holds
[.k,+infty.[ is Element of Borel_Sets &
].-infty,k.[ is Element of Borel_Sets
proof
let k be Real;
A1: k in REAL by XREAL_0:def 1;
set R = ].-infty,k.[;
A2: ].-infty,k.[ in Borel_Sets
proof
set L = halfline(k);
A3: L in Family_of_halflines & L=].-infty,k.[ by A1;
Family_of_halflines c= sigma(Family_of_halflines) by PROB_1:def 9;
hence thesis by A3;
end; then
R` in Borel_Sets by PROB_1:def 1;
hence thesis by Th2,A2;
end;
theorem Th4:
for k1,k2 being Real holds
[.k2,k1.[ is Element of Borel_Sets
proof
let k1,k2 be Real;
set R = ].-infty,k2.[;
k1 in REAL & k2 in REAL by XREAL_0:def 1; then
A1: -infty<k2 & k1<+infty by XXREAL_0:9,12;
A2: REAL \ ].-infty,k2.[=[.k2,+infty.[ by Th2;
R` is Element of Borel_Sets &
].-infty,k1.[ is Element of Borel_Sets &
[.k1,+infty.[ is Element of Borel_Sets by Th3,A2; then
].-infty,k1.[ /\ R` is Element of Borel_Sets by FINSUB_1:def 2; then
].-infty,k1.[ /\ [.k2,+infty.[ is Element of Borel_Sets by Th2;
hence thesis by A1,XXREAL_1:154;
end;
theorem Th5:
for a,b being Real holds
Intersection half_open_sets(a,b) is Element of Borel_Sets
proof
let a,b be Real;
for n being Nat holds
(Complement half_open_sets(a,b)).n is Element of Borel_Sets
proof
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
(half_open_sets(a,b).nn)` is Element of Borel_Sets
proof
half_open_sets(a,b).n is Element of Borel_Sets
proof
per cases by NAT_1:6;
suppose A1: n=0;
half_open_sets(a,b).0=halfline_fin(a,b+1) by Def1;
hence thesis by A1,Th4;
end;
suppose ex k being Nat st n = k + 1; then
consider k being Nat such that A2: n=k+1;
reconsider k as Element of NAT by ORDINAL1:def 12;
half_open_sets(a,b).(k+1) =
halfline_fin(a,b+(1/(k+1))) by Def1;
hence thesis by A2,Th4;
end;
end;
hence thesis by PROB_1:def 1;
end;
hence thesis by PROB_1:def 2;
end; then
Complement half_open_sets(a,b)
is SetSequence of Borel_Sets by PROB_1:25; then
Union Complement half_open_sets(a,b)
is Element of Borel_Sets by PROB_1:26;
hence thesis by PROB_1:def 1;
end;
theorem Th6:
for a,b being Real holds
Intersection half_open_sets(a,b) = [.a,b.]
proof
let a,b be Real;
A1: for c be set holds
not c in [.a,b.] implies not c in Intersection half_open_sets(a,b)
proof
let c be set;
assume
A2: not c in [.a,b.];
per cases by A2;
suppose not c in REAL;
hence thesis;
end;
suppose
A3: c in REAL & not c in [.a,b.];
then reconsider c as Element of REAL;
A4: not c in {q where q is Element of ExtREAL:
a <= q & q <= b} by A3,XXREAL_1:def 1;
A5: a > c or c > b
proof
reconsider q = c as Element of ExtREAL by XXREAL_0:def 1;
not (c = q & a <= c & c <= b) by A4;
hence thesis;
end;
per cases by A5;
suppose A6: a > c;
not for n being Element of NAT holds c in half_open_sets(a,b).n
proof
take n = 0;
c in half_open_sets(a,b).0 implies
c in halfline_fin(a,b+1) by Def1; then
c in half_open_sets(a,b).0 implies
c in {q where q is Element of ExtREAL:
a <= q & q < b+1} by XXREAL_1:def 2; then
ex q being Element of ExtREAL st c in half_open_sets(a,b).0 implies
c = q & a <= q & q < b+1;
hence thesis by A6;
end;
hence thesis by PROB_1:13;
end;
suppose c > b;
then consider n being Nat such that
A7: 1/n<(c-b) & n > 0 by FRECHET:36,XREAL_1:50;
A8: (1/n)+b<(c-b)+b by A7,XREAL_1:6;
c in Intersection half_open_sets(a,b) implies not b+1/n<c
proof
assume c in Intersection half_open_sets(a,b); then
c in half_open_sets(a,b).(n+1) by PROB_1:13; then
c in [.a,b+1/(n+1).[ by Def1; then
c in {q where q is Element of ExtREAL:
a<=q & q<b+1/(n+1)} by XXREAL_1:def 2; then
consider q being Element of ExtREAL such that
A9: c = q & a<=q & q < b+1/(n+1);
reconsider a=1 as Element of NAT;
n*1<(n+1)*1 by NAT_1:13; then
A10: a/(n+1)<a/n by A7,XREAL_1:106;
b+1/(n+1)<b+1/n by A10,XREAL_1:6;
hence thesis by A9,XXREAL_0:2;
end;
hence thesis by A8;
end;
end;
end;
A11:for c be set holds c in [.a,b.] implies
c in Intersection half_open_sets(a,b)
proof
let c be set;
c in [.a,b.] implies
for n being Nat holds c in half_open_sets(a,b).n
proof
assume A12: c in [.a,b.];
let n be Nat;
A13: b<b+1 by XREAL_1:29;
[.a,b.] c= half_open_sets(a,b).n
proof
per cases;
suppose A14: n=0;
half_open_sets(a,b).0=halfline_fin(a,b+1) by Def1;
hence thesis by A14,A13,XXREAL_1:43;
end;
suppose n>0; then
consider k being Nat such that
A15: n=k+1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
A16: half_open_sets(a,b).(k+1) = halfline_fin(a,b+1/(k+1)) by Def1;
b<b+1/n by A15,XREAL_1:29;
hence thesis by A16,A15,XXREAL_1:43;
end;
end;
hence thesis by A12;
end;
hence thesis by PROB_1:13;
end;
for c being object holds
c in Intersection half_open_sets(a,b) iff c in [.a,b.] by A11,A1;
hence thesis by TARSKI:2;
end;
theorem
for a,b being Real, n being Nat holds
(Partial_Intersection half_open_sets(a,b)).n is Element of Borel_Sets
proof
let a,b be Real;
defpred J[Nat] means
(Partial_Intersection half_open_sets(a,b)).$1 is Element of Borel_Sets;
A1: J[0]
proof
(Partial_Intersection half_open_sets(a,b)).0 =
half_open_sets(a,b).0 by PROB_3:def 1; then
(Partial_Intersection half_open_sets(a,b)).0 =
halfline_fin(a,(b+1)) by Def1;
hence thesis by Th4;
end;
A2: for k being Nat st J[k] holds J[k+1]
proof
let k be Nat;
assume A3: (Partial_Intersection half_open_sets(a,b)).k
is Element of Borel_Sets;
reconsider k as Element of NAT by ORDINAL1:def 12;
(Partial_Intersection half_open_sets(a,b)).(k+1) =
(Partial_Intersection half_open_sets(a,b)).k /\
half_open_sets(a,b).(k+1) by PROB_3:def 1; then
A4: (Partial_Intersection half_open_sets(a,b)).(k+1) =
(Partial_Intersection half_open_sets(a,b)).k /\
halfline_fin(a,(b+1/(k+1))) by Def1;
[.a,b+1/(k+1).[ is Element of Borel_Sets &
(Partial_Intersection half_open_sets(a,b)).k
is Element of Borel_Sets by Th4,A3;
hence thesis by A4,FINSUB_1:def 2;
end;
for k being Nat holds J[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th8:
for k1,k2 being Real holds [.k2,k1.] is Element of Borel_Sets
proof
let a,b be Real;
Intersection half_open_sets(b,a) = [.b,a.] by Th6;
hence thesis by Th5;
end;
theorem Th9:
for X being Function of Omega,REAL st
X is (Sigma,Borel_Sets)-random_variable-like holds
(for k being Real holds
{w where w is Element of Omega: X.w >=k} is Element of Sigma &
{w where w is Element of Omega: X.w <k} is Element of Sigma) &
(for k1,k2 being Real st k1<k2 holds
{w where w is Element of Omega: k1 <= X.w & X.w < k2} is Element of Sigma) &
(for k1,k2 being Real st k1<=k2 holds
{w where w is Element of Omega: k1 <= X.w & X.w <= k2} is Element of Sigma) &
(for r being Real holds
less_dom(X,r) = {w where w is Element of Omega: X.w <r}) &
(for r being Real holds
great_eq_dom(X,r) = {w where w is Element of Omega: X.w >=r}) &
(for r being Real holds
eq_dom(X,r) = {w where w is Element of Omega: X.w =r}) &
(for r being Real holds eq_dom(X,r) is Element of Sigma)
proof
let X be Function of Omega,REAL;
assume A1: X is (Sigma,Borel_Sets)-random_variable-like;
A2: for k being Real holds
{w where w is Element of Omega: X.w >=k} is Element of Sigma &
{w where w is Element of Omega: X.w <k} is Element of Sigma
proof
let k be Real;
A3: for q being set holds
(ex w being Element of Omega st q=w & X.w >=k) iff
(ex w being Element of Omega st q=w & X.w in [.k,+infty.])
proof
let q be set;
now assume ex w being Element of Omega st q=w & X.w in [.k,+infty.]; then
consider w being Element of Omega such that
A4: q=w & X.w in [.k,+infty.];
X.w in {z where z is Element of ExtREAL: k<=z & z<=+infty}
by A4,XXREAL_1:def 1; then
ex z being Element of ExtREAL st X.w=z & k<=z & z<=+infty;
hence ex w being Element of Omega st q=w & X.w >=k by A4;
end;
hence thesis by XXREAL_1:219;
end;
A5:for x being object holds
x in {w where w is Element of Omega:X.w >=k} iff
x in {w where w is Element of Omega:X.w in [.k,+infty.[}
proof
let x be object;
x in {w where w is Element of Omega:X.w >=k} iff
ex w being Element of Omega st x=w & X.w >=k; then
A6: x in {w where w is Element of Omega:X.w >=k} iff
ex w being Element of Omega st x=w & X.w in [.k,+infty.] by A3;
x in {w where w is Element of Omega:X.w in [.k,+infty.]} iff
x in {w where w is Element of Omega:X.w in [.k,+infty.[}
proof
hereby assume
x in {w where w is Element of Omega:X.w in [.k,+infty.]};
then consider w being Element of Omega such that
A7: w=x & X.w in [.k,+infty.];
X.w in {a where a is Element of ExtREAL: k<=a & a<=+infty}
by A7,XXREAL_1:def 1; then
consider a being Element of ExtREAL such that
A8: X.w = a & k<=a & a<=+infty;
A9: X.w = a & k<=a & a<+infty by A8,XXREAL_0:9;
{z where z is Element of ExtREAL: k<=z & z <+infty} =
[.k,+infty.[ by XXREAL_1:def 2; then
X.w in [.k,+infty.[ by A9;
hence x in {g where g is Element of Omega:X.g in [.k,+infty.[} by A7;
end;
assume x in {w where w is Element of Omega:X.w in [.k,+infty.[}; then
consider w being Element of Omega such that
A10: w=x & X.w in [.k,+infty.[;
w=x & X.w in {u where u is Element of ExtREAL: k<=u &
u<+infty} by A10,XXREAL_1:def 2; then
w=x & ex u being Element of ExtREAL st u=X.w & k<=u & u<+infty;
then w=x & X.w in {u where u is Element of ExtREAL: k<=u & u<=+infty};
then w=x & X.w in [.k,+infty.] by XXREAL_1:def 1;
hence thesis;
end;
hence thesis by A6;
end;
k in REAL by XREAL_0:def 1; then
A11: [.k,+infty.[ is non empty by XXREAL_0:9,XXREAL_1:31;
A12: {w where w is Element of Omega:X.w >=k} =
{w where w is Element of Omega:X.w is Element of [.k,+infty.[}
proof
{w where w is Element of Omega:X.w in [.k,+infty.[} =
{w where w is Element of Omega:X.w is Element of [.k,+infty.[}
proof
for x being object holds
x in {w where w is Element of Omega:X.w in [.k,+infty.[} iff
x in {w where w is Element of Omega:X.w is Element of [.k,+infty.[}
proof
let x be object;
hereby assume
x in {w where w is Element of Omega:X.w in [.k,+infty.[}; then
ex w being Element of Omega st w = x & X.w in [.k,+infty.[;
hence
x in {w where w is Element of Omega:X.w is Element of [.k,+infty.[};
end;
assume
x in {w where w is Element of Omega:X.w is Element of [.k,+infty.[};
then consider w being Element of Omega such that
A13: w = x & X.w is Element of [.k,+infty.[;
thus thesis by A13,A11;
end;
hence thesis by TARSKI:2;
end;
hence thesis by A5,TARSKI:2;
end;
A14: [.k,+infty.[ is Element of Borel_Sets &
].-infty,k.[ is Element of Borel_Sets by Th3;
A15: {w where w is Element of Omega: X.w is Element of [.k,+infty.[}
= X"([.k,+infty.[) by Lm1,A11;
A16: for q being set holds
(ex w being Element of Omega st q=w & X.w <k) iff
(ex w being Element of Omega st q=w & X.w in [.-infty,k.[)
proof
let q be set;
now assume ex w being Element of Omega st q=w & X.w in [.-infty,k.[; then
consider w being Element of Omega such that
A17: q=w & X.w in [.-infty,k.[;
X.w in {z where z is Element of ExtREAL:-infty<=z & z<k}
by A17,XXREAL_1:def 2; then
ex z being Element of ExtREAL st X.w=z & -infty<=z & z<k;
hence ex w being Element of Omega st q=w & X.w <k by A17;
end;
hence thesis by XXREAL_1:221;
end;
for x being object holds
x in {w where w is Element of Omega:X.w <k} iff
x in {w where w is Element of Omega:X.w in ].-infty,k.[}
proof
let x be object;
x in {w where w is Element of Omega:X.w <k} iff
ex w being Element of Omega st x=w & X.w <k; then
A18: x in {w where w is Element of Omega:X.w <k} iff
ex w being Element of Omega st x=w & X.w in [.-infty,k.[ by A16;
x in {w where w is Element of Omega:X.w in [.-infty,k.[} iff
x in {w where w is Element of Omega:X.w in ].-infty,k.[}
proof
hereby assume
x in {w where w is Element of Omega:X.w in [.-infty,k.[}; then
consider w being Element of Omega such that
A19: w=x & X.w in [.-infty,k.[;
X.w in {a where a is Element of ExtREAL: -infty<=a & a<k}
by A19,XXREAL_1:def 2; then
consider a being Element of ExtREAL such that
A20: X.w = a & -infty<=a & a<k;
A21: X.w = a & -infty<a & a<k by A20,XXREAL_0:12;
{z where z is Element of ExtREAL: -infty<z & z<k} =
].-infty,k.[ by XXREAL_1:def 4; then
X.w in ].-infty,k.[ by A21;
hence x in {g where g is Element of Omega:X.g in ].-infty,k.[} by A19;
end;
assume x in {w where w is Element of Omega:X.w in ].-infty,k.[}; then
consider w being Element of Omega such that
A22: w=x & X.w in ].-infty,k.[;
w=x & X.w in {u where u is Element of ExtREAL: -infty<u & u<k}
by A22,XXREAL_1:def 4; then
w=x & ex u being Element of ExtREAL st u=X.w & -infty<u & u<k;
then w=x &
X.w in {u where u is Element of ExtREAL: -infty<=u & u<k}; then
w=x & X.w in [.-infty,k.[ by XXREAL_1:def 2;
hence thesis;
end;
hence thesis by A18;
end; then
A23: {w where w is Element of Omega:X.w <k} =
{w where w is Element of Omega:X.w in ].-infty,k.[} by TARSKI:2;
{w where w is Element of Omega:X.w <k} is Element of Sigma
proof
A24: [.k,+infty.[ is Element of Borel_Sets &
].-infty,k.[ is Element of Borel_Sets by Th3;
k in REAL by XREAL_0:def 1; then
A25: ].-infty,k.[ is non empty by XXREAL_0:12,XXREAL_1:33; then
A26: {w where w is Element of Omega:X.w is Element of ].-infty,k.[}
= X"(].-infty,k.[) by Lm1;
for x being object holds
x in {w where w is Element of Omega: X.w in ].-infty,k.[} iff
x in {w where w is Element of Omega: X.w is Element of ].-infty,k.[}
proof
let x be object;
hereby assume
x in {w where w is Element of Omega:X.w in ].-infty,k.[}; then
ex w being Element of Omega st w = x & X.w in ].-infty,k.[;
hence
x in {w where w is Element of Omega:X.w is Element of ].-infty,k.[};
end;
assume
x in {w where w is Element of Omega:X.w is Element of ].-infty,k.[};
then consider w being Element of Omega such that
A27: w = x & X.w is Element of ].-infty,k.[;
thus thesis by A27,A25;
end; then
{w where w is Element of Omega:X.w <k} =
{w where w is Element of Omega:X.w is Element of ].-infty,k.[}
by A23,TARSKI:2
.= X"(].-infty,k.[) by A26;
hence thesis by A24,A1;
end;
hence thesis by A14,A1,A12,A15;
end;
A28: for k1,k2 being Real st k1<k2 holds
{w where w is Element of Omega: k1 <= X.w & X.w < k2} is Element of Sigma
proof
let k1,k2 be Real;
assume A29: k1<k2; then
A30: [.k1,k2.[ is non empty by XXREAL_1:31;
{w where w is Element of Omega:k1 <= X.w & X.w < k2} is Element of Sigma
proof
for x being object holds
x in {w where w is Element of Omega:k1 <= X.w & X.w < k2} iff
x in {w where w is Element of Omega:X.w is Element of [.k1,k2.[}
proof
let x be object;
hereby assume x in {w where w is Element of Omega:k1 <= X.w & X.w < k2};
then consider w being Element of Omega such that
A31: x=w & k1 <= X.w & X.w < k2;
reconsider a=X.w as Element of ExtREAL by XXREAL_0:def 1;
a=X.w; then
X.w in {z where z is Element of ExtREAL: k1 <= z & z < k2} by A31; then
X.w is Element of [.k1,k2.[ by XXREAL_1:def 2;
hence x in {w1 where w1 is Element of Omega:
X.w1 is Element of [.k1,k2.[} by A31;
end;
assume x in {w where w is Element of Omega:
X.w is Element of [.k1,k2.[}; then
consider w being Element of Omega such that
A32: x=w & X.w is Element of [.k1,k2.[;
A33: [.k1,k2.[ is non empty by A29,XXREAL_1:31;
X.w in [.k1,k2.[ by A32,A33; then
X.w in {a where a is Element of ExtREAL:
k1 <=a & a <k2} by XXREAL_1:def 2; then
ex a being Element of ExtREAL st a=X.w & k1 <=a & a <k2;
hence thesis by A32;
end; then
A34: {w where w is Element of Omega:k1 <= X.w & X.w < k2} =
{w where w is Element of Omega:X.w is Element of [.k1,k2.[} by TARSKI:2;
A35: [.k2,k1.[ is Element of Borel_Sets &
[.k1,k2.[ is Element of Borel_Sets by Th4;
{w where w is Element of Omega: X.w is Element of [.k1,k2.[}
= X"([.k1,k2.[) by Lm1,A30;
hence thesis by A1,A34,A35;
end;
hence thesis;
end;
A36: for k1,k2 being Real st k1<=k2 holds
{w where w is Element of Omega: k1 <= X.w & X.w <= k2} is Element of Sigma
proof
let k1,k2 be Real;
assume A37: k1<=k2; then
A38: [.k1,k2.] is non empty by XXREAL_1:30;
for x being object holds
(x in {w where w is Element of Omega:k1 <= X.w & X.w <= k2} iff
x in {w where w is Element of Omega:X.w is Element of [.k1,k2.]})
proof
let x be object;
hereby assume x in {w where w is Element of Omega:k1 <= X.w & X.w <= k2};
then consider w being Element of Omega such that
A39: x=w & k1 <= X.w & X.w <= k2;
reconsider a=X.w as Element of ExtREAL by XXREAL_0:def 1;
a=X.w; then
X.w in {z where z is Element of ExtREAL:
k1 <= z & z <= k2} by A39; then
X.w is Element of [.k1,k2.] by XXREAL_1:def 1;
hence x in {w1 where w1 is Element of Omega:
X.w1 is Element of [.k1,k2.]} by A39;
end;
assume x in {w where w is Element of Omega:
X.w is Element of [.k1,k2.]}; then
consider w being Element of Omega such that
A40: x=w & X.w is Element of [.k1,k2.];
A41: [.k1,k2.] is non empty by A37,XXREAL_1:30;
X.w in [.k1,k2.] by A40,A41; then
X.w in {a where a is Element of ExtREAL:
k1 <=a & a <=k2} by XXREAL_1:def 1; then
ex a being Element of ExtREAL st a=X.w & k1 <=a & a <=k2;
hence thesis by A40;
end; then
A42: {w where w is Element of Omega:k1 <= X.w & X.w <= k2} =
{w where w is Element of Omega:X.w is Element of [.k1,k2.]} by TARSKI:2;
A43: [.k1,k2.[ is Element of Borel_Sets &
[.k1,k2.] is Element of Borel_Sets by Th8,Th4;
{w where w is Element of Omega: X.w is Element of [.k1,k2.]}
= X"([.k1,k2.]) by Lm1,A38;
hence thesis by A1,A42,A43;
end;
A44: for r being Real holds
less_dom(X,r) = {w where w is Element of Omega: X.w <r}
proof
let r be Real;
for x being object holds
x in less_dom(X,r) iff x in {w where w is Element of Omega:X.w <r}
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
x in less_dom(X,r) iff x in dom X & X.xx < r by MESFUNC1:def 11; then
x in less_dom(X,r) iff x in Omega & X.xx < r by FUNCT_2:def 1; then
x in less_dom(X,r) iff ex q being Element of Omega st q=x & X.q<r;
hence thesis;
end;
hence thesis by TARSKI:2;
end;
A45: for r being Real holds
great_eq_dom(X,r) = {w where w is Element of Omega: X.w >=r}
proof
let r be Real;
for x being object holds x in great_eq_dom(X,r) iff
x in {w where w is Element of Omega:X.w >=r}
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
x in great_eq_dom(X,r) iff x in dom X & X.xx >= r by MESFUNC1:def 14; then
x in great_eq_dom(X,r) iff x in Omega & X.xx >= r by FUNCT_2:def 1; then
x in great_eq_dom(X,r) iff ex q being Element of Omega st q=x & X.q>=r;
hence thesis;
end;
hence thesis by TARSKI:2;
end;
A46: for r being Real holds
eq_dom(X,r) = {w where w is Element of Omega: X.w = r}
proof
let r be Real;
for x being object holds x in eq_dom(X,r) iff
x in {w where w is Element of Omega:X.w =r}
proof
let x be object;
x in eq_dom(X,r) iff x in dom X & X.x = r by MESFUNC1:def 15; then
x in eq_dom(X,r) iff x in Omega & X.x = r by FUNCT_2:def 1; then
x in eq_dom(X,r) iff (ex q being Element of Omega st q=x & X.q=r);
hence thesis;
end;
hence thesis by TARSKI:2;
end;
for r being Real holds eq_dom(X,r) is Element of Sigma
proof
let r be Real;
for x being object holds
x in {w where w is Element of Omega: r <= X.w & X.w <= r} iff
x in {w where w is Element of Omega: X.w=r}
proof
let x be object;
x in {w where w is Element of Omega: r <= X.w & X.w <= r} iff
ex q being Element of Omega st x=q & r<=X.q & X.q<=r; then
x in {w where w is Element of Omega: r <= X.w & X.w <= r} iff
ex q being Element of Omega st x=q & X.q=r by XXREAL_0:1;
hence thesis;
end; then
{w where w is Element of Omega: r <= X.w & X.w <= r} =
{w where w is Element of Omega: X.w=r} by TARSKI:2; then
{w where w is Element of Omega: X.w=r} is Element of Sigma by A36;
hence thesis by A46;
end;
hence thesis by A2,A28,A36,A44,A45,A46;
end;
theorem
for s being Real, f being Function of Omega, REAL st f = Omega --> s holds
f is (Sigma,Borel_Sets)-random_variable-like
proof
let s be Real;
let X be Function of Omega, REAL;
assume A0: X = Omega --> s;
X is (Sigma,Borel_Sets)-random_variable-like
proof
let x be set;
per cases;
suppose
A1: s in x;
for q being object holds
q in {w where w is Element of Omega: X.w is Element of x} iff q in Omega
proof
let q be object;
hereby assume
q in {w where w is Element of Omega: X.w is Element of x}; then
ex w being Element of Omega st w=q & X.w is Element of x;
hence q in Omega;
end;
assume q in Omega;
then reconsider w = q as Element of Omega;
X.w is Element of x by A1,FUNCOP_1:7,A0;
hence thesis;
end; then
A2: {w where w is Element of Omega: X.w is Element of x}=Omega by TARSKI:2;
x is non empty by A1; then
{w where w is Element of Omega: X.w is Element of x}=X"x by Lm1; then
X"x = Omega by A2; then
X"x is Element of Sigma by PROB_1:23;
hence thesis;
end;
suppose
A3: not s in x;
for q being object holds q in X"x iff q in {}
proof
let q be object;
now assume q in X"x; then
q in dom X & X.q in x by FUNCT_1:def 7;
hence q in {} by A3,FUNCOP_1:7,A0;
end;
hence thesis;
end; then
X"x = {} by TARSKI:2; then
X"x is Element of Sigma by PROB_1:22;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th11:
for phi being Real_Sequence, jpi being pricefunction,
d being Nat st d>0 holds
BuyPortfolioExt(phi,jpi,d) = phi.0 + BuyPortfolio(phi,jpi,d)
proof
let phi be Real_Sequence, jpi be pricefunction,
d be Nat;
assume d>0; then
A1: d-1 is Element of NAT by NAT_1:20;
defpred J[Nat] means
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).($1+1) =
phi.0 + Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)^\1).$1;
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).(0+1) =
phi.0 + Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)^\1).0
proof
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).(0+1) =
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).0+
ElementsOfBuyPortfolio(phi,jpi).1 by SERIES_1:def 1; then
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).(0+1) =
ElementsOfBuyPortfolio(phi,jpi).0+
ElementsOfBuyPortfolio(phi,jpi).1 by SERIES_1:def 1; then
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).(0+1) =
ElementsOfBuyPortfolio(phi,jpi).0+
(ElementsOfBuyPortfolio(phi,jpi)^\1).0 by NAT_1:def 3; then
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).(0+1) =
ElementsOfBuyPortfolio(phi,jpi).0+
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)^\1).0
by SERIES_1:def 1; then
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).(0+1) =
(phi.0 * jpi.0)+
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)^\1).0 by VALUED_1:5; then
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).(0+1) =
(phi.0 * 1)+
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)^\1).0 by Def2;
hence thesis;
end; then
A2: J[0];
A3: for k being Nat st J[k] holds J[k+1]
proof
let k be Nat;
assume A4: Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).(k+1) =
phi.0 + Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)^\1).k;
reconsider k as Element of NAT by ORDINAL1:def 12;
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).((k+1)+1) =
(phi.0 + Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)^\1).k) +
ElementsOfBuyPortfolio(phi,jpi).((k+1)+1) by A4,SERIES_1:def 1; then
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).((k+1)+1) =
(phi.0 + Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)^\1).k) +
(ElementsOfBuyPortfolio(phi,jpi)^\1).(k+1) by NAT_1:def 3; then
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).((k+1)+1) =
phi.0 + (Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)^\1).k +
(ElementsOfBuyPortfolio(phi,jpi)^\1).(k+1));
hence thesis by SERIES_1:def 1;
end;
for k being Nat holds J[k] from NAT_1:sch 2(A2,A3); then
Partial_Sums(ElementsOfBuyPortfolio(phi,jpi)).((d-1)+1) =
phi.0 + BuyPortfolio(phi,jpi,d) by A1;
hence thesis;
end;
theorem Th12:
for d being Nat st d>0 holds
for r being Real
for phi being Real_Sequence
for G being sequence of set_of_random_variables_on(F,Borel_Sets) st
Element_Of(F,Borel_Sets,G,0) = Omega-->1+r holds
for w being Element of Omega holds
PortfolioValueFutExt(d,phi,F,G,w)
= ((1+r) * phi.0) + PortfolioValueFut(d,phi,F,G,w)
proof
let d be Nat;
assume A1: d>0;
let r be Real;
let phi be Real_Sequence;
set X = set_of_random_variables_on(F,Borel_Sets);
let G be sequence of X;
assume A2: Element_Of(F,Borel_Sets,G,0) = Omega-->1+r;
let w be Element of Omega;
A3: (d-1) is Element of NAT by A1,NAT_1:20;
defpred J[Nat] means
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).($1+1) =
((1+r) * phi.0) +
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).$1;
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).(0+1) =
((1+r) * phi.0) +
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).0
proof
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).(0+1) =
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).0 +
ElementsOfPortfolioValue_fut(phi,F,w,G).1
by SERIES_1:def 1; then
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).(0+1) =
ElementsOfPortfolioValue_fut(phi,F,w,G).0 +
ElementsOfPortfolioValue_fut(phi,F,w,G).1
by SERIES_1:def 1; then
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).(0+1) =
ElementsOfPortfolioValue_fut(phi,F,w,G).0 +
(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).0
by NAT_1:def 3; then
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).(0+1) =
ElementsOfPortfolioValue_fut(phi,F,w,G).0 +
Partial_Sums((ElementsOfPortfolioValue_fut(phi,F,w,G)^\1)).0
by SERIES_1:def 1; then
consider d being Element of NAT such that
A4: d=0 & Partial_Sums(
ElementsOfPortfolioValue_fut(phi,F,w,G)).(d+1) =
ElementsOfPortfolioValue_fut(phi,F,w,G).d +
Partial_Sums((ElementsOfPortfolioValue_fut(phi,F,w,G)^\1)).d;
A5: Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).(d+1) =
(ElementsOfPortfolioValueProb_fut(F,G.d).w * phi.d) +
Partial_Sums((ElementsOfPortfolioValue_fut(phi,F,w,G)^\1)).d
by A4,Def10;
set g = G.d;
set g2=Change_Element_to_Func(F,Borel_Sets,g);
g2.w=1+r
proof
Element_Of(F,Borel_Sets,G,0) = G.0 & g2=G.0 &
Element_Of(F,Borel_Sets,G,0) = Omega-->1+r by A2,Def9,Def7,A4;
hence thesis by FUNCOP_1:7;
end;
hence thesis by A4,A5,Def8;
end; then
A6: J[0];
A7: for k being Nat st J[k] holds J[k+1]
proof
let k be Nat;
assume A8:
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).(k+1) =
((1+r) * phi.0) +
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).k;
reconsider k as Element of NAT by ORDINAL1:def 12;
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).((k+1)+1)
= ((1+r) * phi.0) +
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).k
+ ElementsOfPortfolioValue_fut(phi,F,w,G).((k+1)+1)
by A8,SERIES_1:def 1; then
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).((k+1)+1)
= ((1+r) * phi.0) +
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).k
+ (ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).(k+1)
by NAT_1:def 3; then
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).((k+1)+1)
= ((1+r) * phi.0) +
(Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).k
+ (ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).(k+1));
hence thesis by SERIES_1:def 1;
end;
for k being Nat holds J[k] from NAT_1:sch 2(A6,A7); then
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)).(d-1+1) =
((1+r) * phi.0) +
Partial_Sums(ElementsOfPortfolioValue_fut(phi,F,w,G)^\1).((d-1)) by A3;
hence thesis;
end;
theorem Th13:
for d being Nat st d>0 holds
for r being Real st r>-1 holds
for phi being Real_Sequence,
jpi being pricefunction holds
for G being sequence of set_of_random_variables_on(F,Borel_Sets) st
Element_Of(F,Borel_Sets,G,0) = Omega-->1+r holds
for w being Element of Omega holds
BuyPortfolioExt(phi,jpi,d)<=0 implies
(PortfolioValueFutExt(d,phi,F,G,w) <=
PortfolioValueFut(d,phi,F,G,w) - (1+r)*BuyPortfolio(phi,jpi,d))
proof
let d be Nat;
assume A1: d>0;
let r be Real;
assume A2: r>-1;
let phi be Real_Sequence, jpi be pricefunction;
set X = set_of_random_variables_on(F,Borel_Sets);
let G be sequence of X;
assume A3: Element_Of(F,Borel_Sets,G,0) = Omega-->1+r;
let w be Element of Omega;
assume A4: BuyPortfolioExt(phi,jpi,d)<=0;
A5: (1+r)*BuyPortfolioExt(phi,jpi,d) <= 0
proof
1+r>0 by A2,XREAL_1:62;
hence thesis by A4;
end;
((1+r)*BuyPortfolioExt(phi,jpi,d)) + (PortfolioValueFut(d,phi,F,G,w) -
((1+r)*BuyPortfolioExt(phi,jpi,d))) <=
(PortfolioValueFut(d,phi,F,G,w) -
((1+r)*BuyPortfolioExt(phi,jpi,d))) by A5,XREAL_1:32; then
PortfolioValueFut(d,phi,F,G,w) <= (PortfolioValueFut(d,phi,F,G,w) -
(1+r)*(phi.0 + BuyPortfolio(phi,jpi,d))) by A1,Th11; then
PortfolioValueFut(d,phi,F,G,w) <= ((PortfolioValueFut(d,phi,F,G,w) -
(1+r)*BuyPortfolio(phi,jpi,d))) - (1+r)*phi.0; then
PortfolioValueFut(d,phi,F,G,w) + (1+r)*phi.0 <=
((PortfolioValueFut(d,phi,F,G,w) -
(1+r)*BuyPortfolio(phi,jpi,d))) by XREAL_1:19;
hence thesis by A1,A3,Th12;
end;
theorem
for d being Nat st d>0 holds
for r being Real st r>-1 holds
for phi being Real_Sequence,
jpi being pricefunction holds
for G being sequence of set_of_random_variables_on (F,Borel_Sets) st
Element_Of(F,Borel_Sets,G,0) = Omega-->1+r holds
(BuyPortfolioExt(phi,jpi,d)<=0 implies
({w where w is Element of Omega:
PortfolioValueFutExt(d,phi,F,G,w) >= 0} c=
{w where w is Element of Omega:
PortfolioValueFut(d,phi,F,G,w)
>= (1+r)*BuyPortfolio(phi,jpi,d)} &
{w where w is Element of Omega: PortfolioValueFutExt(d,phi,F,G,w) > 0} c=
{w where w is Element of Omega: PortfolioValueFut(d,phi,F,G,w)
> (1+r)*BuyPortfolio(phi,jpi,d)}))
proof
let d be Nat;
assume A1: d>0;
let r be Real;
assume A2:r>-1;
let phi be Real_Sequence,
jpi be pricefunction;
set X = set_of_random_variables_on (F,Borel_Sets);
let G be sequence of X;
assume A3: Element_Of(F,Borel_Sets,G,0) = Omega-->1+r;
assume A4: BuyPortfolioExt(phi,jpi,d)<=0;
A5: {w where w is Element of Omega:
PortfolioValueFutExt(d,phi,F,G,w) >= 0} c=
{w where w is Element of Omega:
PortfolioValueFut(d,phi,F,G,w)
>= (1+r)*BuyPortfolio(phi,jpi,d)}
proof
let x be object;
assume x in {w where w is Element of Omega:
PortfolioValueFutExt(d,phi,F,G,w) >= 0}; then
consider w being Element of Omega such that
A6: x=w & PortfolioValueFutExt(d,phi,F,G,w) >= 0;
0<= PortfolioValueFut(d,phi,F,G,w) -
((1+r)*BuyPortfolio(phi,jpi,d)) by A1,A2,A3,A4,Th13,A6; then
0+ ((1+r)*BuyPortfolio(phi,jpi,d))
<= PortfolioValueFut(d,phi,F,G,w) by XREAL_1:19;
hence thesis by A6;
end;
{w where w is Element of Omega:
PortfolioValueFutExt(d,phi,F,G,w) > 0} c=
{w where w is Element of Omega:
PortfolioValueFut(d,phi,F,G,w) > (1+r)*BuyPortfolio(phi,jpi,d)}
proof
let x be object;
assume x in {w where w is Element of Omega:
PortfolioValueFutExt(d,phi,F,G,w) > 0}; then
consider w being Element of Omega such that
A7: x=w & PortfolioValueFutExt(d,phi,F,G,w) > 0;
PortfolioValueFutExt(d,phi,F,G,w) <= (PortfolioValueFut(d,phi,F,G,w) -
(1+r)*BuyPortfolio(phi,jpi,d)) by A1,A2,A3,A4,Th13; then
0+((1+r)*BuyPortfolio(phi,jpi,d))
< (PortfolioValueFut(d,phi,F,G,w) - (1+r)*BuyPortfolio(phi,jpi,d))
+((1+r)*BuyPortfolio(phi,jpi,d)) by A7,XREAL_1:6;
hence thesis by A7;
end;
hence thesis by A5;
end;
theorem Th15:
for f being Function of Omega,REAL st
f is (Sigma,Borel_Sets)-random_variable-like holds
f is ([#]Sigma)-measurable &
f is Real-Valued-Random-Variable of Sigma
proof
let f be Function of Omega,REAL;
assume A1: f is (Sigma,Borel_Sets)-random_variable-like;
A2: for r being Element of REAL holds Omega /\ less_dom(f,r) in Sigma
proof
let r be Element of REAL;
less_dom(f,r) = {w where w is Element of Omega: f.w <r} by A1,Th9;
then less_dom(f,r) is Element of Sigma by A1,Th9; then
less_dom(f,r) in Sigma;
hence thesis by XBOOLE_1:28;
end;
for r being Real holds [#]Sigma /\ less_dom(f,r) in Sigma
proof
let r be Real;
reconsider r as Element of REAL by XREAL_0:def 1;
[#]Sigma /\ less_dom(f,r) in Sigma by A2;
hence thesis;
end;
hence thesis by MESFUNC6:12;
end;
theorem
set_of_random_variables_on (Sigma,Borel_Sets) c=
Real-Valued-Random-Variables-Set Sigma
proof
let x be object;
assume x in set_of_random_variables_on (Sigma,Borel_Sets); then
consider f being Function of Omega,REAL such that
A1: x=f & f is (Sigma,Borel_Sets)-random_variable-like;
A2: f is (Sigma,Borel_Sets)-random_variable-like implies
f is Real-Valued-Random-Variable of Sigma by Th15;
x in the set of all q where q is Real-Valued-Random-Variable of Sigma
by A2,A1;
hence thesis by RANDOM_2:def 3;
end;
theorem
Omega --> the Element of Omega2 is random_variable of F,F2 by LemmaExample;