let X be non empty set ; :: thesis: for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let F be with_the_same_dom Functional_Sequence of X,ExtREAL; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let M be sigma_Measure of S; :: thesis: for E being Element of S
for f being PartFunc of X,ExtREAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let E be Element of S; :: thesis: for f being PartFunc of X,ExtREAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds
( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
let f be PartFunc of X,ExtREAL; :: thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f implies ( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) )
assume that
A1: M . E < +infty and
A2: E = dom (F . 0) and
A3: for n being Nat holds F . n is_integrable_on M and
A4: F is_uniformly_convergent_to f ; :: thesis: ( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) )
consider N being Nat such that
A5: for n being Nat
for x being set st n >= N & x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < 1 / 2 by A4, Def2;
reconsider N1 = N as Element of NAT by ORDINAL1:def 13;
consider h being PartFunc of X,ExtREAL such that
A6: h is_simple_func_in S and
A7: dom h = E and
A8: for x being set st x in E holds
h . x = 1. by MESFUNC5:47;
A9: max- h is_measurable_on E by A6, A7, MESFUNC2:28, MESFUNC2:37;
for x being set st x in E holds
h . x >= 0. by A8;
then A10: h is nonnegative by A7, SUPINF_2:71;
then A11: Integral (M,h) = integral' (M,h) by A6, MESFUNC5:95;
set AFN = |.(F . N).|;
A12: dom (F . N) = dom |.(F . N).| by MESFUNC1:def 10;
now
let x be set ; :: thesis: ( x in dom |.(F . N).| implies 0 <= |.(F . N).| . x )
assume x in dom |.(F . N).| ; :: thesis: 0 <= |.(F . N).| . x
then |.(F . N).| . x = |.((F . N) . x).| by MESFUNC1:def 10;
hence 0 <= |.(F . N).| . x by EXTREAL2:51; :: thesis: verum
end;
then A13: |.(F . N).| is nonnegative by SUPINF_2:71;
then A14: dom (|.(F . N).| + h) = (dom |.(F . N).|) /\ (dom h) by A10, MESFUNC5:28;
A15: for x being set st x in dom (F . 0) holds
|.(((F . N) . x) - (f . x)).| < 1 / 2 by A5;
A16: now
let x be set ; :: thesis: for n being Nat st n >= N & x in dom (F . 0) holds
|.(F . n).| . x <= (|.(F . N).| + h) . x
let n be Nat; :: thesis: ( n >= N & x in dom (F . 0) implies |.(F . n).| . x <= (|.(F . N).| + h) . x )
assume that
A17: n >= N and
A18: x in dom (F . 0) ; :: thesis: |.(F . n).| . x <= (|.(F . N).| + h) . x
A19: |.(((F . n) . x) - (f . x)).| < 1 / 2 by A5, A17, A18;
A20: |.(((F . N) . x) - (f . x)).| < 1 / 2 by A5, A18;
A21: now
A22: |.(((F . n) . x) - (f . x)).| < 1. by A19, XXREAL_0:2;
then A23: ((F . n) . x) - (f . x) < 1. by EXTREAL2:58;
A24: |.(((F . N) . x) - (f . x)).| < 1. by A20, XXREAL_0:2;
then A25: - 1. < ((F . N) . x) - (f . x) by EXTREAL2:58;
A26: ((F . N) . x) - (f . x) < 1. by A24, EXTREAL2:58;
assume A27: ( f . x = +infty or f . x = -infty ) ; :: thesis: |.((F . n) . x).| <= |.((F . N) . x).| + 1.
- 1. < ((F . n) . x) - (f . x) by A22, EXTREAL2:58;
then ( ( (F . n) . x = +infty & (F . N) . x = +infty ) or ( (F . n) . x = -infty & (F . N) . x = -infty ) ) by A27, A25, A23, A26, XXREAL_3:64, XXREAL_3:65;
hence |.((F . n) . x).| <= |.((F . N) . x).| + 1. by EXTREAL2:67, XXREAL_3:63; :: thesis: verum
end;
dom (|.(F . N).| + h) = (dom |.(F . N).|) /\ (dom h) by A10, A13, MESFUNC5:28;
then dom (|.(F . N).| + h) = E /\ E by A2, A7, A12, MESFUNC8:def 2;
then (|.(F . N).| . x) + (h . x) = (|.(F . N).| + h) . x by A2, A18, MESFUNC1:def 3;
then A28: (|.(F . N).| . x) + 1. = (|.(F . N).| + h) . x by A2, A8, A18;
dom (F . n) = E by A2, MESFUNC8:def 2;
then A29: x in dom |.(F . n).| by A2, A18, MESFUNC1:def 10;
A30: now
A31: 0 <= |.(((F . n) . x) - (f . x)).| by EXTREAL2:51;
|.(((F . n) . x) - (f . x)).| < +infty by A19, XXREAL_0:2, XXREAL_0:9;
then reconsider a = |.(((F . n) . x) - (f . x)).| as Real by A31, XXREAL_0:14;
|.((f . x) - ((F . N) . x)).| < 1 / 2 by A20, MESFUNC5:1;
then A32: |.((f . x) - ((F . N) . x)).| < +infty by XXREAL_0:2, XXREAL_0:9;
0 <= |.((f . x) - ((F . N) . x)).| by EXTREAL2:51;
then reconsider b = |.((f . x) - ((F . N) . x)).| as Real by A32, XXREAL_0:14;
assume A33: f . x in REAL ; :: thesis: |.((F . n) . x).| <= |.((F . N) . x).| + 1.
A34: now
assume ( (F . N) . x = +infty or (F . N) . x = -infty ) ; :: thesis: contradiction
then ( ((F . N) . x) - (f . x) = +infty or ((F . N) . x) - (f . x) = -infty ) by A33, XXREAL_3:13, XXREAL_3:14;
then 1. < |.(((F . N) . x) - (f . x)).| by EXTREAL2:67, XXREAL_0:9;
hence contradiction by A15, A18, XXREAL_0:2; :: thesis: verum
end;
A35: now
assume ( (F . n) . x = +infty or (F . n) . x = -infty ) ; :: thesis: contradiction
then ( ((F . n) . x) - (f . x) = +infty or ((F . n) . x) - (f . x) = -infty ) by A33, XXREAL_3:13, XXREAL_3:14;
hence contradiction by A19, EXTREAL2:67, XXREAL_0:9; :: thesis: verum
end;
then (F . n) . x in REAL by XXREAL_0:14;
then A36: |.((F . n) . x).| - |.((F . N) . x).| <= |.(((F . n) . x) - ((F . N) . x)).| by EXTREAL2:68;
b <= 1 / 2 by A20, MESFUNC5:1;
then a + b < (1 / 2) + (1 / 2) by A19, XREAL_1:10;
then A37: |.(((F . n) . x) - (f . x)).| + |.((f . x) - ((F . N) . x)).| < 1 by SUPINF_2:1;
(- (f . x)) + (f . x) = 0. by XXREAL_3:7;
then ((F . n) . x) - ((F . N) . x) = (((F . n) . x) + ((- (f . x)) + (f . x))) - ((F . N) . x) by XXREAL_3:4;
then ((F . n) . x) - ((F . N) . x) = ((((F . n) . x) + (- (f . x))) + (f . x)) - ((F . N) . x) by A33, A35, XXREAL_3:30;
then ((F . n) . x) - ((F . N) . x) = (((F . n) . x) - (f . x)) + ((f . x) - ((F . N) . x)) by A33, A34, XXREAL_3:31;
then |.(((F . n) . x) - ((F . N) . x)).| <= |.(((F . n) . x) - (f . x)).| + |.((f . x) - ((F . N) . x)).| by EXTREAL2:61;
then |.(((F . n) . x) - ((F . N) . x)).| < 1 by A37, XXREAL_0:2;
then |.((F . n) . x).| - |.((F . N) . x).| <= 1. by A36, XXREAL_0:2;
hence |.((F . n) . x).| <= |.((F . N) . x).| + 1. by XXREAL_3:63; :: thesis: verum
end;
x in dom |.(F . N).| by A12, A18, MESFUNC8:def 2;
then |.((F . n) . x).| <= (|.(F . N).| . x) + 1. by A30, A21, MESFUNC1:def 10, XXREAL_0:14;
hence |.(F . n).| . x <= (|.(F . N).| + h) . x by A28, A29, MESFUNC1:def 10; :: thesis: verum
end;
A38: for x being Element of X
for n being Nat st x in E holds
|.((F ^\ N1) . n).| . x <= (|.(F . N).| + h) . x
proof
let x be Element of X; :: thesis: for n being Nat st x in E holds
|.((F ^\ N1) . n).| . x <= (|.(F . N).| + h) . x
let n be Nat; :: thesis: ( x in E implies |.((F ^\ N1) . n).| . x <= (|.(F . N).| + h) . x )
A39: (F ^\ N1) . n = F . (n + N) by NAT_1:def 3;
assume x in E ; :: thesis: |.((F ^\ N1) . n).| . x <= (|.(F . N).| + h) . x
hence |.((F ^\ N1) . n).| . x <= (|.(F . N).| + h) . x by A2, A16, A39, NAT_1:11; :: thesis: verum
end;
A40: max+ h is_measurable_on E by A6, MESFUNC2:27, MESFUNC2:37;
for x being set st x in dom (max- h) holds
0. <= (max- h) . x by MESFUNC2:15;
then A41: max- h is nonnegative by SUPINF_2:71;
A42: for n being Nat holds F . n is_measurable_on E
proof
let n be Nat; :: thesis: F . n is_measurable_on E
F . n is_integrable_on M by A3;
then ex A being Element of S st
( A = dom (F . n) & F . n is_measurable_on A ) by MESFUNC5:def 17;
hence F . n is_measurable_on E by A2, MESFUNC8:def 2; :: thesis: verum
end;
then A43: F . N is_measurable_on E ;
(F ^\ N1) . 0 = F . (0 + N) by NAT_1:def 3;
then A44: dom ((F ^\ N1) . 0) = E by A2, MESFUNC8:def 2;
A45: now
let x be Element of X; :: thesis: ( x in dom f implies (lim F) . x = f . x )
assume x in dom f ; :: thesis: (lim F) . x = f . x
then A46: x in dom (F . 0) by A4, Def2;
then A47: x in dom (lim F) by MESFUNC8:def 10;
lim (F # x) = f . x by A4, A46, Th21;
hence (lim F) . x = f . x by A47, MESFUNC8:def 10; :: thesis: verum
end;
dom f = dom (F . 0) by A4, Def2;
then dom (lim F) = dom f by MESFUNC8:def 10;
then A48: lim F = f by A45, PARTFUN1:34;
A49: F . N is_integrable_on M by A3;
E = dom (F . N) by A2, MESFUNC8:def 2;
then A50: |.(F . N).| is_integrable_on M by A49, A43, MESFUNC5:106;
deffunc H1( Element of NAT ) -> Element of ExtREAL = Integral (M,(F . $1));
A51: (R_EAL 1) * +infty = +infty by XXREAL_3:def 5;
A52: now
let x be Element of X; :: thesis: ( x in dom h implies |.h.| . x = h . x )
assume x in dom h ; :: thesis: |.h.| . x = h . x
then A53: x in dom |.h.| by MESFUNC1:def 10;
0 <= h . x by A10, SUPINF_2:70;
then |.(h . x).| = h . x by EXTREAL1:def 3;
hence |.h.| . x = h . x by A53, MESFUNC1:def 10; :: thesis: verum
end;
dom h = dom |.h.| by MESFUNC1:def 10;
then A54: h = |.h.| by A52, PARTFUN1:34;
Integral (M,h) = integral+ (M,h) by A6, A10, MESFUNC5:95;
then integral+ (M,h) = (R_EAL 1) * (M . (dom h)) by A7, A8, A11, MESFUNC5:110;
then A55: integral+ (M,|.h.|) < +infty by A1, A7, A54, A51, XXREAL_3:83;
A56: for n being Nat holds (F ^\ N1) . n is_measurable_on E
proof
let n be Nat; :: thesis: (F ^\ N1) . n is_measurable_on E
(F ^\ N1) . n = F . (n + N) by NAT_1:def 3;
hence (F ^\ N1) . n is_measurable_on E by A42; :: thesis: verum
end;
A57: for x being Element of X st x in E holds
( (F ^\ N1) # x is convergent & lim (F # x) = lim ((F ^\ N1) # x) )
proof
let x be Element of X; :: thesis: ( x in E implies ( (F ^\ N1) # x is convergent & lim (F # x) = lim ((F ^\ N1) # x) ) )
A58: now
let n be Element of NAT ; :: thesis: ((F ^\ N1) # x) . n = ((F # x) ^\ N1) . n
((F ^\ N1) # x) . n = ((F ^\ N1) . n) . x by MESFUNC5:def 13;
then ((F ^\ N1) # x) . n = (F . (n + N)) . x by NAT_1:def 3;
then ((F ^\ N1) # x) . n = (F # x) . (n + N) by MESFUNC5:def 13;
hence ((F ^\ N1) # x) . n = ((F # x) ^\ N1) . n by NAT_1:def 3; :: thesis: verum
end;
assume x in E ; :: thesis: ( (F ^\ N1) # x is convergent & lim (F # x) = lim ((F ^\ N1) # x) )
then A59: F # x is convergent by A2, A4, Th21;
then (F # x) ^\ N1 is convergent by RINFSUP2:21;
hence (F ^\ N1) # x is convergent by A58, FUNCT_2:113; :: thesis: lim (F # x) = lim ((F ^\ N1) # x)
lim (F # x) = lim ((F # x) ^\ N1) by A59, RINFSUP2:21;
hence lim (F # x) = lim ((F ^\ N1) # x) by A58, FUNCT_2:113; :: thesis: verum
end;
then for x being Element of X st x in E holds
(F ^\ N1) # x is convergent ;
then A60: lim (F ^\ N1) is_measurable_on E by A56, A44, MESFUNC8:25;
dom (lim (F ^\ N1)) = E by A44, MESFUNC8:def 10;
then A61: dom (lim F) = dom (lim (F ^\ N1)) by A2, MESFUNC8:def 10;
A62: now
let x be Element of X; :: thesis: ( x in dom (lim F) implies (lim F) . x = (lim (F ^\ N1)) . x )
assume A63: x in dom (lim F) ; :: thesis: (lim F) . x = (lim (F ^\ N1)) . x
then x in E by A2, MESFUNC8:def 10;
then A64: lim (F # x) = lim ((F ^\ N1) # x) by A57;
lim ((F ^\ N1) # x) = (lim (F ^\ N1)) . x by A61, A63, MESFUNC8:def 10;
hence (lim F) . x = (lim (F ^\ N1)) . x by A63, A64, MESFUNC8:def 10; :: thesis: verum
end;
A65: dom (max- h) = dom h by MESFUNC2:def 3;
then A66: (max- h) | E = max- h by A7, RELAT_1:97;
A67: dom (max+ h) = dom h by MESFUNC2:def 2;
then A68: (max+ h) | E = max+ h by A7, RELAT_1:97;
for x being set st x in dom (max+ h) holds
0. <= (max+ h) . x by MESFUNC2:14;
then A69: max+ h is nonnegative by SUPINF_2:71;
then dom ((max+ h) + (max- h)) = (dom (max+ h)) /\ (dom (max- h)) by A41, MESFUNC5:28;
then ex C being Element of S st
( C = E & integral+ (M,((max+ h) + (max- h))) = (integral+ (M,((max+ h) | C))) + (integral+ (M,((max- h) | C))) ) by A7, A40, A9, A69, A41, A67, A65, MESFUNC5:84;
then A70: integral+ (M,|.h.|) = (integral+ (M,(max+ h))) + (integral+ (M,(max- h))) by A68, A66, MESFUNC2:26;
A71: h is_measurable_on E by A6, MESFUNC2:37;
then 0 <= integral+ (M,(max- h)) by A7, A41, A65, MESFUNC2:28, MESFUNC5:85;
then integral+ (M,(max+ h)) <> +infty by A70, A55, XXREAL_3:def 2;
then A72: integral+ (M,(max+ h)) < +infty by XXREAL_0:4;
0 <= integral+ (M,(max+ h)) by A7, A71, A69, A67, MESFUNC2:27, MESFUNC5:85;
then integral+ (M,(max- h)) <> +infty by A70, A55, XXREAL_3:def 2;
then integral+ (M,(max- h)) < +infty by XXREAL_0:4;
then h is_integrable_on M by A7, A71, A72, MESFUNC5:def 17;
then A73: |.(F . N).| + h is_integrable_on M by A50, MESFUNC5:114;
A74: E = dom |.(F . N).| by A2, A12, MESFUNC8:def 2;
then A75: |.(lim_inf (F ^\ N1)).| is_integrable_on M by A7, A73, A14, A38, A56, A44, Th17;
|.(F . N).| + h is nonnegative by A10, A13, MESFUNC5:28;
then consider J being ExtREAL_sequence such that
A76: for n being Nat holds J . n = Integral (M,((F ^\ N1) . n)) and
lim_inf J >= Integral (M,(lim_inf (F ^\ N1))) and
lim_sup J <= Integral (M,(lim_sup (F ^\ N1))) and
A77: ( ( for x being Element of X st x in E holds
(F ^\ N1) # x is convergent ) implies ( J is convergent & lim J = Integral (M,(lim (F ^\ N1))) ) ) by A7, A73, A14, A74, A38, A56, A44, Th18;
consider I being Function of NAT,ExtREAL such that
A78: for n being Element of NAT holds I . n = H1(n) from FUNCT_2:sch 4();
 reconsider I = I as ExtREAL_sequence ;
A79: dom (lim_inf (F ^\ N1)) = dom ((F ^\ N1) . 0) by MESFUNC8:def 8;
A80: now
let x be Element of X; :: thesis: ( x in dom (lim (F ^\ N1)) implies (lim (F ^\ N1)) . x = (lim_inf (F ^\ N1)) . x )
assume A81: x in dom (lim (F ^\ N1)) ; :: thesis: (lim (F ^\ N1)) . x = (lim_inf (F ^\ N1)) . x
then x in E by A44, MESFUNC8:def 10;
then (F ^\ N1) # x is convergent by A57;
hence (lim (F ^\ N1)) . x = (lim_inf (F ^\ N1)) . x by A81, MESFUNC8:14; :: thesis: verum
end;
dom (lim (F ^\ N1)) = dom ((F ^\ N1) . 0) by MESFUNC8:def 10;
then lim (F ^\ N1) = lim_inf (F ^\ N1) by A79, A80, PARTFUN1:34;
then A82: lim (F ^\ N1) is_integrable_on M by A44, A75, A79, A60, MESFUNC5:106;
A83: for n being Nat holds I . n = Integral (M,(F . n))
proof
let n be Nat; :: thesis: I . n = Integral (M,(F . n))
n is Element of NAT by ORDINAL1:def 13;
hence I . n = Integral (M,(F . n)) by A78; :: thesis: verum
end;
now
let n be Element of NAT ; :: thesis: J . n = (I ^\ N1) . n
A84: (F ^\ N1) . n = F . (n + N) by NAT_1:def 3;
A85: (I ^\ N1) . n = I . (n + N) by NAT_1:def 3;
J . n = Integral (M,((F ^\ N1) . n)) by A76;
hence J . n = (I ^\ N1) . n by A78, A84, A85; :: thesis: verum
end;
then A86: J = I ^\ N1 by FUNCT_2:113;
then A87: I is convergent by A57, A77, RINFSUP2:17;
lim I = lim J by A57, A77, A86, RINFSUP2:17;
then lim I = Integral (M,(lim F)) by A57, A61, A62, A77, PARTFUN1:34;
hence ( f is_integrable_on M & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) by A48, A61, A62, A82, A83, A87, PARTFUN1:34; :: thesis: verum