let X be non empty set ; for S being SigmaField of X
for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative holds
ex F being Functional_Sequence of X,ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) )
let S be SigmaField of X; for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative holds
ex F being Functional_Sequence of X,ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) )
let f be PartFunc of X,ExtREAL ; ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative implies ex F being Functional_Sequence of X,ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) ) )
assume that
A1:
ex A being Element of S st
( A = dom f & f is_measurable_on A )
and
A2:
f is nonnegative
; ex F being Functional_Sequence of X,ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) )
defpred S1[ Nat, PartFunc of X,ExtREAL ] means ( dom $2 = dom f & ( for x being Element of X st x in dom f holds
( ( for k being Nat st 1 <= k & k <= (2 |^ $1) * $1 & (k - 1) / (2 |^ $1) <= f . x & f . x < k / (2 |^ $1) holds
$2 . x = (k - 1) / (2 |^ $1) ) & ( $1 <= f . x implies $2 . x = $1 ) ) ) );
A3:
for n being Element of NAT ex y being Element of PFuncs X,ExtREAL st S1[n,y]
proof
let n be
Element of
NAT ;
ex y being Element of PFuncs X,ExtREAL st S1[n,y]
defpred S2[
set ,
set ]
means ( ( for
k being
Nat st 1
<= k &
k <= (2 |^ n) * n &
(k - 1) / (2 |^ n) <= f . $1 &
f . $1
< k / (2 |^ n) holds
$2
= (k - 1) / (2 |^ n) ) & (
n <= f . $1 implies $2
= n ) );
A4:
for
x being
set st
x in dom f holds
ex
y being
set st
S2[
x,
y]
proof
let x be
set ;
( x in dom f implies ex y being set st S2[x,y] )
assume
x in dom f
;
ex y being set st S2[x,y]
end;
consider fn being
Function such that A12:
(
dom fn = dom f & ( for
x being
set st
x in dom f holds
S2[
x,
fn . x] ) )
from CLASSES1:sch 1(A4);
then
rng fn c= ExtREAL
by TARSKI:def 3;
then reconsider fn =
fn as
PartFunc of
(dom f),
ExtREAL by A12, RELSET_1:11;
reconsider fn =
fn as
PartFunc of
X,
ExtREAL by A12, RELSET_1:13;
reconsider y =
fn as
Element of
PFuncs X,
ExtREAL by PARTFUN1:119;
take
y
;
S1[n,y]
thus
S1[
n,
y]
by A12;
verum
end;
ex F being Function of NAT ,(PFuncs X,ExtREAL ) st
for n being Element of NAT holds S1[n,F . n]
from FUNCT_2:sch 3(A3);
then consider F being Function of NAT ,(PFuncs X,ExtREAL ) such that
A20:
for n being Element of NAT holds dom (F . n) = dom f
and
A21:
for n being Element of NAT
for x being Element of X st x in dom f holds
( ( for k being Nat st 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= f . x & f . x < k / (2 |^ n) holds
(F . n) . x = (k - 1) / (2 |^ n) ) & ( n <= f . x implies (F . n) . x = n ) )
;
reconsider F = F as Functional_Sequence of X,ExtREAL ;
consider A being Element of S such that
A23:
A = dom f
and
A24:
f is_measurable_on A
by A1;
A25:
for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x
proof
let n,
m be
Nat;
( n <= m implies for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x )
assume A26:
n <= m
;
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x
reconsider n =
n,
m =
m as
Element of
NAT by ORDINAL1:def 13;
let x be
Element of
X;
( x in dom f implies (F . n) . x <= (F . m) . x )
assume A27:
x in dom f
;
(F . n) . x <= (F . m) . x
per cases
( R_EAL m <= f . x or f . x < R_EAL m )
;
suppose A30:
f . x < R_EAL m
;
(F . n) . x <= (F . m) . xA31:
0 <= f . x
by A2, SUPINF_2:70;
then consider M being
Nat such that A32:
1
<= M
and A33:
M <= (2 |^ m) * m
and A34:
(M - 1) / (2 |^ m) <= f . x
and A35:
f . x < M / (2 |^ m)
by A30, Th8;
reconsider M =
M as
Element of
NAT by ORDINAL1:def 13;
A36:
(F . m) . x = (M - 1) / (2 |^ m)
by A21, A27, A32, A33, A34, A35;
per cases
( R_EAL n <= f . x or f . x < R_EAL n )
;
suppose A40:
f . x < R_EAL n
;
(F . n) . x <= (F . m) . xconsider k being
Nat such that A41:
m = n + k
by A26, NAT_1:10;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 13;
reconsider K = 2
|^ k as
Element of
NAT ;
consider N1 being
Nat such that A42:
1
<= N1
and A43:
N1 <= (2 |^ n) * n
and A44:
(N1 - 1) / (2 |^ n) <= f . x
and A45:
f . x < N1 / (2 |^ n)
by A31, A40, Th8;
reconsider N1 =
N1 as
Element of
NAT by ORDINAL1:def 13;
A46:
(F . n) . x = (N1 - 1) / (2 |^ n)
by A21, A27, A42, A43, A44, A45;
R_EAL ((N1 - 1) / (2 |^ n)) < R_EAL (M / (2 |^ (n + k)))
by A35, A44, A41, XXREAL_0:2;
then
(N1 - 1) / (2 |^ n) < M / ((2 |^ n) * (2 |^ k))
by NEWTON:13;
then
(N1 - 1) / (2 |^ n) < (M / (2 |^ k)) / (2 |^ n)
by XCMPLX_1:79;
then
N1 - 1
< M / (2 |^ k)
by XREAL_1:74;
then
K * (N1 - 1) < M
by PREPOWER:13, XREAL_1:81;
then
(K * (N1 - 1)) + 1
<= M
by INT_1:20;
then
K * (N1 - 1) <= M - 1
by XREAL_1:21;
then
(K * (N1 - 1)) / (2 |^ (n + k)) <= (M - 1) / (2 |^ (n + k))
by XREAL_1:74;
then A47:
(K * (N1 - 1)) / ((2 |^ n) * (2 |^ k)) <= (M - 1) / (2 |^ (n + k))
by NEWTON:13;
2
|^ k > 0
by PREPOWER:13;
hence
(F . n) . x <= (F . m) . x
by A36, A46, A41, A47, XCMPLX_1:92;
verum end; end;
end;
A48:
for n being Nat holds F . n is_simple_func_in S
proof
let n be
Nat;
F . n is_simple_func_in S
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
reconsider N = 2
|^ n as
Element of
NAT ;
defpred S2[
Nat,
set ]
means ( ( $1
<= N * n implies $2
= (A /\ (great_eq_dom f,(R_EAL (($1 - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL ($1 / (2 |^ n)))) ) & ( $1
= (N * n) + 1 implies $2
= A /\ (great_eq_dom f,(R_EAL n)) ) );
now let x be
Element of
X;
( x in dom (F . n) implies |.((F . n) . b1).| < +infty )assume
x in dom (F . n)
;
|.((F . n) . b1).| < +infty then A49:
x in dom f
by A22;
per cases
( R_EAL n <= f . x or f . x < R_EAL n )
;
suppose A52:
f . x < R_EAL n
;
|.((F . n) . b1).| < +infty A53:
0 <= f . x
by A2, SUPINF_2:70;
R_EAL n < +infty
by XXREAL_0:9;
then reconsider y =
f . x as
Real by A52, A53, XXREAL_0:14;
set k =
[\((2 |^ n) * y)/] + 1;
A54:
[\((2 |^ n) * y)/] <= (2 |^ n) * y
by INT_1:def 4;
((2 |^ n) * y) - 1
< [\((2 |^ n) * y)/]
by INT_1:def 4;
then A55:
(2 |^ n) * y < [\((2 |^ n) * y)/] + 1
by XREAL_1:21;
A56:
0 < 2
|^ n
by PREPOWER:13;
then
(2 |^ n) * y < (2 |^ n) * n
by A52, XREAL_1:70;
then
[\((2 |^ n) * y)/] < (2 |^ n) * n
by A54, XXREAL_0:2;
then A57:
[\((2 |^ n) * y)/] + 1
<= (2 |^ n) * n
by INT_1:20;
A58:
0 <= (2 |^ n) * y
by A53;
then A59:
0 + 1
<= [\((2 |^ n) * y)/] + 1
by A55, INT_1:20;
reconsider k =
[\((2 |^ n) * y)/] + 1 as
Element of
NAT by A58, A55, INT_1:16;
k - 1
<= (2 |^ n) * y
by INT_1:def 4;
then A60:
(k - 1) / (2 |^ n) <= y
by PREPOWER:13, XREAL_1:81;
y < k / (2 |^ n)
by A56, INT_1:52, XREAL_1:83;
then A61:
(F . n) . x = (k - 1) / (2 |^ n)
by A21, A49, A59, A57, A60;
then
-infty < (F . n) . x
by XXREAL_0:12;
then A62:
- +infty < (F . n) . x
by XXREAL_3:def 3;
(F . n) . x < +infty
by A61, XXREAL_0:9;
hence
|.((F . n) . x).| < +infty
by A62, EXTREAL2:59;
verum end; end;
then A63:
F . n is
V55()
by MESFUNC2:def 1;
consider G being
FinSequence of
S such that A67:
(
dom G = Seg ((N * n) + 1) & ( for
k being
Nat st
k in Seg ((N * n) + 1) holds
S2[
k,
G . k] ) )
from FINSEQ_1:sch 5(A64);
A72:
len G = ((2 |^ n) * n) + 1
by A67, FINSEQ_1:def 3;
then reconsider G =
G as
Finite_Sep_Sequence of
S by PROB_2:def 3;
A105:
for
k being
Nat for
x,
y being
Element of
X st
k in dom G &
x in G . k &
y in G . k holds
(F . n) . x = (F . n) . y
proof
let k be
Nat;
for x, y being Element of X st k in dom G & x in G . k & y in G . k holds
(F . n) . x = (F . n) . ylet x,
y be
Element of
X;
( k in dom G & x in G . k & y in G . k implies (F . n) . x = (F . n) . y )
assume that A106:
k in dom G
and A107:
x in G . k
and A108:
y in G . k
;
(F . n) . x = (F . n) . y
A109:
1
<= k
by A67, A106, FINSEQ_1:3;
A110:
k <= (N * n) + 1
by A67, A106, FINSEQ_1:3;
now per cases
( k = (N * n) + 1 or k <> (N * n) + 1 )
;
suppose
k = (N * n) + 1
;
(F . n) . x = (F . n) . ythen A111:
G . k = A /\ (great_eq_dom f,(R_EAL n))
by A67, A106;
then
x in great_eq_dom f,
(R_EAL n)
by A107, XBOOLE_0:def 4;
then A112:
R_EAL n <= f . x
by MESFUNC1:def 15;
y in great_eq_dom f,
(R_EAL n)
by A108, A111, XBOOLE_0:def 4;
then A113:
R_EAL n <= f . y
by MESFUNC1:def 15;
x in A
by A107, A111, XBOOLE_0:def 4;
then A114:
(F . n) . x = R_EAL n
by A23, A21, A112;
y in A
by A108, A111, XBOOLE_0:def 4;
hence
(F . n) . x = (F . n) . y
by A23, A21, A114, A113;
verum end; suppose
k <> (N * n) + 1
;
(F . n) . x = (F . n) . ythen
k < (N * n) + 1
by A110, XXREAL_0:1;
then A115:
k <= N * n
by NAT_1:13;
then A116:
G . k = (A /\ (great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (k / (2 |^ n))))
by A67, A106;
then
x in less_dom f,
(R_EAL (k / (2 |^ n)))
by A107, XBOOLE_0:def 4;
then A117:
f . x < R_EAL (k / (2 |^ n))
by MESFUNC1:def 12;
A118:
x in A /\ (great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n))))
by A107, A116, XBOOLE_0:def 4;
then
x in great_eq_dom f,
(R_EAL ((k - 1) / (2 |^ n)))
by XBOOLE_0:def 4;
then A119:
R_EAL ((k - 1) / (2 |^ n)) <= f . x
by MESFUNC1:def 15;
x in A
by A118, XBOOLE_0:def 4;
then A120:
(F . n) . x = R_EAL ((k - 1) / (2 |^ n))
by A23, A21, A109, A115, A117, A119;
y in less_dom f,
(R_EAL (k / (2 |^ n)))
by A108, A116, XBOOLE_0:def 4;
then A121:
f . y < R_EAL (k / (2 |^ n))
by MESFUNC1:def 12;
A122:
y in A /\ (great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n))))
by A108, A116, XBOOLE_0:def 4;
then
y in great_eq_dom f,
(R_EAL ((k - 1) / (2 |^ n)))
by XBOOLE_0:def 4;
then A123:
R_EAL ((k - 1) / (2 |^ n)) <= f . y
by MESFUNC1:def 15;
y in A
by A122, XBOOLE_0:def 4;
hence
(F . n) . x = (F . n) . y
by A23, A21, A109, A115, A121, A123, A120;
verum end;
hence
(F . n) . x = (F . n) . y
;
verum
end;
for
v being
set st
v in dom f holds
v in union (rng G)
proof
let v be
set ;
( v in dom f implies v in union (rng G) )
assume A124:
v in dom f
;
v in union (rng G)
ex
B being
set st
(
v in B &
B in rng G )
proof
per cases
( f . v < R_EAL n or R_EAL n <= f . v )
;
suppose A125:
f . v < R_EAL n
;
ex B being set st
( v in B & B in rng G )
0 <= f . v
by A2, SUPINF_2:70;
then consider k being
Nat such that A126:
1
<= k
and A127:
k <= (2 |^ n) * n
and A128:
(k - 1) / (2 |^ n) <= f . v
and A129:
f . v < k / (2 |^ n)
by A125, Th8;
v in great_eq_dom f,
(R_EAL ((k - 1) / (2 |^ n)))
by A124, A128, MESFUNC1:def 15;
then A130:
v in A /\ (great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n))))
by A23, A124, XBOOLE_0:def 4;
v in less_dom f,
(R_EAL (k / (2 |^ n)))
by A124, A129, MESFUNC1:def 12;
then A131:
v in (A /\ (great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (k / (2 |^ n))))
by A130, XBOOLE_0:def 4;
take B =
G . k;
( v in B & B in rng G )A132:
k in NAT
by ORDINAL1:def 13;
N * n <= (N * n) + 1
by NAT_1:11;
then
k <= (N * n) + 1
by A127, XXREAL_0:2;
then
k in Seg ((N * n) + 1)
by A126, A132;
hence
(
v in B &
B in rng G )
by A67, A127, A131, FUNCT_1:12;
verum end;
end;
hence
v in union (rng G)
by TARSKI:def 4;
verum
end;
then A135:
dom f c= union (rng G)
by TARSKI:def 3;
for
v being
set st
v in union (rng G) holds
v in dom f
then
union (rng G) c= dom f
by TARSKI:def 3;
then
union (rng G) = dom f
by A135, XBOOLE_0:def 10;
then
dom (F . n) = union (rng G)
by A22;
hence
F . n is_simple_func_in S
by A63, A105, MESFUNC2:def 5;
verum
end;
A141:
now let x be
Element of
X;
( x in dom f implies ( F # b1 is convergent & lim (F # b1) = f . b1 ) )assume A142:
x in dom f
;
( F # b1 is convergent & lim (F # b1) = f . b1 )per cases
( |.(f . x).| = +infty or |.(f . x).| <> +infty )
;
suppose
|.(f . x).| <> +infty
;
( F # b1 is convergent & lim (F # b1) = f . b1 )then reconsider g =
f . x as
Real by EXTREAL2:67, XXREAL_0:14;
A148:
for
p being
real number st
0 < p holds
ex
k being
Nat st
for
j being
Nat st
j >= k holds
|.(((F # x) . j) - (f . x)).| < p
proof
set N2 =
[/g\] + 1;
let p be
real number ;
( 0 < p implies ex k being Nat st
for j being Nat st j >= k holds
|.(((F # x) . j) - (f . x)).| < p )
A149:
g <= [/g\]
by INT_1:def 5;
[/g\] < [/g\] + 1
by XREAL_1:31;
then A150:
g < [/g\] + 1
by A149, XXREAL_0:2;
0 <= g
by A2, SUPINF_2:70;
then reconsider N2 =
[/g\] + 1 as
Element of
NAT by A149, INT_1:16;
A151:
for
N being
Nat st
N >= N2 holds
|.(((F # x) . N) - (f . x)).| < 1
/ (2 |^ N)
proof
let N be
Nat;
( N >= N2 implies |.(((F # x) . N) - (f . x)).| < 1 / (2 |^ N) )
assume A152:
N >= N2
;
|.(((F # x) . N) - (f . x)).| < 1 / (2 |^ N)
reconsider N =
N as
Element of
NAT by ORDINAL1:def 13;
A153:
0 <= f . x
by A2, SUPINF_2:70;
f . x < N
by A150, A152, XXREAL_0:2;
then consider m being
Nat such that A154:
1
<= m
and A155:
m <= (2 |^ N) * N
and A156:
(m - 1) / (2 |^ N) <= f . x
and A157:
f . x < m / (2 |^ N)
by A153, Th8;
reconsider m =
m as
Element of
NAT by ORDINAL1:def 13;
A158:
(F # x) . N =
(F . N) . x
by Def13
.=
(m - 1) / (2 |^ N)
by A21, A142, A154, A155, A156, A157
;
(R_EAL (m / (2 |^ N))) - (R_EAL ((m - 1) / (2 |^ N))) =
(m / (2 |^ N)) - ((m - 1) / (2 |^ N))
by SUPINF_2:5
.=
(m / (2 |^ N)) + (- ((m - 1) / (2 |^ N)))
.=
(m / (2 |^ N)) + ((- (m - 1)) / (2 |^ N))
by XCMPLX_1:188
.=
(m + (- (m - 1))) / (2 |^ N)
by XCMPLX_1:63
;
then A159:
(f . x) - ((F # x) . N) < 1
/ (2 |^ N)
by A157, A158, XXREAL_3:47;
- (((F # x) . N) - (f . x)) = (f . x) - ((F # x) . N)
by XXREAL_3:27;
then A160:
|.(((F # x) . N) - (f . x)).| = |.((f . x) - ((F # x) . N)).|
by EXTREAL2:66;
2
|^ N > 0
by PREPOWER:13;
then A161:
- (R_EAL (1 / (2 |^ N))) < 0
;
0 <= (f . x) - ((F # x) . N)
by A156, A158, XXREAL_3:43;
hence
|.(((F # x) . N) - (f . x)).| < 1
/ (2 |^ N)
by A160, A159, A161, EXTREAL2:59;
verum
end;
assume
0 < p
;
ex k being Nat st
for j being Nat st j >= k holds
|.(((F # x) . j) - (f . x)).| < p
then consider N1 being
Element of
NAT such that A162:
1
/ (2 |^ N1) <= p
by PREPOWER:106;
reconsider k =
max N2,
N1 as
Element of
NAT ;
A163:
for
k being
Nat st
k >= N1 holds
1
/ (2 |^ k) <= p
hence
ex
k being
Nat st
for
j being
Nat st
j >= k holds
|.(((F # x) . j) - (f . x)).| < p
;
verum
end; A168:
f . x = R_EAL g
;
then A169:
F # x is
convergent_to_finite_number
by A148, Def8;
then
F # x is
convergent
by Def11;
hence
(
F # x is
convergent &
lim (F # x) = f . x )
by A168, A148, A169, Def12;
verum end; end;
for n being Nat holds F . n is nonnegative
hence
ex F being Functional_Sequence of X,ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) )
by A22, A48, A25, A141; verum