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 A -measurable ) & 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 A -measurable ) & 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 A -measurable ) & 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 A -measurable )
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[ Element of 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]
reconsider nn =
n as
Nat ;
defpred S2[
object ,
object ]
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
object st
x in dom f holds
ex
y being
object st
S2[
x,
y]
consider fn being
Function such that A14:
(
dom fn = dom f & ( for
x being
object st
x in dom f holds
S2[
x,
fn . x] ) )
from CLASSES1:sch 1(A4);
then
rng fn c= ExtREAL
;
then reconsider fn =
fn as
PartFunc of
(dom f),
ExtREAL by A14, RELSET_1:4;
reconsider fn =
fn as
PartFunc of
X,
ExtREAL by A14, RELSET_1:5;
reconsider y =
fn as
Element of
PFuncs (
X,
ExtREAL)
by PARTFUN1:45;
take
y
;
S1[n,y]
thus
S1[
n,
y]
by A14;
verum
end;
consider F being sequence of (PFuncs (X,ExtREAL)) such that
A22:
for n being Element of NAT holds S1[n,F . n]
from FUNCT_2:sch 3(A3);
A23:
for n being Element of NAT holds dom (F . n) = dom f
by A22;
A24:
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 ) )
by A22;
reconsider F = F as Functional_Sequence of X,ExtREAL ;
consider A being Element of S such that
A26:
A = dom f
and
A27:
f is A -measurable
by A1;
A28:
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 A29:
n <= m
;
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x
reconsider nn =
n,
mm =
m as
Element of
NAT by ORDINAL1:def 12;
let x be
Element of
X;
( x in dom f implies (F . n) . x <= (F . m) . x )
assume A30:
x in dom f
;
(F . n) . x <= (F . m) . x
per cases
( m <= f . x or f . x < m )
;
suppose A33:
f . x < m
;
(F . n) . x <= (F . m) . xA34:
0 <= f . x
by A2, SUPINF_2:51;
then consider M being
Nat such that A35:
1
<= M
and A36:
M <= (2 |^ m) * m
and A37:
(M - 1) / (2 |^ m) <= f . x
and A38:
f . x < M / (2 |^ m)
by A33, Th4;
reconsider M =
M as
Element of
NAT by ORDINAL1:def 12;
A39:
(F . mm) . x = (M - 1) / (2 |^ m)
by A24, A30, A35, A36, A37, A38;
per cases
( n <= f . x or f . x < n )
;
suppose A43:
f . x < n
;
(F . n) . x <= (F . m) . xconsider k being
Nat such that A44:
m = nn + k
by A29, NAT_1:10;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
reconsider K = 2
|^ k as
Element of
NAT ;
consider N1 being
Nat such that A45:
1
<= N1
and A46:
N1 <= (2 |^ n) * n
and A47:
(N1 - 1) / (2 |^ n) <= f . x
and A48:
f . x < N1 / (2 |^ n)
by A34, A43, Th4;
reconsider N1 =
N1 as
Element of
NAT by ORDINAL1:def 12;
A49:
(F . nn) . x = (N1 - 1) / (2 |^ nn)
by A24, A30, A45, A46, A47, A48;
(N1 - 1) / (2 |^ n) < M / (2 |^ (n + k))
by A38, A47, A44, XXREAL_0:2;
then
(N1 - 1) / (2 |^ n) < M / ((2 |^ n) * (2 |^ k))
by NEWTON:8;
then
(N1 - 1) / (2 |^ n) < (M / (2 |^ k)) / (2 |^ n)
by XCMPLX_1:78;
then
N1 - 1
< M / (2 |^ k)
by XREAL_1:72;
then
K * (N1 - 1) < M
by PREPOWER:6, XREAL_1:79;
then
(K * (N1 - 1)) + 1
<= M
by INT_1:7;
then
K * (N1 - 1) <= M - 1
by XREAL_1:19;
then
(K * (N1 - 1)) / (2 |^ (n + k)) <= (M - 1) / (2 |^ (n + k))
by XREAL_1:72;
then A50:
(K * (N1 - 1)) / ((2 |^ n) * (2 |^ k)) <= (M - 1) / (2 |^ (n + k))
by NEWTON:8;
2
|^ k > 0
by PREPOWER:6;
hence
(F . n) . x <= (F . m) . x
by A39, A49, A44, A50, XCMPLX_1:91;
verum end; end;
end;
A51:
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 nn =
n as
Element of
NAT by ORDINAL1:def 12;
reconsider N = 2
|^ nn as
Element of
NAT ;
defpred S2[
Nat,
set ]
means ( ( $1
<= N * n implies $2
= (A /\ (great_eq_dom (f,(($1 - 1) / (2 |^ n))))) /\ (less_dom (f,($1 / (2 |^ n)))) ) & ( $1
= (N * n) + 1 implies $2
= A /\ (great_eq_dom (f,n)) ) );
now for x being Element of X st x in dom (F . n) holds
|.((F . n) . x).| < +infty 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 A52:
x in dom f
by A25;
per cases
( n <= f . x or f . x < n )
;
suppose A55:
f . x < n
;
|.((F . n) . b1).| < +infty A56:
0 <= f . x
by A2, SUPINF_2:51;
nn in REAL
by XREAL_0:def 1;
then
nn < +infty
by XXREAL_0:9;
then reconsider y =
f . x as
Element of
REAL by A55, A56, XXREAL_0:14;
set k =
[\((2 |^ n) * y)/] + 1;
A57:
[\((2 |^ n) * y)/] <= (2 |^ n) * y
by INT_1:def 6;
((2 |^ n) * y) - 1
< [\((2 |^ n) * y)/]
by INT_1:def 6;
then A58:
(2 |^ n) * y < [\((2 |^ n) * y)/] + 1
by XREAL_1:19;
A59:
0 < 2
|^ n
by PREPOWER:6;
then
(2 |^ n) * y < (2 |^ n) * n
by A55, XREAL_1:68;
then
[\((2 |^ n) * y)/] < (2 |^ n) * n
by A57, XXREAL_0:2;
then A60:
[\((2 |^ n) * y)/] + 1
<= (2 |^ n) * n
by INT_1:7;
A61:
0 <= (2 |^ n) * y
by A56;
then A62:
0 + 1
<= [\((2 |^ n) * y)/] + 1
by A58, INT_1:7;
reconsider k =
[\((2 |^ n) * y)/] + 1 as
Element of
NAT by A61, A58, INT_1:3;
reconsider k =
k as
Nat ;
k - 1
<= (2 |^ n) * y
by INT_1:def 6;
then A63:
(k - 1) / (2 |^ nn) <= y
by PREPOWER:6, XREAL_1:79;
A64:
(k - 1) / (2 |^ nn) in REAL
by XREAL_0:def 1;
y < k / (2 |^ nn)
by A59, INT_1:29, XREAL_1:81;
then A65:
(F . nn) . x = (k - 1) / (2 |^ nn)
by A24, A52, A62, A60, A63;
then
-infty < (F . n) . x
by XXREAL_0:12, A64;
then A66:
- +infty < (F . n) . x
by XXREAL_3:def 3;
(F . n) . x < +infty
by A65, XXREAL_0:9, A64;
hence
|.((F . n) . x).| < +infty
by A66, EXTREAL1:22;
verum end; end;
then A67:
F . n is
real-valued
by MESFUNC2:def 1;
consider G being
FinSequence of
S such that A71:
(
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(A68);
A75:
len G = ((2 |^ n) * n) + 1
by A71, FINSEQ_1:def 3;
then reconsider G =
G as
Finite_Sep_Sequence of
S by PROB_2:def 2;
A108:
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 A109:
k in dom G
and A110:
x in G . k
and A111:
y in G . k
;
(F . n) . x = (F . n) . y
A112:
1
<= k
by A71, A109, FINSEQ_1:1;
A113:
k <= (N * n) + 1
by A71, A109, FINSEQ_1:1;
now (F . n) . x = (F . n) . yper cases
( k = (N * n) + 1 or k <> (N * n) + 1 )
;
suppose
k = (N * n) + 1
;
(F . n) . x = (F . n) . ythen A114:
G . k = A /\ (great_eq_dom (f,n))
by A71, A109;
then
x in great_eq_dom (
f,
n)
by A110, XBOOLE_0:def 4;
then A115:
n <= f . x
by MESFUNC1:def 14;
y in great_eq_dom (
f,
n)
by A111, A114, XBOOLE_0:def 4;
then A116:
n <= f . y
by MESFUNC1:def 14;
x in A
by A110, A114, XBOOLE_0:def 4;
then A117:
(F . nn) . x = nn
by A26, A24, A115;
y in A
by A111, A114, XBOOLE_0:def 4;
hence
(F . n) . x = (F . n) . y
by A26, A24, A117, A116;
verum end; suppose
k <> (N * n) + 1
;
(F . n) . x = (F . n) . ythen
k < (N * n) + 1
by A113, XXREAL_0:1;
then A118:
k <= N * n
by NAT_1:13;
then A119:
G . k = (A /\ (great_eq_dom (f,((k - 1) / (2 |^ n))))) /\ (less_dom (f,(k / (2 |^ n))))
by A71, A109;
then
x in less_dom (
f,
(k / (2 |^ n)))
by A110, XBOOLE_0:def 4;
then A120:
f . x < k / (2 |^ n)
by MESFUNC1:def 11;
A121:
x in A /\ (great_eq_dom (f,((k - 1) / (2 |^ n))))
by A110, A119, XBOOLE_0:def 4;
then
x in great_eq_dom (
f,
((k - 1) / (2 |^ n)))
by XBOOLE_0:def 4;
then A122:
(k - 1) / (2 |^ n) <= f . x
by MESFUNC1:def 14;
x in A
by A121, XBOOLE_0:def 4;
then A123:
(F . n) . x = (k - 1) / (2 |^ n)
by A26, A24, A112, A118, A120, A122;
y in less_dom (
f,
(k / (2 |^ n)))
by A111, A119, XBOOLE_0:def 4;
then A124:
f . y < k / (2 |^ n)
by MESFUNC1:def 11;
A125:
y in A /\ (great_eq_dom (f,((k - 1) / (2 |^ n))))
by A111, A119, XBOOLE_0:def 4;
then
y in great_eq_dom (
f,
((k - 1) / (2 |^ n)))
by XBOOLE_0:def 4;
then A126:
(k - 1) / (2 |^ n) <= f . y
by MESFUNC1:def 14;
y in A
by A125, XBOOLE_0:def 4;
hence
(F . n) . x = (F . n) . y
by A26, A24, A112, A118, A124, A126, A123;
verum end;
hence
(F . n) . x = (F . n) . y
;
verum
end;
for
v being
object st
v in dom f holds
v in union (rng G)
proof
let v be
object ;
( v in dom f implies v in union (rng G) )
reconsider vv =
v as
set by TARSKI:1;
assume A127:
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 < n or n <= f . v )
;
suppose A128:
f . v < n
;
ex B being set st
( v in B & B in rng G )
0 <= f . v
by A2, SUPINF_2:51;
then consider k being
Nat such that A129:
1
<= k
and A130:
k <= (2 |^ n) * n
and A131:
(k - 1) / (2 |^ n) <= f . vv
and A132:
f . vv < k / (2 |^ n)
by A128, Th4;
v in great_eq_dom (
f,
((k - 1) / (2 |^ n)))
by A127, A131, MESFUNC1:def 14;
then A133:
v in A /\ (great_eq_dom (f,((k - 1) / (2 |^ n))))
by A26, A127, XBOOLE_0:def 4;
v in less_dom (
f,
(k / (2 |^ n)))
by A127, A132, MESFUNC1:def 11;
then A134:
v in (A /\ (great_eq_dom (f,((k - 1) / (2 |^ n))))) /\ (less_dom (f,(k / (2 |^ n))))
by A133, XBOOLE_0:def 4;
take
G . k
;
( v in G . k & G . k in rng G )
N * n <= (N * n) + 1
by NAT_1:11;
then
k <= (N * n) + 1
by A130, XXREAL_0:2;
then
k in Seg ((N * n) + 1)
by A129;
hence
(
v in G . k &
G . k in rng G )
by A71, A130, A134, FUNCT_1:3;
verum end;
end;
hence
v in union (rng G)
by TARSKI:def 4;
verum
end;
then A137:
dom f c= union (rng G)
;
for
v being
object st
v in union (rng G) holds
v in dom f
then
union (rng G) c= dom f
;
then
union (rng G) = dom f
by A137;
then
dom (F . n) = union (rng G)
by A25;
hence
F . n is_simple_func_in S
by A67, A108, MESFUNC2:def 4;
verum
end;
A143:
now for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x )let x be
Element of
X;
( x in dom f implies ( F # b1 is convergent & lim (F # b1) = f . b1 ) )assume A144:
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
Element of
REAL by EXTREAL1:30, XXREAL_0:14;
A150:
for
p being
Real 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;
( 0 < p implies ex k being Nat st
for j being Nat st j >= k holds
|.(((F # x) . j) - (f . x)).| < p )
A151:
g <= [/g\]
by INT_1:def 7;
[/g\] < [/g\] + 1
by XREAL_1:29;
then A152:
g < [/g\] + 1
by A151, XXREAL_0:2;
0 <= g
by A2, SUPINF_2:51;
then reconsider N2 =
[/g\] + 1 as
Element of
NAT by A151, INT_1:3;
A153:
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 A154:
N >= N2
;
|.(((F # x) . N) - (f . x)).| < 1 / (2 |^ N)
reconsider NN =
N as
Element of
NAT by ORDINAL1:def 12;
A155:
0 <= f . x
by A2, SUPINF_2:51;
f . x < N
by A152, A154, XXREAL_0:2;
then consider m being
Nat such that A156:
1
<= m
and A157:
m <= (2 |^ N) * N
and A158:
(m - 1) / (2 |^ N) <= f . x
and A159:
f . x < m / (2 |^ N)
by A155, Th4;
reconsider m =
m as
Element of
NAT by ORDINAL1:def 12;
A160:
(F # x) . N =
(F . NN) . x
by Def13
.=
(m - 1) / (2 |^ NN)
by A24, A144, A156, A157, A158, A159
;
then A161:
(F # x) . N in REAL
by XREAL_0:def 1;
(m / (2 |^ N)) - ((m - 1) / (2 |^ N)) =
(m / (2 |^ N)) - ((m - 1) / (2 |^ N))
.=
(m / (2 |^ N)) + (- ((m - 1) / (2 |^ N)))
.=
(m / (2 |^ N)) + ((- (m - 1)) / (2 |^ N))
.=
(m + (- (m - 1))) / (2 |^ N)
;
then A162:
(f . x) - ((F # x) . N) < 1
/ (2 |^ N)
by A159, A160, XXREAL_3:43, A161;
- (((F # x) . N) - (f . x)) = (f . x) - ((F # x) . N)
by XXREAL_3:26;
then A163:
|.(((F # x) . N) - (f . x)).| = |.((f . x) - ((F # x) . N)).|
by EXTREAL1:29;
2
|^ N > 0
by PREPOWER:6;
then A164:
- (1 / (2 |^ N)) < 0
;
0 <= (f . x) - ((F # x) . N)
by A158, A160, XXREAL_3:40;
hence
|.(((F # x) . N) - (f . x)).| < 1
/ (2 |^ N)
by A163, A162, A164, EXTREAL1:22;
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
Nat such that A165:
1
/ (2 |^ N1) <= p
by PREPOWER:92;
reconsider k =
max (
N2,
N1) as
Element of
NAT by ORDINAL1:def 12;
A166:
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; A171:
f . x = g
;
then A172:
F # x is
convergent_to_finite_number
by A150;
then
F # x is
convergent
;
hence
(
F # x is
convergent &
lim (F # x) = f . x )
by A171, A150, A172, 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 A25, A51, A28, A143; verum