consider f being Function of Omega,REAL such that
B10:
f = simple_RV_help (ChiFuncs,ConstFuncs,n)
;
f is random_variable of F, Borel_Sets
proof
defpred S1[
Nat]
means simple_RV_help (
ChiFuncs,
ConstFuncs,$1) is
random_variable of
F,
Borel_Sets ;
set RVs0 =
simple_RV_help (
ChiFuncs,
ConstFuncs,
0);
J0:
S1[
0 ]
proof
for
w being
Element of
Omega holds
(simple_RV_help (ChiFuncs,ConstFuncs,0)) . w = ((Conv_RV (ConstFuncs,0)) (#) (Conv_RV (ChiFuncs,0))) . w
proof
let w be
Element of
Omega;
(simple_RV_help (ChiFuncs,ConstFuncs,0)) . w = ((Conv_RV (ConstFuncs,0)) (#) (Conv_RV (ChiFuncs,0))) . w
(simple_RV_help (ChiFuncs,ConstFuncs,0)) . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . 0
by Def777;
then
(simple_RV_help (ChiFuncs,ConstFuncs,0)) . w = ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w))) . 0
by SERIES_1:def 1;
then C2:
(simple_RV_help (ChiFuncs,ConstFuncs,0)) . w = ((Conv2_RV (ConstFuncs,w)) . 0) * ((Conv2_RV (ChiFuncs,w)) . 0)
by VALUED_1:5;
C3:
(Conv2_RV (ConstFuncs,w)) . 0 = (Conv_RV (ConstFuncs,0)) . w
by Def770;
(Conv2_RV (ChiFuncs,w)) . 0 = (Conv_RV (ChiFuncs,0)) . w
by Def770;
hence
(simple_RV_help (ChiFuncs,ConstFuncs,0)) . w = ((Conv_RV (ConstFuncs,0)) (#) (Conv_RV (ChiFuncs,0))) . w
by VALUED_1:5, C2, C3;
verum
end;
then
simple_RV_help (
ChiFuncs,
ConstFuncs,
0)
= (Conv_RV (ConstFuncs,0)) (#) (Conv_RV (ChiFuncs,0))
;
hence
S1[
0 ]
by FINANCE2:25;
verum
end;
J1:
for
n being
Nat st
S1[
n] holds
S1[
n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume ASS0:
S1[
n]
;
S1[n + 1]
set RVsn =
simple_RV_help (
ChiFuncs,
ConstFuncs,
n);
set RVsn1 =
simple_RV_help (
ChiFuncs,
ConstFuncs,
(n + 1));
set RVa =
(Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1)));
for
w being
Element of
Omega holds
(simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = ((simple_RV_help (ChiFuncs,ConstFuncs,n)) + ((Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1))))) . w
proof
let w be
Element of
Omega;
(simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = ((simple_RV_help (ChiFuncs,ConstFuncs,n)) + ((Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1))))) . w
(simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . (n + 1)
by Def777;
then
(simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = (In (((Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n),REAL)) + (((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w))) . (n + 1))
by SERIES_1:def 1;
then
(simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = ((simple_RV_help (ChiFuncs,ConstFuncs,n)) . w) + (((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w))) . (n + 1))
by Def777;
then D1:
(simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = ((simple_RV_help (ChiFuncs,ConstFuncs,n)) . w) + (((Conv2_RV (ConstFuncs,w)) . (n + 1)) * ((Conv2_RV (ChiFuncs,w)) . (n + 1)))
by VALUED_1:5;
D2:
(Conv2_RV (ConstFuncs,w)) . (n + 1) = (Conv_RV (ConstFuncs,(n + 1))) . w
by Def770;
(Conv2_RV (ChiFuncs,w)) . (n + 1) = (Conv_RV (ChiFuncs,(n + 1))) . w
by Def770;
then
(simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = ((simple_RV_help (ChiFuncs,ConstFuncs,n)) . w) + (((Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1)))) . w)
by VALUED_1:5, D1, D2;
hence
(simple_RV_help (ChiFuncs,ConstFuncs,(n + 1))) . w = ((simple_RV_help (ChiFuncs,ConstFuncs,n)) + ((Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1))))) . w
by VALUED_1:1;
verum
end;
then M1:
simple_RV_help (
ChiFuncs,
ConstFuncs,
(n + 1))
= (simple_RV_help (ChiFuncs,ConstFuncs,n)) + ((Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1))))
;
(
simple_RV_help (
ChiFuncs,
ConstFuncs,
n) is
random_variable of
F,
Borel_Sets &
(Conv_RV (ConstFuncs,(n + 1))) (#) (Conv_RV (ChiFuncs,(n + 1))) is
random_variable of
F,
Borel_Sets )
by ASS0, FINANCE2:25;
hence
S1[
n + 1]
by M1, FINANCE2:23;
verum
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(J0, J1);
hence
f is
random_variable of
F,
Borel_Sets
by B10;
verum
end;
hence
simple_RV_help (ChiFuncs,ConstFuncs,n) is random_variable of F, Borel_Sets
by B10; verum