let X be non empty set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: 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 ) ) )
consider A being Element of S such that
A3: ( A = dom f & f is_measurable_on A ) by A1;
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 ) ) ) );
A4: 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 ; :: thesis: 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 ) );
A5: for x being set st x in dom f holds
ex y being set st S2[x,y]
proof
let x be set ; :: thesis: ( x in dom f implies ex y being set st S2[x,y] )
assume x in dom f ; :: thesis: ex y being set st S2[x,y]
per cases ( f . x < n or n <= f . x ) ;
suppose A6: f . x < n ; :: thesis: ex y being set st S2[x,y]
0 <= f . x by A2, SUPINF_2:70;
then consider k being Nat such that
A7: ( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= f . x & f . x < k / (2 |^ n) ) by A6, Th8;
take y = (k - 1) / (2 |^ n); :: thesis: S2[x,y]
now
let k1 be Nat; :: thesis: ( 1 <= k1 & k1 <= (2 |^ n) * n & (k1 - 1) / (2 |^ n) <= f . x & f . x < k1 / (2 |^ n) implies y = (k1 - 1) / (2 |^ n) )
assume A8: ( 1 <= k1 & k1 <= (2 |^ n) * n & (k1 - 1) / (2 |^ n) <= f . x & f . x < k1 / (2 |^ n) ) ; :: thesis: y = (k1 - 1) / (2 |^ n)
A9: now
assume k < k1 ; :: thesis: contradiction
then k + 1 <= k1 by NAT_1:13;
then k <= k1 - 1 by XREAL_1:21;
then k / (2 |^ n) <= (k1 - 1) / (2 |^ n) by XREAL_1:74;
hence contradiction by A7, A8, XXREAL_0:2; :: thesis: verum
end;
now
assume k1 < k ; :: thesis: contradiction
then k1 + 1 <= k by NAT_1:13;
then k1 <= k - 1 by XREAL_1:21;
then k1 / (2 |^ n) <= (k - 1) / (2 |^ n) by XREAL_1:74;
hence contradiction by A7, A8, XXREAL_0:2; :: thesis: verum
end;
hence y = (k1 - 1) / (2 |^ n) by A9, XXREAL_0:1; :: thesis: verum
end;
hence S2[x,y] by A6; :: thesis: verum
end;
suppose A10: n <= f . x ; :: thesis: ex y being set st S2[x,y]
reconsider y = n as Real ;
take y ; :: thesis: S2[x,y]
thus S2[x,y] by A10, Th9; :: thesis: verum
end;
end;
end;
consider fn being Function such that
A15: ( dom fn = dom f & ( for x being set st x in dom f holds
S2[x,fn . x] ) ) from CLASSES1:sch 1(A5);
 rng fn c= ExtREAL
proof
now
let w be set ; :: thesis: ( w in rng fn implies b1 in ExtREAL )
assume w in rng fn ; :: thesis: b1 in ExtREAL
then consider v being set such that
A16: ( v in dom fn & w = fn . v ) by FUNCT_1:def 5;
per cases ( R_EAL n <= f . v or f . v < R_EAL n ) ;
suppose A17: f . v < R_EAL n ; :: thesis: b1 in ExtREAL
0 <= f . v by A2, SUPINF_2:70;
then consider k being Nat such that
A18: ( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= f . v & f . v < k / (2 |^ n) ) by A17, Th8;
fn . v = (k - 1) / (2 |^ n) by A15, A16, A18;
hence w in ExtREAL by A16, XXREAL_0:def 1; :: thesis: verum
end;
end;
end;
hence rng fn c= ExtREAL by TARSKI:def 3; :: thesis: verum
end;
then reconsider fn = fn as PartFunc of dom f, ExtREAL by A15, RELSET_1:11;
reconsider fn = fn as PartFunc of X, ExtREAL by A15, RELSET_1:13;
reconsider y = fn as Element of PFuncs X,ExtREAL by PARTFUN1:119;
take y ; :: thesis: S1[n,y]
thus S1[n,y] by A15; :: thesis: 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(A4);
 then consider F being Function of NAT , PFuncs X,ExtREAL such that
A19: for n being Element of NAT holds dom (F . n) = dom f and
A20: 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 ) ) ;
A21: now
let n be Nat; :: thesis: dom (F . n) = dom f
n in NAT by ORDINAL1:def 13;
hence dom (F . n) = dom f by A19; :: thesis: verum
end;
reconsider F = F as Functional_Sequence of X,ExtREAL ;
A22: for n being Nat holds F . n is_simple_func_in S
proof
let n be Nat; :: thesis: F . n is_simple_func_in S
reconsider n = n as Element of NAT by ORDINAL1:def 13;
now
let x be Element of X; :: thesis: ( x in dom (F . n) implies |.((F . n) . b1).| < +infty )
assume x in dom (F . n) ; :: thesis: |.((F . n) . b1).| < +infty
then A23: x in dom f by A21;
per cases ( R_EAL n <= f . x or f . x < R_EAL n ) ;
suppose R_EAL n <= f . x ; :: thesis: |.((F . n) . b1).| < +infty
then (F . n) . x = R_EAL n by A20, A23;
then ( - +infty < (F . n) . x & (F . n) . x < +infty ) by SUPINF_2:def 3, XXREAL_0:9;
hence |.((F . n) . x).| < +infty by EXTREAL2:59; :: thesis: verum
end;
suppose A24: f . x < R_EAL n ; :: thesis: |.((F . n) . b1).| < +infty
A25: ( 0 <= f . x & R_EAL n < +infty ) by A2, SUPINF_2:70, XXREAL_0:9;
then reconsider y = f . x as Real by A24, XXREAL_0:14;
set k = [\((2 |^ n) * y)/] + 1;
A26: 0 < 2 |^ n by PREPOWER:13;
then A27: ( 0 <= (2 |^ n) * y & (2 |^ n) * y < (2 |^ n) * n ) by A24, A25, XREAL_1:70;
( [\((2 |^ n) * y)/] <= (2 |^ n) * y & ((2 |^ n) * y) - 1 < [\((2 |^ n) * y)/] ) by INT_1:def 4;
then A28: ( (2 |^ n) * y < [\((2 |^ n) * y)/] + 1 & [\((2 |^ n) * y)/] < (2 |^ n) * n ) by A27, XREAL_1:21, XXREAL_0:2;
then A29: ( 0 + 1 <= [\((2 |^ n) * y)/] + 1 & [\((2 |^ n) * y)/] + 1 <= (2 |^ n) * n ) by A27, INT_1:20;
reconsider k = [\((2 |^ n) * y)/] + 1 as Element of NAT by A27, A28, INT_1:16;
( k - 1 <= (2 |^ n) * y & (2 |^ n) * y < k ) by INT_1:52, INT_1:def 4;
then ( (k - 1) / (2 |^ n) <= y & y < k / (2 |^ n) ) by A26, XREAL_1:81, XREAL_1:83;
then (F . n) . x = (k - 1) / (2 |^ n) by A20, A23, A29;
then ( -infty < (F . n) . x & (F . n) . x < +infty ) by XXREAL_0:9, XXREAL_0:12;
then ( - +infty < (F . n) . x & (F . n) . x < +infty ) by SUPINF_2:def 3;
hence |.((F . n) . x).| < +infty by EXTREAL2:59; :: thesis: verum
end;
end;
end;
then A30: F . n is real-valued by MESFUNC2:def 1;
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)) ) );
A31: now
let k be Nat; :: thesis: ( k in Seg ((N * n) + 1) implies ex B being Element of S st S2[B,b2] )
assume k in Seg ((N * n) + 1) ; :: thesis: ex B being Element of S st S2[B,b2]
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;
per cases ( k <> (N * n) + 1 or k = (N * n) + 1 ) ;
suppose A32: k <> (N * n) + 1 ; :: thesis: ex B being Element of S st S2[B,b2]
set B = (A /\ (great_eq_dom f,(R_EAL ((k1 - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (k1 / (2 |^ n))));
reconsider B = (A /\ (great_eq_dom f,(R_EAL ((k1 - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (k1 / (2 |^ n)))) as Element of S by A3, Th39;
take B = B; :: thesis: S2[k,B]
thus S2[k,B] by A32; :: thesis: verum
end;
suppose A33: k = (N * n) + 1 ; :: thesis: ex B being Element of S st S2[B,b2]
set B = A /\ (great_eq_dom f,(R_EAL n));
reconsider B = A /\ (great_eq_dom f,(R_EAL n)) as Element of S by A3, MESFUNC1:31;
take B = B; :: thesis: S2[k,B]
thus S2[k,B] by A33, NAT_1:13; :: thesis: verum
end;
end;
end;
consider G being FinSequence of S such that
A34: ( 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(A31);
 A35: len G = ((2 |^ n) * n) + 1 by A34, FINSEQ_1:def 3;
A36: now
let k be Nat; :: thesis: ( 1 <= k & k <= (2 |^ n) * n implies G . k = (A /\ (great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (k / (2 |^ n)))) )
assume A37: ( 1 <= k & k <= (2 |^ n) * n ) ; :: thesis: G . k = (A /\ (great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (k / (2 |^ n))))
A38: k in NAT by ORDINAL1:def 13;
k <= (N * n) + 1 by A37, NAT_1:12;
then k in Seg ((N * n) + 1) by A37, A38;
hence G . k = (A /\ (great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (k / (2 |^ n)))) by A34, A37; :: thesis: verum
end;
G is disjoint_valued
proof
now
let x, y be set ; :: thesis: ( x <> y implies G . b1 misses G . b2 )
assume A39: x <> y ; :: thesis: G . b1 misses G . b2
per cases ( not x in dom G or not y in dom G or ( x in dom G & y in dom G ) ) ;
suppose ( not x in dom G or not y in dom G ) ; :: thesis: G . b1 misses G . b2
then ( G . x = {} or G . y = {} ) by FUNCT_1:def 4;
hence G . x misses G . y by XBOOLE_1:65; :: thesis: verum
end;
suppose A40: ( x in dom G & y in dom G ) ; :: thesis: G . b1 misses G . b2
then reconsider x1 = x, y1 = y as Element of NAT ;
( x1 in Seg (len G) & y1 in Seg (len G) ) by A40, FINSEQ_1:def 3;
then A41: ( 1 <= x1 & x1 <= ((2 |^ n) * n) + 1 & 1 <= y1 & y1 <= ((2 |^ n) * n) + 1 ) by A35, FINSEQ_1:3;
now
per cases ( x1 < y1 or y1 < x1 ) by A39, XXREAL_0:1;
case A42: x1 < y1 ; :: thesis: ( ( y1 = ((2 |^ n) * n) + 1 implies G . x misses G . y ) & ( y1 <> ((2 |^ n) * n) + 1 implies G . x misses G . y ) )
hereby :: thesis: ( y1 <> ((2 |^ n) * n) + 1 implies G . x misses G . y )
assume A43: y1 = ((2 |^ n) * n) + 1 ; :: thesis: G . x misses G . y
then A44: x1 <= N * n by A42, NAT_1:13;
then A45: G . x = (A /\ (great_eq_dom f,(R_EAL ((x1 - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (x1 / (2 |^ n)))) by A36, A41;
A46: G . y = A /\ (great_eq_dom f,(R_EAL n)) by A34, A40, A43;
now
assume ex v being set st v in (G . x) /\ (G . y) ; :: thesis: contradiction
then consider v being set such that
A47: v in (G . x) /\ (G . y) ;
( v in G . x & v in G . y ) by A47, XBOOLE_0:def 4;
then A48: ( v in less_dom f,(R_EAL (x1 / (2 |^ n))) & v in great_eq_dom f,(R_EAL n) ) by A45, A46, XBOOLE_0:def 4;
then A49: f . v < R_EAL (x1 / (2 |^ n)) by MESFUNC1:def 12;
R_EAL n <= f . v by A48, MESFUNC1:def 15;
then R_EAL n < R_EAL (x1 / (2 |^ n)) by A49, XXREAL_0:2;
hence contradiction by A44, PREPOWER:13, XREAL_1:81; :: thesis: verum
end;
then (G . x) /\ (G . y) = {} by XBOOLE_0:def 1;
hence G . x misses G . y by XBOOLE_0:def 7; :: thesis: verum
end;
assume y1 <> ((2 |^ n) * n) + 1 ; :: thesis: G . x misses G . y
then y1 < (N * n) + 1 by A41, XXREAL_0:1;
then A50: y1 <= N * n by NAT_1:13;
then x1 <= (2 |^ n) * n by A42, XXREAL_0:2;
then A51: ( G . x = (A /\ (great_eq_dom f,(R_EAL ((x1 - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (x1 / (2 |^ n)))) & G . y = (A /\ (great_eq_dom f,(R_EAL ((y1 - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (y1 / (2 |^ n)))) ) by A36, A41, A50;
now
assume ex v being set st v in (G . x) /\ (G . y) ; :: thesis: contradiction
then consider v being set such that
A52: v in (G . x) /\ (G . y) ;
( v in G . x & v in G . y ) by A52, XBOOLE_0:def 4;
then A53: ( v in less_dom f,(R_EAL (x1 / (2 |^ n))) & v in A /\ (great_eq_dom f,(R_EAL ((y1 - 1) / (2 |^ n)))) ) by A51, XBOOLE_0:def 4;
then A54: ( v in less_dom f,(R_EAL (x1 / (2 |^ n))) & v in great_eq_dom f,(R_EAL ((y1 - 1) / (2 |^ n))) ) by XBOOLE_0:def 4;
A55: f . v < R_EAL (x1 / (2 |^ n)) by A53, MESFUNC1:def 12;
R_EAL ((y1 - 1) / (2 |^ n)) <= f . v by A54, MESFUNC1:def 15;
then R_EAL ((y1 - 1) / (2 |^ n)) < R_EAL (x1 / (2 |^ n)) by A55, XXREAL_0:2;
then y1 - 1 < x1 by XREAL_1:74;
then y1 < x1 + 1 by XREAL_1:21;
hence contradiction by A42, NAT_1:13; :: thesis: verum
end;
then (G . x) /\ (G . y) = {} by XBOOLE_0:def 1;
hence G . x misses G . y by XBOOLE_0:def 7; :: thesis: verum
end;
case A56: y1 < x1 ; :: thesis: ( ( x1 <> ((2 |^ n) * n) + 1 implies G . x misses G . y ) & ( x1 = ((2 |^ n) * n) + 1 implies G . x misses G . y ) )
hereby :: thesis: ( x1 = ((2 |^ n) * n) + 1 implies G . x misses G . y )
assume x1 <> ((2 |^ n) * n) + 1 ; :: thesis: G . x misses G . y
then x1 < (N * n) + 1 by A41, XXREAL_0:1;
then A57: x1 <= N * n by NAT_1:13;
then y1 <= (2 |^ n) * n by A56, XXREAL_0:2;
then A58: ( G . y = (A /\ (great_eq_dom f,(R_EAL ((y1 - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (y1 / (2 |^ n)))) & G . x = (A /\ (great_eq_dom f,(R_EAL ((x1 - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (x1 / (2 |^ n)))) ) by A36, A41, A57;
now
assume ex v being set st v in (G . x) /\ (G . y) ; :: thesis: contradiction
then consider v being set such that
A59: v in (G . x) /\ (G . y) ;
( v in G . x & v in G . y ) by A59, XBOOLE_0:def 4;
then A60: ( v in less_dom f,(R_EAL (y1 / (2 |^ n))) & v in A /\ (great_eq_dom f,(R_EAL ((x1 - 1) / (2 |^ n)))) ) by A58, XBOOLE_0:def 4;
then A61: ( v in less_dom f,(R_EAL (y1 / (2 |^ n))) & v in great_eq_dom f,(R_EAL ((x1 - 1) / (2 |^ n))) ) by XBOOLE_0:def 4;
A62: f . v < R_EAL (y1 / (2 |^ n)) by A60, MESFUNC1:def 12;
R_EAL ((x1 - 1) / (2 |^ n)) <= f . v by A61, MESFUNC1:def 15;
then R_EAL ((x1 - 1) / (2 |^ n)) < R_EAL (y1 / (2 |^ n)) by A62, XXREAL_0:2;
then x1 - 1 < y1 by XREAL_1:74;
then x1 < y1 + 1 by XREAL_1:21;
hence contradiction by A56, NAT_1:13; :: thesis: verum
end;
then (G . x) /\ (G . y) = {} by XBOOLE_0:def 1;
hence G . x misses G . y by XBOOLE_0:def 7; :: thesis: verum
end;
assume A63: x1 = ((2 |^ n) * n) + 1 ; :: thesis: G . x misses G . y
then A64: y1 <= N * n by A56, NAT_1:13;
then A65: G . y = (A /\ (great_eq_dom f,(R_EAL ((y1 - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (y1 / (2 |^ n)))) by A36, A41;
A66: G . x = A /\ (great_eq_dom f,(R_EAL n)) by A34, A40, A63;
now
assume ex v being set st v in (G . x) /\ (G . y) ; :: thesis: contradiction
then consider v being set such that
A67: v in (G . x) /\ (G . y) ;
( v in G . x & v in G . y ) by A67, XBOOLE_0:def 4;
then A68: ( v in less_dom f,(R_EAL (y1 / (2 |^ n))) & v in great_eq_dom f,(R_EAL n) ) by A65, A66, XBOOLE_0:def 4;
then A69: f . v < R_EAL (y1 / (2 |^ n)) by MESFUNC1:def 12;
R_EAL n <= f . v by A68, MESFUNC1:def 15;
then R_EAL n < R_EAL (y1 / (2 |^ n)) by A69, XXREAL_0:2;
hence contradiction by A64, PREPOWER:13, XREAL_1:81; :: thesis: verum
end;
then (G . x) /\ (G . y) = {} by XBOOLE_0:def 1;
hence G . x misses G . y by XBOOLE_0:def 7; :: thesis: verum
end;
end;
end;
hence G . x misses G . y ; :: thesis: verum
end;
end;
end;
hence G is disjoint_valued by PROB_2:def 3; :: thesis: verum
end;
then reconsider G = G as Finite_Sep_Sequence of S ;
union (rng G) = dom f
proof
for v being set st v in union (rng G) holds
v in dom f
proof
let v be set ; :: thesis: ( v in union (rng G) implies v in dom f )
assume v in union (rng G) ; :: thesis: v in dom f
then consider B being set such that
A70: ( v in B & B in rng G ) by TARSKI:def 4;
consider m being set such that
A71: ( m in dom G & B = G . m ) by A70, FUNCT_1:def 5;
reconsider m = m as Element of NAT by A71;
A72: ( 1 <= m & m <= (N * n) + 1 ) by A34, A71, FINSEQ_1:3;
now
per cases ( m = (N * n) + 1 or m <> (N * n) + 1 ) ;
suppose m <> (N * n) + 1 ; :: thesis: v in A
then m < (N * n) + 1 by A72, XXREAL_0:1;
then m <= N * n by NAT_1:13;
then B = (A /\ (great_eq_dom f,(R_EAL ((m - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (m / (2 |^ n)))) by A34, A71;
then v in A /\ (great_eq_dom f,(R_EAL ((m - 1) / (2 |^ n)))) by A70, XBOOLE_0:def 4;
hence v in A by XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
hence v in dom f by A3; :: thesis: verum
end;
then A73: union (rng G) c= dom f by TARSKI:def 3;
for v being set st v in dom f holds
v in union (rng G)
proof
let v be set ; :: thesis: ( v in dom f implies v in union (rng G) )
assume A74: v in dom f ; :: thesis: 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 A75: f . v < R_EAL n ; :: thesis: 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
A76: ( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= f . v & f . v < k / (2 |^ n) ) by A75, Th8;
v in great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n))) by A74, A76, MESFUNC1:def 15;
then A77: v in A /\ (great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n)))) by A3, A74, XBOOLE_0:def 4;
v in less_dom f,(R_EAL (k / (2 |^ n))) by A74, A76, MESFUNC1:def 12;
then A78: v in (A /\ (great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (k / (2 |^ n)))) by A77, XBOOLE_0:def 4;
A79: k in NAT by ORDINAL1:def 13;
N * n <= (N * n) + 1 by NAT_1:11;
then k <= (N * n) + 1 by A76, XXREAL_0:2;
then A80: k in Seg ((N * n) + 1) by A76, A79;
take B = G . k; :: thesis: ( v in B & B in rng G )
thus ( v in B & B in rng G ) by A34, A76, A78, A80, FUNCT_1:12; :: thesis: verum
end;
suppose R_EAL n <= f . v ; :: thesis: ex B being set st
( v in B & B in rng G )
then v in great_eq_dom f,(R_EAL n) by A74, MESFUNC1:def 15;
then A81: v in A /\ (great_eq_dom f,(R_EAL n)) by A3, A74, XBOOLE_0:def 4;
set k = (N * n) + 1;
take B = G . ((N * n) + 1); :: thesis: ( v in B & B in rng G )
1 <= (N * n) + 1 by NAT_1:11;
then (N * n) + 1 in Seg ((N * n) + 1) ;
hence ( v in B & B in rng G ) by A34, A81, FUNCT_1:12; :: thesis: verum
end;
end;
end;
hence v in union (rng G) by TARSKI:def 4; :: thesis: verum
end;
then dom f c= union (rng G) by TARSKI:def 3;
hence union (rng G) = dom f by A73, XBOOLE_0:def 10; :: thesis: verum
end;
then A82: dom (F . n) = union (rng G) by A21;
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; :: thesis: 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
let x, y be Element of X; :: thesis: ( k in dom G & x in G . k & y in G . k implies (F . n) . x = (F . n) . y )
assume A83: ( k in dom G & x in G . k & y in G . k ) ; :: thesis: (F . n) . x = (F . n) . y
then A84: ( 1 <= k & k <= (N * n) + 1 ) by A34, FINSEQ_1:3;
now
per cases ( k = (N * n) + 1 or k <> (N * n) + 1 ) ;
suppose k = (N * n) + 1 ; :: thesis: (F . n) . x = (F . n) . y
then G . k = A /\ (great_eq_dom f,(R_EAL n)) by A34, A83;
then A85: ( x in A & x in great_eq_dom f,(R_EAL n) & y in A & y in great_eq_dom f,(R_EAL n) ) by A83, XBOOLE_0:def 4;
then R_EAL n <= f . x by MESFUNC1:def 15;
then A86: (F . n) . x = R_EAL n by A3, A20, A85;
R_EAL n <= f . y by A85, MESFUNC1:def 15;
hence (F . n) . x = (F . n) . y by A3, A20, A85, A86; :: thesis: verum
end;
suppose k <> (N * n) + 1 ; :: thesis: (F . n) . x = (F . n) . y
then k < (N * n) + 1 by A84, XXREAL_0:1;
then A87: k <= N * n by NAT_1:13;
then G . k = (A /\ (great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n))))) /\ (less_dom f,(R_EAL (k / (2 |^ n)))) by A34, A83;
then A88: ( x in A /\ (great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n)))) & x in less_dom f,(R_EAL (k / (2 |^ n))) & y in A /\ (great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n)))) & y in less_dom f,(R_EAL (k / (2 |^ n))) ) by A83, XBOOLE_0:def 4;
then A89: ( x in A & x in great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n))) & y in A & y in great_eq_dom f,(R_EAL ((k - 1) / (2 |^ n))) ) by XBOOLE_0:def 4;
A90: f . x < R_EAL (k / (2 |^ n)) by A88, MESFUNC1:def 12;
A91: f . y < R_EAL (k / (2 |^ n)) by A88, MESFUNC1:def 12;
A92: R_EAL ((k - 1) / (2 |^ n)) <= f . y by A89, MESFUNC1:def 15;
R_EAL ((k - 1) / (2 |^ n)) <= f . x by A89, MESFUNC1:def 15;
then (F . n) . x = R_EAL ((k - 1) / (2 |^ n)) by A3, A20, A84, A87, A89, A90;
hence (F . n) . x = (F . n) . y by A3, A20, A84, A87, A89, A91, A92; :: thesis: verum
end;
end;
end;
hence (F . n) . x = (F . n) . y ; :: thesis: verum
end;
hence F . n is_simple_func_in S by A30, A82, MESFUNC2:def 5; :: thesis: verum
end;
A93: for n being Nat holds F . n is nonnegative
proof
let n be Nat; :: thesis: F . n is nonnegative
reconsider n = n as Element of NAT by ORDINAL1:def 13;
now
let x be set ; :: thesis: ( x in dom (F . n) implies 0 <= (F . n) . b1 )
assume x in dom (F . n) ; :: thesis: 0 <= (F . n) . b1
then A94: x in dom f by A21;
per cases ( n <= f . x or f . x < n ) ;
suppose n <= f . x ; :: thesis: 0 <= (F . n) . b1
hence 0 <= (F . n) . x by A20, A94; :: thesis: verum
end;
suppose A95: f . x < n ; :: thesis: 0 <= (F . n) . b1
0 <= f . x by A2, SUPINF_2:70;
then consider k being Nat such that
A96: ( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= f . x & f . x < k / (2 |^ n) ) by A95, Th8;
A97: (F . n) . x = (k - 1) / (2 |^ n) by A20, A94, A96;
( 0 <= k - 1 & 2 |^ n > 0 ) by A96, XREAL_1:50;
hence 0 <= (F . n) . x by A97; :: thesis: verum
end;
end;
end;
hence F . n is nonnegative by SUPINF_2:71; :: thesis: verum
end;
A98: 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; :: thesis: ( n <= m implies for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x )
assume A99: n <= m ; :: thesis: 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; :: thesis: ( x in dom f implies (F . n) . x <= (F . m) . x )
assume A100: x in dom f ; :: thesis: (F . n) . x <= (F . m) . x
per cases ( R_EAL m <= f . x or f . x < R_EAL m ) ;
suppose A101: R_EAL m <= f . x ; :: thesis: (F . n) . x <= (F . m) . x
then A102: (F . m) . x = R_EAL m by A20, A100;
R_EAL n <= f . x by A99, A101, XXREAL_0:2;
hence (F . n) . x <= (F . m) . x by A20, A99, A100, A102; :: thesis: verum
end;
suppose A103: f . x < R_EAL m ; :: thesis: (F . n) . x <= (F . m) . x
A104: 0 <= f . x by A2, SUPINF_2:70;
then consider M being Nat such that
A105: ( 1 <= M & M <= (2 |^ m) * m & (M - 1) / (2 |^ m) <= f . x & f . x < M / (2 |^ m) ) by A103, Th8;
reconsider M = M as Element of NAT by ORDINAL1:def 13;
A106: (F . m) . x = (M - 1) / (2 |^ m) by A20, A100, A105;
per cases ( R_EAL n <= f . x or f . x < R_EAL n ) ;
suppose A107: R_EAL n <= f . x ; :: thesis: (F . n) . x <= (F . m) . x
then A108: (F . n) . x = R_EAL n by A20, A100;
A109: n < M / (2 |^ m) by A105, A107, XXREAL_0:2;
A110: 0 < 2 |^ m by PREPOWER:13;
A111: (2 |^ m) * n < M by A109, PREPOWER:13, XREAL_1:81;
reconsider M1 = 2 |^ m as Element of NAT ;
(M1 * n) + 1 <= M by A111, NAT_1:13;
then M1 * n <= M - 1 by XREAL_1:21;
hence (F . n) . x <= (F . m) . x by A106, A108, A110, XREAL_1:79; :: thesis: verum
end;
suppose f . x < R_EAL n ; :: thesis: (F . n) . x <= (F . m) . x
then consider N1 being Nat such that
A112: ( 1 <= N1 & N1 <= (2 |^ n) * n & (N1 - 1) / (2 |^ n) <= f . x & f . x < N1 / (2 |^ n) ) by A104, Th8;
reconsider N1 = N1 as Element of NAT by ORDINAL1:def 13;
A113: (F . n) . x = (N1 - 1) / (2 |^ n) by A20, A100, A112;
consider k being Nat such that
A114: m = n + k by A99, NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A115: ( 2 |^ n > 0 & 2 |^ k > 0 & 2 |^ (n + k) > 0 ) by PREPOWER:13;
reconsider K = 2 |^ k as Element of NAT ;
R_EAL ((N1 - 1) / (2 |^ n)) < R_EAL (M / (2 |^ (n + k))) by A105, A112, A114, 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 (K * (N1 - 1)) / ((2 |^ n) * (2 |^ k)) <= (M - 1) / (2 |^ (n + k)) by NEWTON:13;
hence (F . n) . x <= (F . m) . x by A106, A113, A114, A115, XCMPLX_1:92; :: thesis: verum
end;
end;
end;
end;
end;
now
let x be Element of X; :: thesis: ( x in dom f implies ( F # b1 is convergent & lim (F # b1) = f . b1 ) )
assume A116: x in dom f ; :: thesis: ( F # b1 is convergent & lim (F # b1) = f . b1 )
per cases ( |.(f . x).| = +infty or |.(f . x).| <> +infty ) ;
suppose A117: |.(f . x).| = +infty ; :: thesis: ( F # b1 is convergent & lim (F # b1) = f . b1 )
then A118: f . x = +infty by A117, EXTREAL2:50;
for g being real number st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= (F # x) . m
proof
let g be real number ; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= (F # x) . m )
assume 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= (F # x) . m
then reconsider n = [/g\] as Nat by INT_1:80;
A119: g <= n by INT_1:def 5;
for m being Nat st n <= m holds
g <= (F # x) . m
proof
let m be Nat; :: thesis: ( n <= m implies g <= (F # x) . m )
assume n <= m ; :: thesis: g <= (F # x) . m
then A120: g <= m by A119, XXREAL_0:2;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
R_EAL m <= f . x by A118, XXREAL_0:4;
then (F . m) . x = R_EAL m by A20, A116;
hence g <= (F # x) . m by A120, Def13; :: thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
g <= (F # x) . m ; :: thesis: verum
end;
then A121: F # x is convergent_to_+infty by Def9;
then F # x is convergent by Def11;
hence ( F # x is convergent & lim (F # x) = f . x ) by A118, A121, Def12; :: thesis: verum
end;
suppose |.(f . x).| <> +infty ; :: thesis: ( F # b1 is convergent & lim (F # b1) = f . b1 )
then reconsider g = f . x as Real by EXTREAL2:67, XXREAL_0:14;
A122: f . x = R_EAL g ;
A123: 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
let p be real number ; :: thesis: ( 0 < p implies ex k being Nat st
for j being Nat st j >= k holds
|.(((F # x) . j) - (f . x)).| < p )
assume 0 < p ; :: thesis: 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
A124: 1 / (2 |^ N1) <= p by PREPOWER:106;
A125: for k being Nat st k >= N1 holds
1 / (2 |^ k) <= p
proof
let k be Nat; :: thesis: ( k >= N1 implies 1 / (2 |^ k) <= p )
assume k >= N1 ; :: thesis: 1 / (2 |^ k) <= p
then consider i being Nat such that
A126: k = N1 + i by NAT_1:10;
A127: ( 2 |^ N1 > 0 & 2 |^ i >= 1 ) by PREPOWER:19;
(2 |^ N1) * (2 |^ i) >= 2 |^ N1 by PREPOWER:19, XREAL_1:153;
then 2 |^ k >= 2 |^ N1 by A126, NEWTON:13;
then (2 |^ k) " <= (2 |^ N1) " by A127, XREAL_1:87;
then 1 / (2 |^ k) <= (2 |^ N1) " by XCMPLX_1:217;
then 1 / (2 |^ k) <= 1 / (2 |^ N1) by XCMPLX_1:217;
hence 1 / (2 |^ k) <= p by A124, XXREAL_0:2; :: thesis: verum
end;
A128: 0 <= g by A2, SUPINF_2:70;
set N2 = [/g\] + 1;
A129: ( g <= [/g\] & [/g\] < [/g\] + 1 ) by INT_1:def 5, XREAL_1:31;
then A130: g < [/g\] + 1 by XXREAL_0:2;
reconsider N2 = [/g\] + 1 as Element of NAT by A128, A129, INT_1:16;
A131: for N being Nat st N >= N2 holds
|.(((F # x) . N) - (f . x)).| < 1 / (2 |^ N)
proof
let N be Nat; :: thesis: ( N >= N2 implies |.(((F # x) . N) - (f . x)).| < 1 / (2 |^ N) )
assume A132: N >= N2 ; :: thesis: |.(((F # x) . N) - (f . x)).| < 1 / (2 |^ N)
reconsider N = N as Element of NAT by ORDINAL1:def 13;
( 0 <= f . x & f . x < N ) by A2, A130, A132, SUPINF_2:70, XXREAL_0:2;
then consider m being Nat such that
A133: ( 1 <= m & m <= (2 |^ N) * N & (m - 1) / (2 |^ N) <= f . x & f . x < m / (2 |^ N) ) by Th8;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A134: (F # x) . N = (F . N) . x by Def13
.= (m - 1) / (2 |^ N) by A20, A116, A133 ;
- (((F # x) . N) - (f . x)) = (f . x) - ((F # x) . N) by EXTREAL2:15;
then A135: |.(((F # x) . N) - (f . x)).| = |.((f . x) - ((F # x) . N)).| by EXTREAL2:66;
(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 A136: (f . x) - ((F # x) . N) < 1 / (2 |^ N) by A133, A134, MEASURE6:12;
2 |^ N > 0 by PREPOWER:13;
then (2 |^ N) " > 0 ;
then 1 / (2 |^ N) > 0 by XCMPLX_1:217;
then A137: - (R_EAL (1 / (2 |^ N))) < 0 by EXTREAL1:25;
0 <= (f . x) - ((F # x) . N) by A133, A134, SUPINF_2:72;
hence |.(((F # x) . N) - (f . x)).| < 1 / (2 |^ N) by A135, A136, A137, EXTREAL2:59; :: thesis: verum
end;
reconsider k = max N2,N1 as Element of NAT ;
now
let j be Nat; :: thesis: ( j >= k implies |.(((F # x) . j) - (f . x)).| < p )
assume A138: j >= k ; :: thesis: |.(((F # x) . j) - (f . x)).| < p
( k >= N1 & k >= N2 ) by XXREAL_0:25;
then ( j >= N1 & j >= N2 ) by A138, XXREAL_0:2;
then ( 1 / (2 |^ j) <= p & |.(((F # x) . j) - (f . x)).| < R_EAL (1 / (2 |^ j)) ) by A125, A131;
hence |.(((F # x) . j) - (f . x)).| < p by XXREAL_0:2; :: thesis: verum
end;
hence ex k being Nat st
for j being Nat st j >= k holds
|.(((F # x) . j) - (f . x)).| < p ; :: thesis: verum
end;
then A139: F # x is convergent_to_finite_number by A122, Def8;
then F # x is convergent by Def11;
hence ( F # x is convergent & lim (F # x) = f . x ) by A122, A123, A139, Def12; :: thesis: verum
end;
end;
end;
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 A21, A22, A93, A98; :: thesis: verum