:: MESFUN10 semantic presentation
begin
theorem Th1: :: MESFUN10:1
for seq1, seq2 being ExtREAL_sequence st ( for n being Nat holds seq1 . n <= seq2 . n ) holds
inf (rng seq1) <= inf (rng seq2)
proof
let seq1, seq2 be ExtREAL_sequence; ::_thesis: ( ( for n being Nat holds seq1 . n <= seq2 . n ) implies inf (rng seq1) <= inf (rng seq2) )
assume A1: for n being Nat holds seq1 . n <= seq2 . n ; ::_thesis: inf (rng seq1) <= inf (rng seq2)
now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_seq2_holds_
inf_(rng_seq1)_<=_x
let x be ext-real number ; ::_thesis: ( x in rng seq2 implies inf (rng seq1) <= x )
A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_inf_(rng_seq1)_<=_seq2_._n
let n be Element of NAT ; ::_thesis: inf (rng seq1) <= seq2 . n
dom seq1 = NAT by FUNCT_2:def_1;
then A3: seq1 . n in rng seq1 by FUNCT_1:def_3;
A4: seq1 . n <= seq2 . n by A1;
inf (rng seq1) is LowerBound of rng seq1 by XXREAL_2:def_4;
then inf (rng seq1) <= seq1 . n by A3, XXREAL_2:def_2;
hence inf (rng seq1) <= seq2 . n by A4, XXREAL_0:2; ::_thesis: verum
end;
assume x in rng seq2 ; ::_thesis: inf (rng seq1) <= x
then ex z being set st
( z in dom seq2 & x = seq2 . z ) by FUNCT_1:def_3;
hence inf (rng seq1) <= x by A2; ::_thesis: verum
end;
then inf (rng seq1) is LowerBound of rng seq2 by XXREAL_2:def_2;
hence inf (rng seq1) <= inf (rng seq2) by XXREAL_2:def_4; ::_thesis: verum
end;
theorem Th2: :: MESFUN10:2
for seq1, seq2 being ExtREAL_sequence
for k being Nat st ( for n being Nat holds seq1 . n <= seq2 . n ) holds
( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k )
proof
let seq1, seq2 be ExtREAL_sequence; ::_thesis: for k being Nat st ( for n being Nat holds seq1 . n <= seq2 . n ) holds
( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k )
let k be Nat; ::_thesis: ( ( for n being Nat holds seq1 . n <= seq2 . n ) implies ( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k ) )
reconsider k1 = k as Element of NAT by ORDINAL1:def_12;
assume A1: for n being Nat holds seq1 . n <= seq2 . n ; ::_thesis: ( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k )
A2: now__::_thesis:_for_n_being_Nat_holds_(seq1_^\_k1)_._n_<=_(seq2_^\_k1)_._n
let n be Nat; ::_thesis: (seq1 ^\ k1) . n <= (seq2 ^\ k1) . n
A3: (seq2 ^\ k1) . n = seq2 . (n + k) by NAT_1:def_3;
(seq1 ^\ k1) . n = seq1 . (n + k) by NAT_1:def_3;
hence (seq1 ^\ k1) . n <= (seq2 ^\ k1) . n by A1, A3; ::_thesis: verum
end;
then sup (seq1 ^\ k1) <= sup (seq2 ^\ k1) by MESFUNC5:55;
then A4: (superior_realsequence seq1) . k <= sup (seq2 ^\ k1) by RINFSUP2:27;
inf (seq1 ^\ k1) <= inf (seq2 ^\ k1) by A2, Th1;
then (inferior_realsequence seq1) . k <= inf (seq2 ^\ k1) by RINFSUP2:27;
hence ( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k ) by A4, RINFSUP2:27; ::_thesis: verum
end;
theorem Th3: :: MESFUN10:3
for seq1, seq2 being ExtREAL_sequence st ( for n being Nat holds seq1 . n <= seq2 . n ) holds
( lim_inf seq1 <= lim_inf seq2 & lim_sup seq1 <= lim_sup seq2 )
proof
let seq1, seq2 be ExtREAL_sequence; ::_thesis: ( ( for n being Nat holds seq1 . n <= seq2 . n ) implies ( lim_inf seq1 <= lim_inf seq2 & lim_sup seq1 <= lim_sup seq2 ) )
assume for n being Nat holds seq1 . n <= seq2 . n ; ::_thesis: ( lim_inf seq1 <= lim_inf seq2 & lim_sup seq1 <= lim_sup seq2 )
then for n being Nat holds
( (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n & (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) by Th2;
hence ( lim_inf seq1 <= lim_inf seq2 & lim_sup seq1 <= lim_sup seq2 ) by Th1, MESFUNC5:55; ::_thesis: verum
end;
theorem Th4: :: MESFUN10:4
for seq being ExtREAL_sequence
for a being R_eal st ( for n being Nat holds seq . n >= a ) holds
inf seq >= a
proof
let seq be ExtREAL_sequence; ::_thesis: for a being R_eal st ( for n being Nat holds seq . n >= a ) holds
inf seq >= a
let a be R_eal; ::_thesis: ( ( for n being Nat holds seq . n >= a ) implies inf seq >= a )
assume A1: for n being Nat holds seq . n >= a ; ::_thesis: inf seq >= a
now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_seq_holds_
x_>=_a
let x be ext-real number ; ::_thesis: ( x in rng seq implies x >= a )
assume x in rng seq ; ::_thesis: x >= a
then ex z being set st
( z in dom seq & x = seq . z ) by FUNCT_1:def_3;
hence x >= a by A1; ::_thesis: verum
end;
then a is LowerBound of rng seq by XXREAL_2:def_2;
hence inf seq >= a by XXREAL_2:def_4; ::_thesis: verum
end;
theorem Th5: :: MESFUN10:5
for seq being ExtREAL_sequence
for a being R_eal st ( for n being Nat holds seq . n <= a ) holds
sup seq <= a
proof
let seq be ExtREAL_sequence; ::_thesis: for a being R_eal st ( for n being Nat holds seq . n <= a ) holds
sup seq <= a
let a be R_eal; ::_thesis: ( ( for n being Nat holds seq . n <= a ) implies sup seq <= a )
assume A1: for n being Nat holds seq . n <= a ; ::_thesis: sup seq <= a
now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_seq_holds_
x_<=_a
let x be ext-real number ; ::_thesis: ( x in rng seq implies x <= a )
assume x in rng seq ; ::_thesis: x <= a
then ex z being set st
( z in dom seq & x = seq . z ) by FUNCT_1:def_3;
hence x <= a by A1; ::_thesis: verum
end;
then a is UpperBound of rng seq by XXREAL_2:def_1;
hence sup seq <= a by XXREAL_2:def_3; ::_thesis: verum
end;
theorem Th6: :: MESFUN10:6
for X being non empty set
for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for x being Element of X
for n being Element of NAT st x in dom (inf (F ^\ n)) holds
(inf (F ^\ n)) . x = inf ((F # x) ^\ n)
proof
let X be non empty set ; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,ExtREAL
for x being Element of X
for n being Element of NAT st x in dom (inf (F ^\ n)) holds
(inf (F ^\ n)) . x = inf ((F # x) ^\ n)
let F be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for x being Element of X
for n being Element of NAT st x in dom (inf (F ^\ n)) holds
(inf (F ^\ n)) . x = inf ((F # x) ^\ n)
let x be Element of X; ::_thesis: for n being Element of NAT st x in dom (inf (F ^\ n)) holds
(inf (F ^\ n)) . x = inf ((F # x) ^\ n)
let n be Element of NAT ; ::_thesis: ( x in dom (inf (F ^\ n)) implies (inf (F ^\ n)) . x = inf ((F # x) ^\ n) )
now__::_thesis:_for_k_being_Element_of_NAT_holds_((F_^\_n)_#_x)_._k_=_((F_#_x)_^\_n)_._k
reconsider g = F as Function of NAT,(PFuncs (X,ExtREAL)) ;
let k be Element of NAT ; ::_thesis: ((F ^\ n) # x) . k = ((F # x) ^\ n) . k
((F ^\ n) # x) . k = ((F ^\ n) . k) . x by MESFUNC5:def_13;
then ((F ^\ n) # x) . k = (g . (n + k)) . x by NAT_1:def_3;
then ((F ^\ n) # x) . k = (F # x) . (n + k) by MESFUNC5:def_13;
hence ((F ^\ n) # x) . k = ((F # x) ^\ n) . k by NAT_1:def_3; ::_thesis: verum
end;
then A1: (F ^\ n) # x = (F # x) ^\ n by FUNCT_2:63;
assume x in dom (inf (F ^\ n)) ; ::_thesis: (inf (F ^\ n)) . x = inf ((F # x) ^\ n)
hence (inf (F ^\ n)) . x = inf ((F # x) ^\ n) by A1, MESFUNC8:def_3; ::_thesis: verum
end;
theorem Th7: :: MESFUN10:7
for X being non empty set
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 st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I )
proof
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 st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I )
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 st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I )
let M be sigma_Measure of S; ::_thesis: for E being Element of S st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I )
let E be Element of S; ::_thesis: ( E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) implies ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I ) )
assume that
A1: E = dom (F . 0) and
A2: for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ; ::_thesis: ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I )
set H = inferior_realsequence F;
deffunc H1( Element of NAT ) -> Element of K6(K7(X,ExtREAL)) = inf (F ^\ $1);
consider G being Function such that
A3: ( dom G = NAT & ( for n being Element of NAT holds G . n = H1(n) ) ) from FUNCT_1:sch_4();
now__::_thesis:_for_n_being_Element_of_NAT_holds_G_._n_is_PartFunc_of_X,ExtREAL
let n be Element of NAT ; ::_thesis: G . n is PartFunc of X,ExtREAL
G . n = inf (F ^\ n) by A3;
hence G . n is PartFunc of X,ExtREAL ; ::_thesis: verum
end;
then reconsider G = G as Functional_Sequence of X,ExtREAL by A3, SEQFUNC:1;
A4: for n being Element of NAT holds G . n = (inferior_realsequence F) . n
proof
let n be Element of NAT ; ::_thesis: G . n = (inferior_realsequence F) . n
(inferior_realsequence F) . n = inf (F ^\ n) by MESFUNC8:8;
hence G . n = (inferior_realsequence F) . n by A3; ::_thesis: verum
end;
then A5: G = inferior_realsequence F by FUNCT_2:63;
reconsider G = G as with_the_same_dom Functional_Sequence of X,ExtREAL by A4, FUNCT_2:63;
A6: dom ((inferior_realsequence F) . 0) = dom (G . 0) by A4;
A7: for n, m being Nat
for x being Element of X st n <= m & x in E holds
( (G . n) . x <= (G . m) . x & (G # x) . n <= (G # x) . m )
proof
let n, m be Nat; ::_thesis: for x being Element of X st n <= m & x in E holds
( (G . n) . x <= (G . m) . x & (G # x) . n <= (G # x) . m )
let x be Element of X; ::_thesis: ( n <= m & x in E implies ( (G . n) . x <= (G . m) . x & (G # x) . n <= (G # x) . m ) )
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def_12;
assume that
A8: n <= m and
A9: x in E ; ::_thesis: ( (G . n) . x <= (G . m) . x & (G # x) . n <= (G # x) . m )
(inferior_realsequence F) # x = inferior_realsequence (F # x) by A1, A9, MESFUNC8:7;
then ((inferior_realsequence F) # x) . n1 <= ((inferior_realsequence F) # x) . m1 by A8, RINFSUP2:7;
then ((inferior_realsequence F) . n) . x <= ((inferior_realsequence F) # x) . m by MESFUNC5:def_13;
hence (G . n) . x <= (G . m) . x by A5, MESFUNC5:def_13; ::_thesis: (G # x) . n <= (G # x) . m
then (G # x) . n <= (G . m) . x by MESFUNC5:def_13;
hence (G # x) . n <= (G # x) . m by MESFUNC5:def_13; ::_thesis: verum
end;
A10: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_
G_#_x_is_convergent
let x be Element of X; ::_thesis: ( x in E implies G # x is convergent )
assume x in E ; ::_thesis: G # x is convergent
then for n, m being Element of NAT st m <= n holds
(G # x) . m <= (G # x) . n by A7;
then G # x is non-decreasing by RINFSUP2:7;
hence G # x is convergent by RINFSUP2:37; ::_thesis: verum
end;
deffunc H2( Element of NAT ) -> Element of ExtREAL = Integral (M,(F . $1));
consider I being Function of NAT,ExtREAL such that
A11: for n being Element of NAT holds I . n = H2(n) from FUNCT_2:sch_4();
A12: for n being Nat holds G . n is_measurable_on E by A1, A2, A5, MESFUNC8:20;
A13: dom ((inferior_realsequence F) . 0) = dom (F . 0) by MESFUNC8:def_5;
then A14: dom (lim G) = E by A1, A6, MESFUNC8:def_9;
for x being set st x in dom (G . 0) holds
0 <= (G . 0) . x
proof
let x be set ; ::_thesis: ( x in dom (G . 0) implies 0 <= (G . 0) . x )
assume A15: x in dom (G . 0) ; ::_thesis: 0 <= (G . 0) . x
then reconsider x = x as Element of X ;
A16: now__::_thesis:_for_n_being_Nat_holds_0._<=_((F_#_x)_^\_0)_._n
let n be Nat; ::_thesis: 0. <= ((F # x) ^\ 0) . n
F . n is nonnegative by A2;
then 0 <= (F . n) . x by SUPINF_2:51;
then 0 <= (F # x) . (0 + n) by MESFUNC5:def_13;
hence 0. <= ((F # x) ^\ 0) . n by NAT_1:def_3; ::_thesis: verum
end;
(F ^\ 0) . 0 = F . (0 + 0) by NAT_1:def_3;
then dom (inf (F ^\ 0)) = dom (F . 0) by MESFUNC8:def_3;
then (inf (F ^\ 0)) . x = inf ((F # x) ^\ 0) by A13, A6, A15, Th6;
then (G . 0) . x = inf ((F # x) ^\ 0) by A3;
hence 0 <= (G . 0) . x by A16, Th4; ::_thesis: verum
end;
then A17: G . 0 is nonnegative by SUPINF_2:52;
for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(G . n) . x <= (G . m) . x by A7;
then consider J being ExtREAL_sequence such that
A18: for n being Nat holds J . n = Integral (M,(G . n)) and
A19: J is convergent and
A20: Integral (M,(lim G)) = lim J by A1, A13, A6, A17, A12, A10, MESFUNC9:52;
reconsider I = I as ExtREAL_sequence ;
for n being Nat holds J . n <= I . n
proof
let n be Nat; ::_thesis: J . n <= I . n
A21: dom (F . n) = E by A1, MESFUNC8:def_2;
A22: F . n is nonnegative by A2;
A23: n is Element of NAT by ORDINAL1:def_12;
A24: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(G_._n)_holds_
(G_._n)_._x_<=_(F_._n)_._x
let x be Element of X; ::_thesis: ( x in dom (G . n) implies (G . n) . x <= (F . n) . x )
assume A25: x in dom (G . n) ; ::_thesis: (G . n) . x <= (F . n) . x
(inferior_realsequence (F # x)) . n <= (F # x) . n by A23, RINFSUP2:8;
then ((inferior_realsequence F) . n) . x <= (F # x) . n by A5, A25, MESFUNC8:def_5;
then ((inferior_realsequence F) . n) . x <= (F . n) . x by MESFUNC5:def_13;
hence (G . n) . x <= (F . n) . x by A4, A23; ::_thesis: verum
end;
A26: F . n is_measurable_on E by A2;
A27: G . n is_measurable_on E by A1, A2, A5, MESFUNC8:20;
A28: dom (G . n) = E by A1, A13, A6, MESFUNC8:def_2;
A29: now__::_thesis:_for_x_being_set_st_x_in_dom_(G_._n)_holds_
0_<=_(G_._n)_._x
let x be set ; ::_thesis: ( x in dom (G . n) implies 0 <= (G . n) . x )
assume A30: x in dom (G . n) ; ::_thesis: 0 <= (G . n) . x
0 <= (G . 0) . x by A17, SUPINF_2:51;
hence 0 <= (G . n) . x by A7, A28, A30; ::_thesis: verum
end;
then G . n is nonnegative by SUPINF_2:52;
then integral+ (M,(G . n)) <= integral+ (M,(F . n)) by A21, A28, A26, A27, A22, A24, MESFUNC5:85;
then Integral (M,(G . n)) <= integral+ (M,(F . n)) by A28, A27, A29, MESFUNC5:88, SUPINF_2:52;
then A31: Integral (M,(G . n)) <= Integral (M,(F . n)) by A21, A26, A22, MESFUNC5:88;
I . n = Integral (M,(F . n)) by A11, A23;
hence J . n <= I . n by A18, A31; ::_thesis: verum
end;
then lim_inf J <= lim_inf I by Th3;
then A32: lim J <= lim_inf I by A19, RINFSUP2:41;
A33: dom (sup G) = E by A1, A13, A6, MESFUNC8:def_4;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_G)_holds_
(lim_G)_._x_=_(sup_G)_._x
let x be Element of X; ::_thesis: ( x in dom (lim G) implies (lim G) . x = (sup G) . x )
assume A34: x in dom (lim G) ; ::_thesis: (lim G) . x = (sup G) . x
then for n, m being Element of NAT st m <= n holds
(G # x) . m <= (G # x) . n by A7, A14;
then G # x is non-decreasing by RINFSUP2:7;
then A35: lim (G # x) = sup (G # x) by RINFSUP2:37;
(sup G) . x = sup (G # x) by A14, A33, A34, MESFUNC8:def_4;
hence (lim G) . x = (sup G) . x by A34, A35, MESFUNC8:def_9; ::_thesis: verum
end;
then A36: lim G = sup G by A14, A33, PARTFUN1:5;
take I ; ::_thesis: ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I )
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_12;
hence I . n = Integral (M,(F . n)) by A11; ::_thesis: verum
end;
hence ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I ) by A5, A20, A36, A32, MESFUNC8:11; ::_thesis: verum
end;
begin
theorem Th8: :: MESFUN10:8
for Y being non empty Subset of ExtREAL
for r being R_eal st r in REAL holds
sup ({r} + Y) = (sup {r}) + (sup Y)
proof
let Y be non empty Subset of ExtREAL; ::_thesis: for r being R_eal st r in REAL holds
sup ({r} + Y) = (sup {r}) + (sup Y)
let r be R_eal; ::_thesis: ( r in REAL implies sup ({r} + Y) = (sup {r}) + (sup Y) )
set X = {r};
assume A1: r in REAL ; ::_thesis: sup ({r} + Y) = (sup {r}) + (sup Y)
set W = {r} + Y;
A2: - r <> -infty by A1, XXREAL_3:23;
A3: - r <> +infty by A1, XXREAL_3:23;
now__::_thesis:_for_z_being_set_st_z_in_(-_{r})_+_({r}_+_Y)_holds_
z_in_Y
let z be set ; ::_thesis: ( z in (- {r}) + ({r} + Y) implies z in Y )
assume z in (- {r}) + ({r} + Y) ; ::_thesis: z in Y
then consider x, y being R_eal such that
A4: z = x + y and
A5: x in - {r} and
A6: y in {r} + Y ;
consider x1, y1 being R_eal such that
A7: y = x1 + y1 and
A8: x1 in {r} and
A9: y1 in Y by A6;
- x in - (- {r}) by A5;
then - x in {r} ;
then - x = r by TARSKI:def_1;
then z = (- r) + (r + y1) by A4, A8, A7, TARSKI:def_1;
then z = ((- r) + r) + y1 by A1, A3, A2, XXREAL_3:29;
then z = 0. + y1 by XXREAL_3:7;
hence z in Y by A9, XXREAL_3:4; ::_thesis: verum
end;
then A10: (- {r}) + ({r} + Y) c= Y by TARSKI:def_3;
A11: r in {r} by TARSKI:def_1;
now__::_thesis:_for_z_being_set_st_z_in_Y_holds_
z_in_(-_{r})_+_({r}_+_Y)
let z be set ; ::_thesis: ( z in Y implies z in (- {r}) + ({r} + Y) )
assume A12: z in Y ; ::_thesis: z in (- {r}) + ({r} + Y)
then reconsider y = z as Element of ExtREAL ;
(r + y) - r = ((- r) + r) + y by A1, A3, A2, XXREAL_3:29;
then (r + y) - r = 0. + y by XXREAL_3:7;
then A13: y = (r + y) - r by XXREAL_3:4;
A14: - r in - {r} by A11;
r + y in {r} + Y by A11, A12;
hence z in (- {r}) + ({r} + Y) by A14, A13; ::_thesis: verum
end;
then Y c= (- {r}) + ({r} + Y) by TARSKI:def_3;
then Y = (- {r}) + ({r} + Y) by A10, XBOOLE_0:def_10;
then sup Y <= (sup ({r} + Y)) + (sup (- {r})) by SUPINF_2:8;
then sup Y <= (sup ({r} + Y)) + (- (inf {r})) by SUPINF_2:15;
then sup Y <= (sup ({r} + Y)) - r by XXREAL_2:13;
then r + (sup Y) <= sup ({r} + Y) by A1, XXREAL_3:57;
then A15: (sup {r}) + (sup Y) <= sup ({r} + Y) by XXREAL_2:11;
sup ({r} + Y) <= (sup {r}) + (sup Y) by SUPINF_2:8;
hence sup ({r} + Y) = (sup {r}) + (sup Y) by A15, XXREAL_0:1; ::_thesis: verum
end;
theorem Th9: :: MESFUN10:9
for Y being non empty Subset of ExtREAL
for r being R_eal st r in REAL holds
inf ({r} + Y) = (inf {r}) + (inf Y)
proof
let Y be non empty Subset of ExtREAL; ::_thesis: for r being R_eal st r in REAL holds
inf ({r} + Y) = (inf {r}) + (inf Y)
let r be R_eal; ::_thesis: ( r in REAL implies inf ({r} + Y) = (inf {r}) + (inf Y) )
set X = {r};
assume A1: r in REAL ; ::_thesis: inf ({r} + Y) = (inf {r}) + (inf Y)
set W = {r} + Y;
set Z = - {r};
A2: - r <> -infty by A1, XXREAL_3:23;
A3: - r <> +infty by A1, XXREAL_3:23;
now__::_thesis:_for_z_being_set_st_z_in_(-_{r})_+_({r}_+_Y)_holds_
z_in_Y
let z be set ; ::_thesis: ( z in (- {r}) + ({r} + Y) implies z in Y )
assume z in (- {r}) + ({r} + Y) ; ::_thesis: z in Y
then consider x, y being R_eal such that
A4: z = x + y and
A5: x in - {r} and
A6: y in {r} + Y ;
consider x1, y1 being R_eal such that
A7: y = x1 + y1 and
A8: x1 in {r} and
A9: y1 in Y by A6;
- x in - (- {r}) by A5;
then - x in {r} ;
then - x = r by TARSKI:def_1;
then z = (- r) + (r + y1) by A4, A8, A7, TARSKI:def_1;
then z = ((- r) + r) + y1 by A1, A3, A2, XXREAL_3:29;
then z = 0. + y1 by XXREAL_3:7;
hence z in Y by A9, XXREAL_3:4; ::_thesis: verum
end;
then A10: (- {r}) + ({r} + Y) c= Y by TARSKI:def_3;
A11: r in {r} by TARSKI:def_1;
now__::_thesis:_for_z_being_set_st_z_in_Y_holds_
z_in_(-_{r})_+_({r}_+_Y)
let z be set ; ::_thesis: ( z in Y implies z in (- {r}) + ({r} + Y) )
assume A12: z in Y ; ::_thesis: z in (- {r}) + ({r} + Y)
then reconsider y = z as Element of ExtREAL ;
(r + y) - r = ((- r) + r) + y by A1, A3, A2, XXREAL_3:29;
then (r + y) - r = 0. + y by XXREAL_3:7;
then A13: y = (r + y) - r by XXREAL_3:4;
A14: - r in - {r} by A11;
r + y in {r} + Y by A11, A12;
hence z in (- {r}) + ({r} + Y) by A14, A13; ::_thesis: verum
end;
then Y c= (- {r}) + ({r} + Y) by TARSKI:def_3;
then Y = (- {r}) + ({r} + Y) by A10, XBOOLE_0:def_10;
then inf Y >= (inf ({r} + Y)) + (inf (- {r})) by SUPINF_2:9;
then inf Y >= (inf ({r} + Y)) + (- (sup {r})) by SUPINF_2:14;
then inf Y >= (inf ({r} + Y)) - r by XXREAL_2:11;
then r + (inf Y) >= inf ({r} + Y) by A1, XXREAL_3:52;
then A15: (inf {r}) + (inf Y) >= inf ({r} + Y) by XXREAL_2:13;
inf ({r} + Y) >= (inf {r}) + (inf Y) by SUPINF_2:9;
hence inf ({r} + Y) = (inf {r}) + (inf Y) by A15, XXREAL_0:1; ::_thesis: verum
end;
theorem Th10: :: MESFUN10:10
for seq1, seq2 being ExtREAL_sequence
for r being R_eal st r in REAL & ( for n being Nat holds seq1 . n = r + (seq2 . n) ) holds
( lim_inf seq1 = r + (lim_inf seq2) & lim_sup seq1 = r + (lim_sup seq2) )
proof
let seq1, seq2 be ExtREAL_sequence; ::_thesis: for r being R_eal st r in REAL & ( for n being Nat holds seq1 . n = r + (seq2 . n) ) holds
( lim_inf seq1 = r + (lim_inf seq2) & lim_sup seq1 = r + (lim_sup seq2) )
let r be R_eal; ::_thesis: ( r in REAL & ( for n being Nat holds seq1 . n = r + (seq2 . n) ) implies ( lim_inf seq1 = r + (lim_inf seq2) & lim_sup seq1 = r + (lim_sup seq2) ) )
assume that
A1: r in REAL and
A2: for n being Nat holds seq1 . n = r + (seq2 . n) ; ::_thesis: ( lim_inf seq1 = r + (lim_inf seq2) & lim_sup seq1 = r + (lim_sup seq2) )
reconsider R1 = rng (inferior_realsequence seq1), R2 = rng (inferior_realsequence seq2), P1 = rng (superior_realsequence seq1), P2 = rng (superior_realsequence seq2) as non empty Subset of ExtREAL ;
now__::_thesis:_for_z_being_set_st_z_in_{r}_+_R2_holds_
z_in_R1
let z be set ; ::_thesis: ( z in {r} + R2 implies z in R1 )
assume z in {r} + R2 ; ::_thesis: z in R1
then consider z2, z3 being R_eal such that
A3: z = z2 + z3 and
A4: z2 in {r} and
A5: z3 in R2 ;
consider n being set such that
A6: n in NAT and
A7: (inferior_realsequence seq2) . n = z3 by A5, FUNCT_2:11;
reconsider n = n as Element of NAT by A6;
consider Y2 being non empty Subset of ExtREAL such that
A8: Y2 = { (seq2 . k) where k is Element of NAT : n <= k } and
A9: z3 = inf Y2 by A7, RINFSUP2:def_6;
consider Y1 being non empty Subset of ExtREAL such that
A10: Y1 = { (seq1 . k) where k is Element of NAT : n <= k } and
A11: (inferior_realsequence seq1) . n = inf Y1 by RINFSUP2:def_6;
now__::_thesis:_for_w_being_set_st_w_in_Y1_holds_
w_in_{r}_+_Y2
let w be set ; ::_thesis: ( w in Y1 implies w in {r} + Y2 )
A12: r in {r} by TARSKI:def_1;
assume w in Y1 ; ::_thesis: w in {r} + Y2
then consider k1 being Element of NAT such that
A13: w = seq1 . k1 and
A14: n <= k1 by A10;
reconsider w1 = w as R_eal by A13;
A15: seq2 . k1 in Y2 by A8, A14;
w1 = r + (seq2 . k1) by A2, A13;
hence w in {r} + Y2 by A12, A15; ::_thesis: verum
end;
then A16: Y1 c= {r} + Y2 by TARSKI:def_3;
now__::_thesis:_for_w_being_set_st_w_in_{r}_+_Y2_holds_
w_in_Y1
let w be set ; ::_thesis: ( w in {r} + Y2 implies w in Y1 )
assume w in {r} + Y2 ; ::_thesis: w in Y1
then consider w1, w2 being R_eal such that
A17: w = w1 + w2 and
A18: w1 in {r} and
A19: w2 in Y2 ;
consider k2 being Element of NAT such that
A20: w2 = seq2 . k2 and
A21: n <= k2 by A8, A19;
w1 = r by A18, TARSKI:def_1;
then w = seq1 . k2 by A2, A17, A20;
hence w in Y1 by A10, A21; ::_thesis: verum
end;
then {r} + Y2 c= Y1 by TARSKI:def_3;
then Y1 = {r} + Y2 by A16, XBOOLE_0:def_10;
then inf Y1 = (inf {r}) + (inf Y2) by A1, Th9;
then inf Y1 = r + (inf Y2) by XXREAL_2:13;
then z = (inferior_realsequence seq1) . n by A4, A3, A9, A11, TARSKI:def_1;
hence z in R1 by FUNCT_2:4; ::_thesis: verum
end;
then A22: {r} + R2 c= R1 by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_{r}_+_P2_holds_
z_in_P1
let z be set ; ::_thesis: ( z in {r} + P2 implies z in P1 )
assume z in {r} + P2 ; ::_thesis: z in P1
then consider z2, z3 being R_eal such that
A23: z = z2 + z3 and
A24: z2 in {r} and
A25: z3 in P2 ;
consider n being set such that
A26: n in NAT and
A27: (superior_realsequence seq2) . n = z3 by A25, FUNCT_2:11;
reconsider n = n as Element of NAT by A26;
consider Y2 being non empty Subset of ExtREAL such that
A28: Y2 = { (seq2 . k) where k is Element of NAT : n <= k } and
A29: z3 = sup Y2 by A27, RINFSUP2:def_7;
consider Y1 being non empty Subset of ExtREAL such that
A30: Y1 = { (seq1 . k) where k is Element of NAT : n <= k } and
A31: (superior_realsequence seq1) . n = sup Y1 by RINFSUP2:def_7;
now__::_thesis:_for_w_being_set_st_w_in_Y1_holds_
w_in_{r}_+_Y2
let w be set ; ::_thesis: ( w in Y1 implies w in {r} + Y2 )
A32: r in {r} by TARSKI:def_1;
assume w in Y1 ; ::_thesis: w in {r} + Y2
then consider k1 being Element of NAT such that
A33: w = seq1 . k1 and
A34: n <= k1 by A30;
reconsider w1 = w as R_eal by A33;
A35: seq2 . k1 in Y2 by A28, A34;
w1 = r + (seq2 . k1) by A2, A33;
hence w in {r} + Y2 by A32, A35; ::_thesis: verum
end;
then A36: Y1 c= {r} + Y2 by TARSKI:def_3;
now__::_thesis:_for_w_being_set_st_w_in_{r}_+_Y2_holds_
w_in_Y1
let w be set ; ::_thesis: ( w in {r} + Y2 implies w in Y1 )
assume w in {r} + Y2 ; ::_thesis: w in Y1
then consider w1, w2 being R_eal such that
A37: w = w1 + w2 and
A38: w1 in {r} and
A39: w2 in Y2 ;
consider k2 being Element of NAT such that
A40: w2 = seq2 . k2 and
A41: n <= k2 by A28, A39;
w1 = r by A38, TARSKI:def_1;
then w = seq1 . k2 by A2, A37, A40;
hence w in Y1 by A30, A41; ::_thesis: verum
end;
then {r} + Y2 c= Y1 by TARSKI:def_3;
then Y1 = {r} + Y2 by A36, XBOOLE_0:def_10;
then sup Y1 = (sup {r}) + (sup Y2) by A1, Th8;
then sup Y1 = r + (sup Y2) by XXREAL_2:11;
then z = (superior_realsequence seq1) . n by A24, A23, A29, A31, TARSKI:def_1;
hence z in P1 by FUNCT_2:4; ::_thesis: verum
end;
then A42: {r} + P2 c= P1 by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_R1_holds_
z_in_{r}_+_R2
let z be set ; ::_thesis: ( z in R1 implies z in {r} + R2 )
assume z in R1 ; ::_thesis: z in {r} + R2
then consider n being set such that
A43: n in NAT and
A44: (inferior_realsequence seq1) . n = z by FUNCT_2:11;
reconsider n = n as Element of NAT by A43;
consider Y1 being non empty Subset of ExtREAL such that
A45: Y1 = { (seq1 . k) where k is Element of NAT : n <= k } and
A46: z = inf Y1 by A44, RINFSUP2:def_6;
consider Y2 being non empty Subset of ExtREAL such that
A47: Y2 = { (seq2 . k) where k is Element of NAT : n <= k } and
A48: (inferior_realsequence seq2) . n = inf Y2 by RINFSUP2:def_6;
now__::_thesis:_for_w_being_set_st_w_in_Y1_holds_
w_in_{r}_+_Y2
let w be set ; ::_thesis: ( w in Y1 implies w in {r} + Y2 )
A49: r in {r} by TARSKI:def_1;
assume w in Y1 ; ::_thesis: w in {r} + Y2
then consider k1 being Element of NAT such that
A50: w = seq1 . k1 and
A51: n <= k1 by A45;
reconsider w1 = w as R_eal by A50;
A52: seq2 . k1 in Y2 by A47, A51;
w1 = r + (seq2 . k1) by A2, A50;
hence w in {r} + Y2 by A49, A52; ::_thesis: verum
end;
then A53: Y1 c= {r} + Y2 by TARSKI:def_3;
now__::_thesis:_for_w_being_set_st_w_in_{r}_+_Y2_holds_
w_in_Y1
let w be set ; ::_thesis: ( w in {r} + Y2 implies w in Y1 )
assume w in {r} + Y2 ; ::_thesis: w in Y1
then consider w1, w2 being R_eal such that
A54: w = w1 + w2 and
A55: w1 in {r} and
A56: w2 in Y2 ;
consider k2 being Element of NAT such that
A57: w2 = seq2 . k2 and
A58: n <= k2 by A47, A56;
w1 = r by A55, TARSKI:def_1;
then w = seq1 . k2 by A2, A54, A57;
hence w in Y1 by A45, A58; ::_thesis: verum
end;
then {r} + Y2 c= Y1 by TARSKI:def_3;
then Y1 = {r} + Y2 by A53, XBOOLE_0:def_10;
then inf Y1 = (inf {r}) + (inf Y2) by A1, Th9;
then A59: inf Y1 = r + (inf Y2) by XXREAL_2:13;
A60: (inferior_realsequence seq2) . n in R2 by FUNCT_2:4;
r in {r} by TARSKI:def_1;
hence z in {r} + R2 by A46, A48, A59, A60; ::_thesis: verum
end;
then R1 c= {r} + R2 by TARSKI:def_3;
then R1 = {r} + R2 by A22, XBOOLE_0:def_10;
then sup R1 = (sup {r}) + (sup R2) by A1, Th8;
hence lim_inf seq1 = r + (lim_inf seq2) by XXREAL_2:11; ::_thesis: lim_sup seq1 = r + (lim_sup seq2)
now__::_thesis:_for_z_being_set_st_z_in_P1_holds_
z_in_{r}_+_P2
let z be set ; ::_thesis: ( z in P1 implies z in {r} + P2 )
assume z in P1 ; ::_thesis: z in {r} + P2
then consider n being set such that
A61: n in NAT and
A62: (superior_realsequence seq1) . n = z by FUNCT_2:11;
reconsider n = n as Element of NAT by A61;
consider Y1 being non empty Subset of ExtREAL such that
A63: Y1 = { (seq1 . k) where k is Element of NAT : n <= k } and
A64: z = sup Y1 by A62, RINFSUP2:def_7;
consider Y2 being non empty Subset of ExtREAL such that
A65: Y2 = { (seq2 . k) where k is Element of NAT : n <= k } and
A66: (superior_realsequence seq2) . n = sup Y2 by RINFSUP2:def_7;
now__::_thesis:_for_w_being_set_st_w_in_Y1_holds_
w_in_{r}_+_Y2
let w be set ; ::_thesis: ( w in Y1 implies w in {r} + Y2 )
A67: r in {r} by TARSKI:def_1;
assume w in Y1 ; ::_thesis: w in {r} + Y2
then consider k1 being Element of NAT such that
A68: w = seq1 . k1 and
A69: n <= k1 by A63;
reconsider w1 = w as R_eal by A68;
A70: seq2 . k1 in Y2 by A65, A69;
w1 = r + (seq2 . k1) by A2, A68;
hence w in {r} + Y2 by A67, A70; ::_thesis: verum
end;
then A71: Y1 c= {r} + Y2 by TARSKI:def_3;
now__::_thesis:_for_w_being_set_st_w_in_{r}_+_Y2_holds_
w_in_Y1
let w be set ; ::_thesis: ( w in {r} + Y2 implies w in Y1 )
assume w in {r} + Y2 ; ::_thesis: w in Y1
then consider w1, w2 being R_eal such that
A72: w = w1 + w2 and
A73: w1 in {r} and
A74: w2 in Y2 ;
consider k2 being Element of NAT such that
A75: w2 = seq2 . k2 and
A76: n <= k2 by A65, A74;
w1 = r by A73, TARSKI:def_1;
then w = seq1 . k2 by A2, A72, A75;
hence w in Y1 by A63, A76; ::_thesis: verum
end;
then {r} + Y2 c= Y1 by TARSKI:def_3;
then Y1 = {r} + Y2 by A71, XBOOLE_0:def_10;
then sup Y1 = (sup {r}) + (sup Y2) by A1, Th8;
then A77: sup Y1 = r + (sup Y2) by XXREAL_2:11;
A78: (superior_realsequence seq2) . n in P2 by FUNCT_2:4;
r in {r} by TARSKI:def_1;
hence z in {r} + P2 by A64, A66, A77, A78; ::_thesis: verum
end;
then P1 c= {r} + P2 by TARSKI:def_3;
then P1 = {r} + P2 by A42, XBOOLE_0:def_10;
then inf P1 = (inf {r}) + (inf P2) by A1, Th9;
hence lim_sup seq1 = r + (lim_sup seq2) by XXREAL_2:13; ::_thesis: verum
end;
theorem Th11: :: MESFUN10:11
for X being non empty set
for F1, F2 being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & f " {+infty} = {} & f " {-infty} = {} & ( for n being Nat holds F1 . n = f + (F2 . n) ) holds
( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) )
proof
let X be non empty set ; ::_thesis: for F1, F2 being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & f " {+infty} = {} & f " {-infty} = {} & ( for n being Nat holds F1 . n = f + (F2 . n) ) holds
( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) )
let F1, F2 be Functional_Sequence of X,ExtREAL; ::_thesis: for f being PartFunc of X,ExtREAL st dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & f " {+infty} = {} & f " {-infty} = {} & ( for n being Nat holds F1 . n = f + (F2 . n) ) holds
( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) )
let f be PartFunc of X,ExtREAL; ::_thesis: ( dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & f " {+infty} = {} & f " {-infty} = {} & ( for n being Nat holds F1 . n = f + (F2 . n) ) implies ( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) ) )
assume that
A1: dom (F1 . 0) = dom (F2 . 0) and
A2: F1 is with_the_same_dom and
A3: f " {+infty} = {} and
A4: f " {-infty} = {} and
A5: for n being Nat holds F1 . n = f + (F2 . n) ; ::_thesis: ( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) )
A6: F1 . 0 = f + (F2 . 0) by A5;
A7: dom (f + (F2 . 0)) = ((dom f) /\ (dom (F2 . 0))) \ (((f " {-infty}) /\ ((F2 . 0) " {+infty})) \/ ((f " {+infty}) /\ ((F2 . 0) " {-infty}))) by MESFUNC1:def_3;
A8: dom (f + (lim_sup F2)) = ((dom f) /\ (dom (lim_sup F2))) \ (((f " {-infty}) /\ ((lim_sup F2) " {+infty})) \/ ((f " {+infty}) /\ ((lim_sup F2) " {-infty}))) by MESFUNC1:def_3;
then A9: dom (f + (lim_sup F2)) = (dom f) /\ (dom (F2 . 0)) by A3, A4, MESFUNC8:def_8;
then A10: dom (lim_sup F1) = dom (f + (lim_sup F2)) by A3, A4, A6, A7, MESFUNC8:def_8;
A11: dom (f + (lim_inf F2)) = ((dom f) /\ (dom (lim_inf F2))) \ (((f " {-infty}) /\ ((lim_inf F2) " {+infty})) \/ ((f " {+infty}) /\ ((lim_inf F2) " {-infty}))) by MESFUNC1:def_3;
then A12: dom (f + (lim_inf F2)) = (dom f) /\ (dom (F2 . 0)) by A3, A4, MESFUNC8:def_7;
then A13: dom (lim_inf F1) = dom (f + (lim_inf F2)) by A3, A4, A6, A7, MESFUNC8:def_7;
A14: dom (lim_inf F2) = dom (F2 . 0) by MESFUNC8:def_7;
A15: dom (lim_inf F1) = dom (F1 . 0) by MESFUNC8:def_7;
for x being Element of X st x in dom (lim_inf F1) holds
(lim_inf F1) . x = (f + (lim_inf F2)) . x
proof
let x be Element of X; ::_thesis: ( x in dom (lim_inf F1) implies (lim_inf F1) . x = (f + (lim_inf F2)) . x )
assume A16: x in dom (lim_inf F1) ; ::_thesis: (lim_inf F1) . x = (f + (lim_inf F2)) . x
then A17: (lim_inf F1) . x = lim_inf (F1 # x) by MESFUNC8:def_7;
A18: for n being Nat holds (F1 # x) . n = (f . x) + ((F2 # x) . n)
proof
let n be Nat; ::_thesis: (F1 # x) . n = (f . x) + ((F2 # x) . n)
F1 . n = f + (F2 . n) by A5;
then dom (f + (F2 . n)) = dom (F1 . 0) by A2, MESFUNC8:def_2;
then A19: x in dom (f + (F2 . n)) by A16, MESFUNC8:def_7;
(F1 . n) . x = (f + (F2 . n)) . x by A5;
then (F1 . n) . x = (f . x) + ((F2 . n) . x) by A19, MESFUNC1:def_3;
then (F1 # x) . n = (f . x) + ((F2 . n) . x) by MESFUNC5:def_13;
hence (F1 # x) . n = (f . x) + ((F2 # x) . n) by MESFUNC5:def_13; ::_thesis: verum
end;
A20: dom (f + (lim_inf F2)) c= dom f by A3, A4, A11, XBOOLE_1:17;
then not f . x in {-infty} by A4, A13, A16, FUNCT_1:def_7;
then A21: f . x <> -infty by TARSKI:def_1;
not f . x in {+infty} by A3, A13, A16, A20, FUNCT_1:def_7;
then f . x <> +infty by TARSKI:def_1;
then A22: f . x is Real by A21, XXREAL_0:14;
x in dom (f + (lim_inf F2)) by A3, A4, A6, A7, A12, A16, MESFUNC8:def_7;
then A23: (f + (lim_inf F2)) . x = (f . x) + ((lim_inf F2) . x) by MESFUNC1:def_3;
(lim_inf F2) . x = lim_inf (F2 # x) by A1, A15, A14, A16, MESFUNC8:def_7;
hence (lim_inf F1) . x = (f + (lim_inf F2)) . x by A22, A18, A17, A23, Th10; ::_thesis: verum
end;
hence lim_inf F1 = f + (lim_inf F2) by A13, PARTFUN1:5; ::_thesis: lim_sup F1 = f + (lim_sup F2)
A24: dom (lim_sup F1) = dom (F1 . 0) by MESFUNC8:def_8;
A25: dom (lim_sup F2) = dom (F2 . 0) by MESFUNC8:def_8;
for x being Element of X st x in dom (lim_sup F1) holds
(lim_sup F1) . x = (f + (lim_sup F2)) . x
proof
let x be Element of X; ::_thesis: ( x in dom (lim_sup F1) implies (lim_sup F1) . x = (f + (lim_sup F2)) . x )
assume A26: x in dom (lim_sup F1) ; ::_thesis: (lim_sup F1) . x = (f + (lim_sup F2)) . x
then A27: (lim_sup F1) . x = lim_sup (F1 # x) by MESFUNC8:def_8;
A28: for n being Nat holds (F1 # x) . n = (f . x) + ((F2 # x) . n)
proof
let n be Nat; ::_thesis: (F1 # x) . n = (f . x) + ((F2 # x) . n)
F1 . n = f + (F2 . n) by A5;
then A29: dom (f + (F2 . n)) = dom (F1 . 0) by A2, MESFUNC8:def_2;
(F1 . n) . x = (f + (F2 . n)) . x by A5;
then (F1 . n) . x = (f . x) + ((F2 . n) . x) by A24, A26, A29, MESFUNC1:def_3;
then (F1 # x) . n = (f . x) + ((F2 . n) . x) by MESFUNC5:def_13;
hence (F1 # x) . n = (f . x) + ((F2 # x) . n) by MESFUNC5:def_13; ::_thesis: verum
end;
A30: dom (f + (lim_sup F2)) c= dom f by A3, A4, A8, XBOOLE_1:17;
then not f . x in {-infty} by A4, A10, A26, FUNCT_1:def_7;
then A31: f . x <> -infty by TARSKI:def_1;
not f . x in {+infty} by A3, A10, A26, A30, FUNCT_1:def_7;
then f . x <> +infty by TARSKI:def_1;
then A32: f . x is Real by A31, XXREAL_0:14;
x in dom (f + (lim_sup F2)) by A3, A4, A6, A7, A9, A26, MESFUNC8:def_8;
then A33: (f + (lim_sup F2)) . x = (f . x) + ((lim_sup F2) . x) by MESFUNC1:def_3;
(lim_sup F2) . x = lim_sup (F2 # x) by A1, A24, A25, A26, MESFUNC8:def_8;
hence (lim_sup F1) . x = (f + (lim_sup F2)) . x by A32, A28, A27, A33, Th10; ::_thesis: verum
end;
hence lim_sup F1 = f + (lim_sup F2) by A10, PARTFUN1:5; ::_thesis: verum
end;
theorem Th12: :: MESFUN10:12
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
f - g is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
f - g is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
f - g is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
f - g is_integrable_on M
let f, g be PartFunc of X,ExtREAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies f - g is_integrable_on M )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; ::_thesis: f - g is_integrable_on M
(- 1) (#) g is_integrable_on M by A2, MESFUNC5:110;
then - g is_integrable_on M by MESFUNC2:9;
then f + (- g) is_integrable_on M by A1, MESFUNC5:108;
hence f - g is_integrable_on M by MESFUNC2:8; ::_thesis: verum
end;
theorem Th13: :: MESFUN10:13
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )
let f, g be PartFunc of X,ExtREAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; ::_thesis: ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )
(- 1) (#) g is_integrable_on M by A2, MESFUNC5:110;
then - g is_integrable_on M by MESFUNC2:9;
then consider E being Element of S such that
A3: E = (dom f) /\ (dom (- g)) and
A4: Integral (M,(f + (- g))) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) by A1, MESFUNC5:109;
A5: dom g = dom (- g) by MESFUNC1:def_7;
Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) by A4, MESFUNC2:8;
hence ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) by A3, A5; ::_thesis: verum
end;
theorem Th14: :: MESFUN10:14
for seq1, seq2 being ExtREAL_sequence st ( for n being Nat holds seq1 . n = - (seq2 . n) ) holds
( lim_inf seq2 = - (lim_sup seq1) & lim_sup seq2 = - (lim_inf seq1) )
proof
let seq1, seq2 be ExtREAL_sequence; ::_thesis: ( ( for n being Nat holds seq1 . n = - (seq2 . n) ) implies ( lim_inf seq2 = - (lim_sup seq1) & lim_sup seq2 = - (lim_inf seq1) ) )
assume A1: for n being Nat holds seq1 . n = - (seq2 . n) ; ::_thesis: ( lim_inf seq2 = - (lim_sup seq1) & lim_sup seq2 = - (lim_inf seq1) )
now__::_thesis:_for_z_being_set_st_z_in_rng_(inferior_realsequence_seq2)_holds_
z_in_-_(rng_(superior_realsequence_seq1))
let z be set ; ::_thesis: ( z in rng (inferior_realsequence seq2) implies z in - (rng (superior_realsequence seq1)) )
assume z in rng (inferior_realsequence seq2) ; ::_thesis: z in - (rng (superior_realsequence seq1))
then consider n being set such that
A2: n in dom (inferior_realsequence seq2) and
A3: z = (inferior_realsequence seq2) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A2;
consider R2 being non empty Subset of ExtREAL such that
A4: R2 = { (seq2 . k) where k is Element of NAT : n <= k } and
A5: z = inf R2 by A3, RINFSUP2:def_6;
reconsider z2 = z as Element of ExtREAL by A3;
set R1 = { (seq1 . k) where k is Element of NAT : n <= k } ;
reconsider R1 = { (seq1 . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5;
set z1 = - z2;
A6: ex K1 being non empty Subset of ExtREAL st
( K1 = { (seq1 . k) where k is Element of NAT : n <= k } & (superior_realsequence seq1) . n = sup K1 ) by RINFSUP2:def_7;
now__::_thesis:_for_x_being_set_st_x_in_R1_holds_
x_in_-_R2
let x be set ; ::_thesis: ( x in R1 implies x in - R2 )
assume x in R1 ; ::_thesis: x in - R2
then consider k being Element of NAT such that
A7: x = seq1 . k and
A8: n <= k ;
reconsider x1 = x as Element of ExtREAL by A7;
- x1 = - (- (seq2 . k)) by A1, A7;
then - x1 in { (seq2 . k2) where k2 is Element of NAT : n <= k2 } by A8;
then - (- x1) in - R2 by A4;
hence x in - R2 ; ::_thesis: verum
end;
then A9: R1 c= - R2 by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_-_R2_holds_
x_in_R1
let x be set ; ::_thesis: ( x in - R2 implies x in R1 )
assume x in - R2 ; ::_thesis: x in R1
then consider y being R_eal such that
A10: x = - y and
A11: y in R2 ;
consider k being Element of NAT such that
A12: y = seq2 . k and
A13: n <= k by A4, A11;
seq1 . k = - (seq2 . k) by A1;
hence x in R1 by A10, A12, A13; ::_thesis: verum
end;
then - R2 c= R1 by TARSKI:def_3;
then - R2 = R1 by A9, XBOOLE_0:def_10;
then (superior_realsequence seq1) . n = - z2 by A5, A6, SUPINF_2:15;
then A14: - z2 in rng (superior_realsequence seq1) by FUNCT_2:4;
z2 = - (- z2) ;
hence z in - (rng (superior_realsequence seq1)) by A14; ::_thesis: verum
end;
then A15: rng (inferior_realsequence seq2) c= - (rng (superior_realsequence seq1)) by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_rng_(superior_realsequence_seq2)_holds_
z_in_-_(rng_(inferior_realsequence_seq1))
let z be set ; ::_thesis: ( z in rng (superior_realsequence seq2) implies z in - (rng (inferior_realsequence seq1)) )
assume z in rng (superior_realsequence seq2) ; ::_thesis: z in - (rng (inferior_realsequence seq1))
then consider n being set such that
A16: n in dom (superior_realsequence seq2) and
A17: z = (superior_realsequence seq2) . n by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A16;
consider R2 being non empty Subset of ExtREAL such that
A18: R2 = { (seq2 . k) where k is Element of NAT : n <= k } and
A19: z = sup R2 by A17, RINFSUP2:def_7;
reconsider z2 = z as Element of ExtREAL by A17;
set R1 = { (seq1 . k) where k is Element of NAT : n <= k } ;
reconsider R1 = { (seq1 . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5;
set z1 = - z2;
A20: ex K1 being non empty Subset of ExtREAL st
( K1 = { (seq1 . k) where k is Element of NAT : n <= k } & (inferior_realsequence seq1) . n = inf K1 ) by RINFSUP2:def_6;
now__::_thesis:_for_x_being_set_st_x_in_R1_holds_
x_in_-_R2
let x be set ; ::_thesis: ( x in R1 implies x in - R2 )
assume x in R1 ; ::_thesis: x in - R2
then consider k being Element of NAT such that
A21: x = seq1 . k and
A22: n <= k ;
reconsider x1 = x as Element of ExtREAL by A21;
- x1 = - (- (seq2 . k)) by A1, A21;
then - x1 in { (seq2 . k2) where k2 is Element of NAT : n <= k2 } by A22;
then - (- x1) in - R2 by A18;
hence x in - R2 ; ::_thesis: verum
end;
then A23: R1 c= - R2 by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_-_R2_holds_
x_in_R1
let x be set ; ::_thesis: ( x in - R2 implies x in R1 )
assume x in - R2 ; ::_thesis: x in R1
then consider y being R_eal such that
A24: x = - y and
A25: y in R2 ;
consider k being Element of NAT such that
A26: y = seq2 . k and
A27: n <= k by A18, A25;
seq1 . k = - (seq2 . k) by A1;
hence x in R1 by A24, A26, A27; ::_thesis: verum
end;
then - R2 c= R1 by TARSKI:def_3;
then - R2 = R1 by A23, XBOOLE_0:def_10;
then (inferior_realsequence seq1) . n = - z2 by A19, A20, SUPINF_2:14;
then A28: - z2 in rng (inferior_realsequence seq1) by FUNCT_2:4;
z2 = - (- z2) ;
hence z in - (rng (inferior_realsequence seq1)) by A28; ::_thesis: verum
end;
then A29: rng (superior_realsequence seq2) c= - (rng (inferior_realsequence seq1)) by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_-_(rng_(superior_realsequence_seq1))_holds_
z_in_rng_(inferior_realsequence_seq2)
let z be set ; ::_thesis: ( z in - (rng (superior_realsequence seq1)) implies z in rng (inferior_realsequence seq2) )
assume z in - (rng (superior_realsequence seq1)) ; ::_thesis: z in rng (inferior_realsequence seq2)
then consider t being R_eal such that
A30: z = - t and
A31: t in rng (superior_realsequence seq1) ;
consider n being set such that
A32: n in dom (superior_realsequence seq1) and
A33: t = (superior_realsequence seq1) . n by A31, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A32;
consider R1 being non empty Subset of ExtREAL such that
A34: R1 = { (seq1 . k) where k is Element of NAT : n <= k } and
A35: t = sup R1 by A33, RINFSUP2:def_7;
reconsider z1 = z as Element of ExtREAL by A30;
set R2 = { (seq2 . k) where k is Element of NAT : n <= k } ;
reconsider R2 = { (seq2 . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5;
A36: ex K2 being non empty Subset of ExtREAL st
( K2 = { (seq2 . k) where k is Element of NAT : n <= k } & (inferior_realsequence seq2) . n = inf K2 ) by RINFSUP2:def_6;
now__::_thesis:_for_x_being_set_st_x_in_R2_holds_
x_in_-_R1
let x be set ; ::_thesis: ( x in R2 implies x in - R1 )
assume x in R2 ; ::_thesis: x in - R1
then consider k being Element of NAT such that
A37: x = seq2 . k and
A38: n <= k ;
reconsider x1 = x as Element of ExtREAL by A37;
- x1 = - (- (seq1 . k)) by A1, A37;
then - x1 in { (seq1 . k2) where k2 is Element of NAT : n <= k2 } by A38;
then - (- x1) in - R1 by A34;
hence x in - R1 ; ::_thesis: verum
end;
then A39: R2 c= - R1 by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_-_R1_holds_
x_in_R2
let x be set ; ::_thesis: ( x in - R1 implies x in R2 )
assume x in - R1 ; ::_thesis: x in R2
then consider y being R_eal such that
A40: x = - y and
A41: y in R1 ;
consider k being Element of NAT such that
A42: y = seq1 . k and
A43: n <= k by A34, A41;
seq1 . k = - (seq2 . k) by A1;
hence x in R2 by A40, A42, A43; ::_thesis: verum
end;
then - R1 c= R2 by TARSKI:def_3;
then - R1 = R2 by A39, XBOOLE_0:def_10;
then (inferior_realsequence seq2) . n = z1 by A30, A35, A36, SUPINF_2:14;
hence z in rng (inferior_realsequence seq2) by FUNCT_2:4; ::_thesis: verum
end;
then - (rng (superior_realsequence seq1)) c= rng (inferior_realsequence seq2) by TARSKI:def_3;
then rng (inferior_realsequence seq2) = - (rng (superior_realsequence seq1)) by A15, XBOOLE_0:def_10;
hence lim_inf seq2 = - (lim_sup seq1) by SUPINF_2:15; ::_thesis: lim_sup seq2 = - (lim_inf seq1)
now__::_thesis:_for_z_being_set_st_z_in_-_(rng_(inferior_realsequence_seq1))_holds_
z_in_rng_(superior_realsequence_seq2)
let z be set ; ::_thesis: ( z in - (rng (inferior_realsequence seq1)) implies z in rng (superior_realsequence seq2) )
assume z in - (rng (inferior_realsequence seq1)) ; ::_thesis: z in rng (superior_realsequence seq2)
then consider t being R_eal such that
A44: z = - t and
A45: t in rng (inferior_realsequence seq1) ;
consider n being set such that
A46: n in dom (inferior_realsequence seq1) and
A47: t = (inferior_realsequence seq1) . n by A45, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A46;
consider R1 being non empty Subset of ExtREAL such that
A48: R1 = { (seq1 . k) where k is Element of NAT : n <= k } and
A49: t = inf R1 by A47, RINFSUP2:def_6;
reconsider z1 = z as Element of ExtREAL by A44;
set R2 = { (seq2 . k) where k is Element of NAT : n <= k } ;
reconsider R2 = { (seq2 . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5;
A50: ex K2 being non empty Subset of ExtREAL st
( K2 = { (seq2 . k) where k is Element of NAT : n <= k } & (superior_realsequence seq2) . n = sup K2 ) by RINFSUP2:def_7;
now__::_thesis:_for_x_being_set_st_x_in_R2_holds_
x_in_-_R1
let x be set ; ::_thesis: ( x in R2 implies x in - R1 )
assume x in R2 ; ::_thesis: x in - R1
then consider k being Element of NAT such that
A51: x = seq2 . k and
A52: n <= k ;
reconsider x1 = x as Element of ExtREAL by A51;
seq1 . k = - (seq2 . k) by A1;
then - x1 in R1 by A48, A51, A52;
then - (- x1) in - R1 ;
hence x in - R1 ; ::_thesis: verum
end;
then A53: R2 c= - R1 by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_-_R1_holds_
x_in_R2
let x be set ; ::_thesis: ( x in - R1 implies x in R2 )
assume x in - R1 ; ::_thesis: x in R2
then consider y being R_eal such that
A54: x = - y and
A55: y in R1 ;
consider k being Element of NAT such that
A56: y = seq1 . k and
A57: n <= k by A48, A55;
seq1 . k = - (seq2 . k) by A1;
hence x in R2 by A54, A56, A57; ::_thesis: verum
end;
then - R1 c= R2 by TARSKI:def_3;
then - R1 = R2 by A53, XBOOLE_0:def_10;
then (superior_realsequence seq2) . n = z1 by A44, A49, A50, SUPINF_2:15;
hence z in rng (superior_realsequence seq2) by FUNCT_2:4; ::_thesis: verum
end;
then - (rng (inferior_realsequence seq1)) c= rng (superior_realsequence seq2) by TARSKI:def_3;
then rng (superior_realsequence seq2) = - (rng (inferior_realsequence seq1)) by A29, XBOOLE_0:def_10;
hence lim_sup seq2 = - (lim_inf seq1) by SUPINF_2:14; ::_thesis: verum
end;
theorem Th15: :: MESFUN10:15
for X being non empty set
for F1, F2 being Functional_Sequence of X,ExtREAL st dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & ( for n being Nat holds F1 . n = - (F2 . n) ) holds
( lim_inf F1 = - (lim_sup F2) & lim_sup F1 = - (lim_inf F2) )
proof
let X be non empty set ; ::_thesis: for F1, F2 being Functional_Sequence of X,ExtREAL st dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & ( for n being Nat holds F1 . n = - (F2 . n) ) holds
( lim_inf F1 = - (lim_sup F2) & lim_sup F1 = - (lim_inf F2) )
let F1, F2 be Functional_Sequence of X,ExtREAL; ::_thesis: ( dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & ( for n being Nat holds F1 . n = - (F2 . n) ) implies ( lim_inf F1 = - (lim_sup F2) & lim_sup F1 = - (lim_inf F2) ) )
assume that
A1: dom (F1 . 0) = dom (F2 . 0) and
A2: F1 is with_the_same_dom and
A3: for n being Nat holds F1 . n = - (F2 . n) ; ::_thesis: ( lim_inf F1 = - (lim_sup F2) & lim_sup F1 = - (lim_inf F2) )
A4: dom (lim_inf F1) = dom (F1 . 0) by MESFUNC8:def_7;
A5: dom (lim_sup F2) = dom (F2 . 0) by MESFUNC8:def_8;
A6: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(F1_._0)_holds_
for_n_being_Nat_holds_(F2_#_x)_._n_=_-_((F1_#_x)_._n)
let x be Element of X; ::_thesis: ( x in dom (F1 . 0) implies for n being Nat holds (F2 # x) . n = - ((F1 # x) . n) )
assume A7: x in dom (F1 . 0) ; ::_thesis: for n being Nat holds (F2 # x) . n = - ((F1 # x) . n)
let n be Nat; ::_thesis: (F2 # x) . n = - ((F1 # x) . n)
dom (F1 . n) = dom (F1 . 0) by A2, MESFUNC8:def_2;
then A8: x in dom (- (F2 . n)) by A3, A7;
(F1 . n) . x = (- (F2 . n)) . x by A3;
then (F1 . n) . x = - ((F2 . n) . x) by A8, MESFUNC1:def_7;
then (F1 # x) . n = - ((F2 . n) . x) by MESFUNC5:def_13;
hence (F2 # x) . n = - ((F1 # x) . n) by MESFUNC5:def_13; ::_thesis: verum
end;
A9: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_inf_F1)_holds_
(lim_inf_F1)_._x_=_(-_(lim_sup_F2))_._x
let x be Element of X; ::_thesis: ( x in dom (lim_inf F1) implies (lim_inf F1) . x = (- (lim_sup F2)) . x )
assume A10: x in dom (lim_inf F1) ; ::_thesis: (lim_inf F1) . x = (- (lim_sup F2)) . x
then A11: (lim_inf F1) . x = lim_inf (F1 # x) by MESFUNC8:def_7;
x in dom (- (lim_sup F2)) by A1, A4, A5, A10, MESFUNC1:def_7;
then A12: (- (lim_sup F2)) . x = - ((lim_sup F2) . x) by MESFUNC1:def_7;
A13: for n being Nat holds (F2 # x) . n = - ((F1 # x) . n) by A4, A6, A10;
(lim_sup F2) . x = lim_sup (F2 # x) by A1, A4, A5, A10, MESFUNC8:def_8;
hence (lim_inf F1) . x = (- (lim_sup F2)) . x by A13, A11, A12, Th14; ::_thesis: verum
end;
dom (- (lim_sup F2)) = dom (lim_sup F2) by MESFUNC1:def_7;
hence lim_inf F1 = - (lim_sup F2) by A1, A4, A5, A9, PARTFUN1:5; ::_thesis: lim_sup F1 = - (lim_inf F2)
A14: dom (lim_sup F1) = dom (F1 . 0) by MESFUNC8:def_8;
A15: dom (lim_inf F2) = dom (F2 . 0) by MESFUNC8:def_7;
A16: for x being Element of X st x in dom (lim_sup F1) holds
(lim_sup F1) . x = (- (lim_inf F2)) . x
proof
let x be Element of X; ::_thesis: ( x in dom (lim_sup F1) implies (lim_sup F1) . x = (- (lim_inf F2)) . x )
assume A17: x in dom (lim_sup F1) ; ::_thesis: (lim_sup F1) . x = (- (lim_inf F2)) . x
then A18: (lim_sup F1) . x = lim_sup (F1 # x) by MESFUNC8:def_8;
x in dom (- (lim_inf F2)) by A1, A14, A15, A17, MESFUNC1:def_7;
then A19: (- (lim_inf F2)) . x = - ((lim_inf F2) . x) by MESFUNC1:def_7;
A20: for n being Nat holds (F2 # x) . n = - ((F1 # x) . n) by A14, A6, A17;
(lim_inf F2) . x = lim_inf (F2 # x) by A1, A14, A15, A17, MESFUNC8:def_7;
hence (lim_sup F1) . x = (- (lim_inf F2)) . x by A20, A18, A19, Th14; ::_thesis: verum
end;
dom (- (lim_inf F2)) = dom (lim_inf F2) by MESFUNC1:def_7;
hence lim_sup F1 = - (lim_inf F2) by A1, A14, A15, A16, PARTFUN1:5; ::_thesis: verum
end;
theorem Th16: :: MESFUN10:16
for X being non empty set
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 P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )
proof
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 P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )
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 P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )
let M be sigma_Measure of S; ::_thesis: for E being Element of S
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )
let E be Element of S; ::_thesis: for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )
let P be PartFunc of X,ExtREAL; ::_thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) implies ( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M ) )
assume that
A1: E = dom (F . 0) and
A2: E = dom P and
A3: for n being Nat holds F . n is_measurable_on E and
A4: P is_integrable_on M and
A5: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ; ::_thesis: ( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )
A6: lim_inf F is_measurable_on E by A1, A3, MESFUNC8:24;
hereby ::_thesis: ( |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M )
let n be Nat; ::_thesis: |.(F . n).| is_integrable_on M
A7: F . n is_measurable_on E by A3;
A8: E = dom (F . n) by A1, MESFUNC8:def_2;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(F_._n)_holds_
|.((F_._n)_._x).|_<=_P_._x
let x be Element of X; ::_thesis: ( x in dom (F . n) implies |.((F . n) . x).| <= P . x )
assume A9: x in dom (F . n) ; ::_thesis: |.((F . n) . x).| <= P . x
then A10: x in dom |.(F . n).| by MESFUNC1:def_10;
|.(F . n).| . x <= P . x by A5, A8, A9;
hence |.((F . n) . x).| <= P . x by A10, MESFUNC1:def_10; ::_thesis: verum
end;
then F . n is_integrable_on M by A2, A4, A8, A7, MESFUNC5:102;
hence |.(F . n).| is_integrable_on M by A8, A7, MESFUNC5:100; ::_thesis: verum
end;
A11: E = dom (lim_inf F) by A1, MESFUNC8:def_7;
A12: lim_sup F is_measurable_on E by A1, A3, MESFUNC8:23;
A13: for x being Element of X
for k being Nat st x in E holds
( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )
proof
let x be Element of X; ::_thesis: for k being Nat st x in E holds
( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )
let k be Nat; ::_thesis: ( x in E implies ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) )
assume A14: x in E ; ::_thesis: ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )
then x in dom (F . k) by A1, MESFUNC8:def_2;
then A15: x in dom |.(F . k).| by MESFUNC1:def_10;
|.(F . k).| . x <= P . x by A5, A14;
then A16: |.((F . k) . x).| <= P . x by A15, MESFUNC1:def_10;
then A17: (F . k) . x <= P . x by EXTREAL2:12;
- (P . x) <= (F . k) . x by A16, EXTREAL2:12;
hence ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) by A17, MESFUNC5:def_13; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_inf_F)_holds_
|.((lim_inf_F)_._x).|_<=_P_._x
let x be Element of X; ::_thesis: ( x in dom (lim_inf F) implies |.((lim_inf F) . x).| <= P . x )
assume A18: x in dom (lim_inf F) ; ::_thesis: |.((lim_inf F) . x).| <= P . x
then A19: x in E by A1, MESFUNC8:def_7;
for k being Nat holds (inferior_realsequence (F # x)) . k <= P . x
proof
let k be Nat; ::_thesis: (inferior_realsequence (F # x)) . k <= P . x
reconsider k1 = k as Element of NAT by ORDINAL1:def_12;
A20: (inferior_realsequence (F # x)) . k1 <= (F # x) . k1 by RINFSUP2:8;
(F # x) . k <= P . x by A13, A19;
hence (inferior_realsequence (F # x)) . k <= P . x by A20, XXREAL_0:2; ::_thesis: verum
end;
then lim_inf (F # x) <= P . x by Th5;
then A21: (lim_inf F) . x <= P . x by A18, MESFUNC8:def_7;
now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(F_#_x)_holds_
-_(P_._x)_<=_y
let y be ext-real number ; ::_thesis: ( y in rng (F # x) implies - (P . x) <= y )
assume y in rng (F # x) ; ::_thesis: - (P . x) <= y
then ex k being set st
( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def_3;
hence - (P . x) <= y by A13, A19; ::_thesis: verum
end;
then - (P . x) is LowerBound of rng (F # x) by XXREAL_2:def_2;
then - (P . x) <= inf (F # x) by XXREAL_2:def_4;
then - (P . x) <= inf ((F # x) ^\ 0) by NAT_1:47;
then A22: - (P . x) <= (inferior_realsequence (F # x)) . 0 by RINFSUP2:27;
(inferior_realsequence (F # x)) . 0 <= sup (inferior_realsequence (F # x)) by RINFSUP2:23;
then - (P . x) <= lim_inf (F # x) by A22, XXREAL_0:2;
then - (P . x) <= (lim_inf F) . x by A18, MESFUNC8:def_7;
hence |.((lim_inf F) . x).| <= P . x by A21, EXTREAL2:12; ::_thesis: verum
end;
then lim_inf F is_integrable_on M by A2, A4, A11, A6, MESFUNC5:102;
hence |.(lim_inf F).| is_integrable_on M by A11, A6, MESFUNC5:100; ::_thesis: |.(lim_sup F).| is_integrable_on M
A23: E = dom (lim_sup F) by A1, MESFUNC8:def_8;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_sup_F)_holds_
|.((lim_sup_F)_._x).|_<=_P_._x
let x be Element of X; ::_thesis: ( x in dom (lim_sup F) implies |.((lim_sup F) . x).| <= P . x )
assume A24: x in dom (lim_sup F) ; ::_thesis: |.((lim_sup F) . x).| <= P . x
for k being Nat holds (superior_realsequence (F # x)) . k >= - (P . x)
proof
let k be Nat; ::_thesis: (superior_realsequence (F # x)) . k >= - (P . x)
reconsider k1 = k as Element of NAT by ORDINAL1:def_12;
A25: (superior_realsequence (F # x)) . k1 >= (F # x) . k1 by RINFSUP2:8;
(F # x) . k >= - (P . x) by A23, A13, A24;
hence (superior_realsequence (F # x)) . k >= - (P . x) by A25, XXREAL_0:2; ::_thesis: verum
end;
then lim_sup (F # x) >= - (P . x) by Th4;
then A26: (lim_sup F) . x >= - (P . x) by A24, MESFUNC8:def_8;
now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(F_#_x)_holds_
P_._x_>=_y
let y be ext-real number ; ::_thesis: ( y in rng (F # x) implies P . x >= y )
assume y in rng (F # x) ; ::_thesis: P . x >= y
then ex k being set st
( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def_3;
hence P . x >= y by A23, A13, A24; ::_thesis: verum
end;
then P . x is UpperBound of rng (F # x) by XXREAL_2:def_1;
then P . x >= sup (rng (F # x)) by XXREAL_2:def_3;
then P . x >= sup ((F # x) ^\ 0) by NAT_1:47;
then A27: P . x >= (superior_realsequence (F # x)) . 0 by RINFSUP2:27;
(superior_realsequence (F # x)) . 0 >= inf (superior_realsequence (F # x)) by RINFSUP2:23;
then P . x >= lim_sup (F # x) by A27, XXREAL_0:2;
then P . x >= (lim_sup F) . x by A24, MESFUNC8:def_8;
hence |.((lim_sup F) . x).| <= P . x by A26, EXTREAL2:12; ::_thesis: verum
end;
then lim_sup F is_integrable_on M by A2, A4, A23, A12, MESFUNC5:102;
hence |.(lim_sup F).| is_integrable_on M by A23, A12, MESFUNC5:100; ::_thesis: verum
end;
Lm1: for X being non empty set
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 P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
proof
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 P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim 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 P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let M be sigma_Measure of S; ::_thesis: for E being Element of S
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let E be Element of S; ::_thesis: for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let P be PartFunc of X,ExtREAL; ::_thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} implies ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) )
assume that
A1: E = dom (F . 0) and
A2: E = dom P and
A3: for n being Nat holds F . n is_measurable_on E and
A4: P is_integrable_on M and
A5: P is nonnegative and
A6: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x and
A7: eq_dom (P,+infty) = {} ; ::_thesis: ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
A8: E = dom (lim_inf F) by A1, MESFUNC8:def_7;
then A9: (lim_inf F) | E = lim_inf F by RELAT_1:68;
deffunc H1( Element of NAT ) -> Element of K6(K7(X,ExtREAL)) = P + (F . $1);
consider G being Function such that
A10: ( dom G = NAT & ( for n being Element of NAT holds G . n = H1(n) ) ) from FUNCT_1:sch_4();
A11: for x being Element of X
for k being Nat st x in E holds
( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )
proof
let x be Element of X; ::_thesis: for k being Nat st x in E holds
( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )
let k be Nat; ::_thesis: ( x in E implies ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) )
assume A12: x in E ; ::_thesis: ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x )
then x in dom (F . k) by A1, MESFUNC8:def_2;
then A13: x in dom |.(F . k).| by MESFUNC1:def_10;
|.(F . k).| . x <= P . x by A6, A12;
then A14: |.((F . k) . x).| <= P . x by A13, MESFUNC1:def_10;
then A15: (F . k) . x <= P . x by EXTREAL2:12;
- (P . x) <= (F . k) . x by A14, EXTREAL2:12;
hence ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) by A15, MESFUNC5:def_13; ::_thesis: verum
end;
A16: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_inf_F)_holds_
|.((lim_inf_F)_._x).|_<=_P_._x
let x be Element of X; ::_thesis: ( x in dom (lim_inf F) implies |.((lim_inf F) . x).| <= P . x )
assume A17: x in dom (lim_inf F) ; ::_thesis: |.((lim_inf F) . x).| <= P . x
now__::_thesis:_for_k_being_Nat_holds_(inferior_realsequence_(F_#_x))_._k_<=_P_._x
let k be Nat; ::_thesis: (inferior_realsequence (F # x)) . k <= P . x
k is Element of NAT by ORDINAL1:def_12;
then A18: (inferior_realsequence (F # x)) . k <= (F # x) . k by RINFSUP2:8;
(F # x) . k <= P . x by A8, A11, A17;
hence (inferior_realsequence (F # x)) . k <= P . x by A18, XXREAL_0:2; ::_thesis: verum
end;
then lim_inf (F # x) <= P . x by Th5;
then A19: (lim_inf F) . x <= P . x by A17, MESFUNC8:def_7;
now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(F_#_x)_holds_
-_(P_._x)_<=_y
let y be ext-real number ; ::_thesis: ( y in rng (F # x) implies - (P . x) <= y )
assume y in rng (F # x) ; ::_thesis: - (P . x) <= y
then ex k being set st
( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def_3;
hence - (P . x) <= y by A8, A11, A17; ::_thesis: verum
end;
then - (P . x) is LowerBound of rng (F # x) by XXREAL_2:def_2;
then - (P . x) <= inf (rng (F # x)) by XXREAL_2:def_4;
then - (P . x) <= inf ((F # x) ^\ 0) by NAT_1:47;
then A20: - (P . x) <= (inferior_realsequence (F # x)) . 0 by RINFSUP2:27;
(inferior_realsequence (F # x)) . 0 <= sup (inferior_realsequence (F # x)) by RINFSUP2:23;
then - (P . x) <= lim_inf (F # x) by A20, XXREAL_0:2;
then - (P . x) <= (lim_inf F) . x by A17, MESFUNC8:def_7;
hence |.((lim_inf F) . x).| <= P . x by A19, EXTREAL2:12; ::_thesis: verum
end;
lim_inf F is_measurable_on E by A1, A3, MESFUNC8:24;
then lim_inf F is_integrable_on M by A2, A4, A8, A16, MESFUNC5:102;
then A21: ex E3 being Element of S st
( E3 = (dom P) /\ (dom (lim_inf F)) & Integral (M,(P + (lim_inf F))) = (Integral (M,(P | E3))) + (Integral (M,((lim_inf F) | E3))) ) by A4, MESFUNC5:109;
A22: P | E = P by A2, RELAT_1:68;
A23: Integral (M,P) < +infty by A4, MESFUNC5:96;
-infty < Integral (M,P) by A4, MESFUNC5:96;
then A24: Integral (M,P) is Real by A23, XXREAL_0:14;
now__::_thesis:_for_x_being_set_holds_not_x_in_P_"_{-infty}
let x be set ; ::_thesis: not x in P " {-infty}
assume x in P " {-infty} ; ::_thesis: contradiction
then A25: P . x in {-infty} by FUNCT_1:def_7;
0 <= P . x by A5, SUPINF_2:51;
hence contradiction by A25, TARSKI:def_1; ::_thesis: verum
end;
then A26: P " {-infty} = {} by XBOOLE_0:def_1;
A27: now__::_thesis:_for_n_being_Element_of_NAT_holds_G_._n_is_PartFunc_of_X,ExtREAL
let n be Element of NAT ; ::_thesis: G . n is PartFunc of X,ExtREAL
G . n = P + (F . n) by A10;
hence G . n is PartFunc of X,ExtREAL ; ::_thesis: verum
end;
A28: now__::_thesis:_for_n_being_Nat_holds_G_._n_=_P_+_(F_._n)
let n be Nat; ::_thesis: G . n = P + (F . n)
n is Element of NAT by ORDINAL1:def_12;
hence G . n = P + (F . n) by A10; ::_thesis: verum
end;
reconsider G = G as Functional_Sequence of X,ExtREAL by A10, A27, SEQFUNC:1;
A29: P " {+infty} = {} by A7, MESFUNC5:30;
A30: for n being Nat holds dom (G . n) = E
proof
let n be Nat; ::_thesis: dom (G . n) = E
dom (G . n) = dom (P + (F . n)) by A28;
then A31: dom (G . n) = ((dom P) /\ (dom (F . n))) \ (((P " {-infty}) /\ ((F . n) " {+infty})) \/ ((P " {+infty}) /\ ((F . n) " {-infty}))) by MESFUNC1:def_3;
dom (F . n) = E by A1, MESFUNC8:def_2;
hence dom (G . n) = E by A2, A29, A26, A31; ::_thesis: verum
end;
A32: now__::_thesis:_for_n,_m_being_Nat_holds_dom_(G_._n)_=_dom_(G_._m)
let n, m be Nat; ::_thesis: dom (G . n) = dom (G . m)
thus dom (G . n) = E by A30
.= dom (G . m) by A30 ; ::_thesis: verum
end;
deffunc H2( Element of NAT ) -> Element of K6(K7(X,ExtREAL)) = P - (F . $1);
consider H being Function such that
A33: ( dom H = NAT & ( for n being Element of NAT holds H . n = H2(n) ) ) from FUNCT_1:sch_4();
reconsider G = G as with_the_same_dom Functional_Sequence of X,ExtREAL by A32, MESFUNC8:def_2;
A34: dom (G . 0) = dom (F . 0) by A1, A30;
A35: for n being Nat holds F . n is_integrable_on M
proof
let n be Nat; ::_thesis: F . n is_integrable_on M
A36: E = dom (F . n) by A1, MESFUNC8:def_2;
A37: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(F_._n)_holds_
|.((F_._n)_._x).|_<=_P_._x
let x be Element of X; ::_thesis: ( x in dom (F . n) implies |.((F . n) . x).| <= P . x )
assume A38: x in dom (F . n) ; ::_thesis: |.((F . n) . x).| <= P . x
then A39: x in dom |.(F . n).| by MESFUNC1:def_10;
|.(F . n).| . x <= P . x by A6, A36, A38;
hence |.((F . n) . x).| <= P . x by A39, MESFUNC1:def_10; ::_thesis: verum
end;
F . n is_measurable_on E by A3;
hence F . n is_integrable_on M by A2, A4, A36, A37, MESFUNC5:102; ::_thesis: verum
end;
A40: now__::_thesis:_for_n_being_Nat_holds_
(_G_._n_is_nonnegative_&_G_._n_is_measurable_on_E_)
let n be Nat; ::_thesis: ( G . n is nonnegative & G . n is_measurable_on E )
A41: G . n = P + (F . n) by A28;
now__::_thesis:_for_x_being_set_st_x_in_dom_(P_+_(F_._n))_holds_
0_<=_(P_+_(F_._n))_._x
let x be set ; ::_thesis: ( x in dom (P + (F . n)) implies 0 <= (P + (F . n)) . x )
assume A42: x in dom (P + (F . n)) ; ::_thesis: 0 <= (P + (F . n)) . x
then reconsider x1 = x as Element of X ;
x in E by A30, A41, A42;
then - (P . x) <= (F # x1) . n by A11;
then A43: - (P . x) <= (F . n) . x by MESFUNC5:def_13;
(- (P . x)) + (P . x) = 0 by XXREAL_3:7;
then 0 <= ((F . n) . x) + (P . x) by A43, XXREAL_3:36;
hence 0 <= (P + (F . n)) . x by A42, MESFUNC1:def_3; ::_thesis: verum
end;
hence G . n is nonnegative by A41, SUPINF_2:52; ::_thesis: G . n is_measurable_on E
F . n is_integrable_on M by A35;
then G . n is_integrable_on M by A4, A41, MESFUNC5:108;
then ex E1 being Element of S st
( E1 = dom (G . n) & G . n is_measurable_on E1 ) by MESFUNC5:def_17;
hence G . n is_measurable_on E by A30; ::_thesis: verum
end;
E = dom (G . 0) by A30;
then consider IG being ExtREAL_sequence such that
A44: for n being Nat holds IG . n = Integral (M,(G . n)) and
A45: Integral (M,(lim_inf G)) <= lim_inf IG by A40, Th7;
A46: Integral (M,P) < +infty by A4, MESFUNC5:96;
deffunc H3( Element of NAT ) -> Element of ExtREAL = Integral (M,(F . $1));
consider I being Function of NAT,ExtREAL such that
A47: for n being Element of NAT holds I . n = H3(n) from FUNCT_2:sch_4();
reconsider I = I as ExtREAL_sequence ;
A48: -infty < Integral (M,P) by A4, MESFUNC5:96;
A49: for n being Nat holds
( I . n = Integral (M,(F . n)) & I . n is Real )
proof
let n be Nat; ::_thesis: ( I . n = Integral (M,(F . n)) & I . n is Real )
n is Element of NAT by ORDINAL1:def_12;
then A50: I . n = Integral (M,(F . n)) by A47;
A51: F . n is_integrable_on M by A35;
then A52: Integral (M,(F . n)) < +infty by MESFUNC5:96;
-infty < Integral (M,(F . n)) by A51, MESFUNC5:96;
hence ( I . n = Integral (M,(F . n)) & I . n is Real ) by A50, A52, XXREAL_0:14; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Nat_holds_IG_._n_=_(Integral_(M,P))_+_(I_._n)
let n be Nat; ::_thesis: IG . n = (Integral (M,P)) + (I . n)
A53: G . n = P + (F . n) by A28;
F . n is_integrable_on M by A35;
then A54: ex E2 being Element of S st
( E2 = (dom P) /\ (dom (F . n)) & Integral (M,(G . n)) = (Integral (M,(P | E2))) + (Integral (M,((F . n) | E2))) ) by A4, A53, MESFUNC5:109;
A55: P | E = P by A2, RELAT_1:68;
A56: dom (F . n) = E by A1, MESFUNC8:def_2;
then (F . n) | E = F . n by RELAT_1:68;
then Integral (M,(G . n)) = (Integral (M,P)) + (I . n) by A2, A49, A54, A56, A55;
hence IG . n = (Integral (M,P)) + (I . n) by A44; ::_thesis: verum
end;
then lim_inf IG = (Integral (M,P)) + (lim_inf I) by A24, Th10;
then (Integral (M,P)) + (Integral (M,(lim_inf F))) <= (Integral (M,P)) + (lim_inf I) by A2, A8, A28, A29, A26, A45, A21, A22, A9, A34, Th11;
then Integral (M,(lim_inf F)) <= ((lim_inf I) + (Integral (M,P))) - (Integral (M,P)) by A48, A46, XXREAL_3:56;
then Integral (M,(lim_inf F)) <= (lim_inf I) + ((Integral (M,P)) - (Integral (M,P))) by A48, A46, XXREAL_3:30;
then Integral (M,(lim_inf F)) <= (lim_inf I) + 0. by XXREAL_3:7;
then A57: Integral (M,(lim_inf F)) <= lim_inf I by XXREAL_3:4;
A58: now__::_thesis:_for_n_being_Element_of_NAT_holds_H_._n_is_PartFunc_of_X,ExtREAL
let n be Element of NAT ; ::_thesis: H . n is PartFunc of X,ExtREAL
H . n = P - (F . n) by A33;
hence H . n is PartFunc of X,ExtREAL ; ::_thesis: verum
end;
A59: now__::_thesis:_for_n_being_Nat_holds_H_._n_=_P_-_(F_._n)
let n be Nat; ::_thesis: H . n = P - (F . n)
n is Element of NAT by ORDINAL1:def_12;
hence H . n = P - (F . n) by A33; ::_thesis: verum
end;
A60: E = dom (lim_sup F) by A1, MESFUNC8:def_8;
A61: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_sup_F)_holds_
|.((lim_sup_F)_._x).|_<=_P_._x
let x be Element of X; ::_thesis: ( x in dom (lim_sup F) implies |.((lim_sup F) . x).| <= P . x )
assume A62: x in dom (lim_sup F) ; ::_thesis: |.((lim_sup F) . x).| <= P . x
for k being Nat holds (superior_realsequence (F # x)) . k >= - (P . x)
proof
let k be Nat; ::_thesis: (superior_realsequence (F # x)) . k >= - (P . x)
k is Element of NAT by ORDINAL1:def_12;
then A63: (superior_realsequence (F # x)) . k >= (F # x) . k by RINFSUP2:8;
(F # x) . k >= - (P . x) by A60, A11, A62;
hence (superior_realsequence (F # x)) . k >= - (P . x) by A63, XXREAL_0:2; ::_thesis: verum
end;
then lim_sup (F # x) >= - (P . x) by Th4;
then A64: (lim_sup F) . x >= - (P . x) by A62, MESFUNC8:def_8;
now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(F_#_x)_holds_
P_._x_>=_y
let y be ext-real number ; ::_thesis: ( y in rng (F # x) implies P . x >= y )
assume y in rng (F # x) ; ::_thesis: P . x >= y
then ex k being set st
( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def_3;
hence P . x >= y by A60, A11, A62; ::_thesis: verum
end;
then P . x is UpperBound of rng (F # x) by XXREAL_2:def_1;
then P . x >= sup (rng (F # x)) by XXREAL_2:def_3;
then P . x >= sup ((F # x) ^\ 0) by NAT_1:47;
then A65: P . x >= (superior_realsequence (F # x)) . 0 by RINFSUP2:27;
(superior_realsequence (F # x)) . 0 >= inf (superior_realsequence (F # x)) by RINFSUP2:23;
then P . x >= lim_sup (F # x) by A65, XXREAL_0:2;
then P . x >= (lim_sup F) . x by A62, MESFUNC8:def_8;
hence |.((lim_sup F) . x).| <= P . x by A64, EXTREAL2:12; ::_thesis: verum
end;
lim_sup F is_measurable_on E by A1, A3, MESFUNC8:23;
then A66: lim_sup F is_integrable_on M by A2, A4, A60, A61, MESFUNC5:102;
then A67: ex E6 being Element of S st
( E6 = (dom P) /\ (dom (lim_sup F)) & Integral (M,(P - (lim_sup F))) = (Integral (M,(P | E6))) + (Integral (M,((- (lim_sup F)) | E6))) ) by A4, Th13;
set E1 = Integral (M,(lim_sup F));
A68: Integral (M,(lim_sup F)) < +infty by A66, MESFUNC5:96;
-infty < Integral (M,(lim_sup F)) by A66, MESFUNC5:96;
then reconsider e1 = Integral (M,(lim_sup F)) as Real by A68, XXREAL_0:14;
A69: - (Integral (M,(lim_sup F))) = - e1 by SUPINF_2:2;
A70: P | E = P by A2, RELAT_1:68;
deffunc H4( Element of NAT ) -> Element of K6(K7(X,ExtREAL)) = - (F . $1);
consider F1 being Function such that
A71: ( dom F1 = NAT & ( for n being Element of NAT holds F1 . n = H4(n) ) ) from FUNCT_1:sch_4();
reconsider H = H as Functional_Sequence of X,ExtREAL by A33, A58, SEQFUNC:1;
A72: now__::_thesis:_for_n_being_Nat_holds_dom_(H_._n)_=_E
let n be Nat; ::_thesis: dom (H . n) = E
A73: dom (H . n) = dom (P - (F . n)) by A59;
dom (F . n) = E by A1, MESFUNC8:def_2;
then dom (H . n) = (E /\ E) \ (({} /\ ((F . n) " {+infty})) \/ ({} /\ ((F . n) " {-infty}))) by A2, A29, A26, A73, MESFUNC1:def_4;
hence dom (H . n) = E ; ::_thesis: verum
end;
now__::_thesis:_for_n,_m_being_Nat_holds_dom_(H_._n)_=_dom_(H_._m)
let n, m be Nat; ::_thesis: dom (H . n) = dom (H . m)
thus dom (H . n) = E by A72
.= dom (H . m) by A72 ; ::_thesis: verum
end;
then reconsider H = H as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def_2;
A74: -infty < Integral (M,P) by A4, MESFUNC5:96;
A75: now__::_thesis:_for_n_being_Nat_holds_
(_H_._n_is_nonnegative_&_H_._n_is_measurable_on_E_)
let n be Nat; ::_thesis: ( H . n is nonnegative & H . n is_measurable_on E )
A76: H . n = P - (F . n) by A59;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(F_._n)_holds_
(F_._n)_._x_<=_P_._x
let x be Element of X; ::_thesis: ( x in dom (F . n) implies (F . n) . x <= P . x )
assume x in dom (F . n) ; ::_thesis: (F . n) . x <= P . x
then x in E by A1, MESFUNC8:def_2;
then (F # x) . n <= P . x by A11;
hence (F . n) . x <= P . x by MESFUNC5:def_13; ::_thesis: verum
end;
hence H . n is nonnegative by A76, MESFUNC7:1; ::_thesis: H . n is_measurable_on E
F . n is_integrable_on M by A35;
then H . n is_integrable_on M by A4, A76, Th12;
then ex E4 being Element of S st
( E4 = dom (H . n) & H . n is_measurable_on E4 ) by MESFUNC5:def_17;
hence H . n is_measurable_on E by A72; ::_thesis: verum
end;
E = dom (H . 0) by A72;
then consider IH being ExtREAL_sequence such that
A77: for n being Nat holds IH . n = Integral (M,(H . n)) and
A78: Integral (M,(lim_inf H)) <= lim_inf IH by A75, Th7;
A79: Integral (M,P) < +infty by A4, MESFUNC5:96;
now__::_thesis:_for_n_being_Element_of_NAT_holds_F1_._n_is_PartFunc_of_X,ExtREAL
let n be Element of NAT ; ::_thesis: F1 . n is PartFunc of X,ExtREAL
F1 . n = - (F . n) by A71;
hence F1 . n is PartFunc of X,ExtREAL ; ::_thesis: verum
end;
then reconsider F1 = F1 as Functional_Sequence of X,ExtREAL by A71, SEQFUNC:1;
A80: now__::_thesis:_for_n_being_Nat_holds_F1_._n_=_-_(F_._n)
let n be Nat; ::_thesis: F1 . n = - (F . n)
n is Element of NAT by ORDINAL1:def_12;
hence F1 . n = - (F . n) by A71; ::_thesis: verum
end;
now__::_thesis:_for_n,_m_being_Nat_holds_dom_(F1_._n)_=_dom_(F1_._m)
let n, m be Nat; ::_thesis: dom (F1 . n) = dom (F1 . m)
F1 . m = - (F . m) by A80;
then A81: dom (F1 . m) = dom (F . m) by MESFUNC1:def_7;
F1 . n = - (F . n) by A80;
then dom (F1 . n) = dom (F . n) by MESFUNC1:def_7;
hence dom (F1 . n) = dom (F1 . m) by A81, MESFUNC8:def_2; ::_thesis: verum
end;
then reconsider F1 = F1 as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def_2;
A82: Integral (M,(- (lim_sup F))) = Integral (M,((- 1) (#) (lim_sup F))) by MESFUNC2:9;
A83: now__::_thesis:_for_n_being_Nat_holds_H_._n_=_P_+_(F1_._n)
let n be Nat; ::_thesis: H . n = P + (F1 . n)
H . n = P - (F . n) by A59;
then H . n = P + (- (F . n)) by MESFUNC2:8;
hence H . n = P + (F1 . n) by A80; ::_thesis: verum
end;
F1 . 0 = - (F . 0) by A80;
then A84: dom (F1 . 0) = dom (F . 0) by MESFUNC1:def_7;
then dom (F1 . 0) = dom (H . 0) by A1, A72;
then lim_inf H = P + (lim_inf F1) by A29, A26, A83, Th11;
then lim_inf H = P + (- (lim_sup F)) by A80, A84, Th15;
then A85: lim_inf H = P - (lim_sup F) by MESFUNC2:8;
E = dom (lim_sup F) by A1, MESFUNC8:def_8;
then E = dom (- (lim_sup F)) by MESFUNC1:def_7;
then A86: (- (lim_sup F)) | E = - (lim_sup F) by RELAT_1:68;
deffunc H5( Element of NAT ) -> Element of ExtREAL = - (I . $1);
consider I1 being Function of NAT,ExtREAL such that
A87: for n being Element of NAT holds I1 . n = H5(n) from FUNCT_2:sch_4();
reconsider I1 = I1 as ExtREAL_sequence ;
A88: now__::_thesis:_for_n_being_Nat_holds_I1_._n_=_-_(I_._n)
let n be Nat; ::_thesis: I1 . n = - (I . n)
n is Element of NAT by ORDINAL1:def_12;
hence I1 . n = - (I . n) by A87; ::_thesis: verum
end;
then A89: - (lim_inf I1) = lim_sup I by Th14;
now__::_thesis:_for_n_being_Nat_holds_IH_._n_=_(Integral_(M,P))_+_(I1_._n)
let n be Nat; ::_thesis: IH . n = (Integral (M,P)) + (I1 . n)
A90: F . n is_integrable_on M by A35;
Integral (M,(- (F . n))) = Integral (M,((- 1) (#) (F . n))) by MESFUNC2:9;
then A91: Integral (M,(- (F . n))) = (R_EAL (- 1)) * (Integral (M,(F . n))) by A90, MESFUNC5:110;
A92: dom (F . n) = E by A1, MESFUNC8:def_2;
then E = dom (- (F . n)) by MESFUNC1:def_7;
then A93: (- (F . n)) | E = - (F . n) by RELAT_1:68;
H . n = P - (F . n) by A59;
then A94: ex E5 being Element of S st
( E5 = (dom P) /\ (dom (F . n)) & Integral (M,(H . n)) = (Integral (M,(P | E5))) + (Integral (M,((- (F . n)) | E5))) ) by A4, A90, Th13;
reconsider In = I . n as Real by A49;
A95: (R_EAL (- 1)) * (I . n) = (- 1) * In by EXTREAL1:1;
A96: - (I . n) = - In by SUPINF_2:2;
P | E = P by A2, RELAT_1:68;
then Integral (M,(H . n)) = (Integral (M,P)) + (- (I . n)) by A2, A49, A94, A92, A93, A91, A95, A96;
then IH . n = (Integral (M,P)) + (- (I . n)) by A77;
hence IH . n = (Integral (M,P)) + (I1 . n) by A88; ::_thesis: verum
end;
then lim_inf IH = (Integral (M,P)) + (lim_inf I1) by A24, Th10;
then (Integral (M,P)) + ((R_EAL (- 1)) * (Integral (M,(lim_sup F)))) <= (Integral (M,P)) + (- (lim_sup I)) by A2, A60, A78, A89, A85, A66, A67, A70, A86, A82, MESFUNC5:110;
then (R_EAL (- 1)) * (Integral (M,(lim_sup F))) <= ((- (lim_sup I)) + (Integral (M,P))) - (Integral (M,P)) by A74, A79, XXREAL_3:56;
then (R_EAL (- 1)) * (Integral (M,(lim_sup F))) <= (- (lim_sup I)) + ((Integral (M,P)) - (Integral (M,P))) by A74, A79, XXREAL_3:30;
then A97: (R_EAL (- 1)) * (Integral (M,(lim_sup F))) <= (- (lim_sup I)) + 0. by XXREAL_3:7;
(R_EAL (- 1)) * (Integral (M,(lim_sup F))) = (- 1) * e1 by EXTREAL1:1;
then - (Integral (M,(lim_sup F))) <= - (lim_sup I) by A97, A69, XXREAL_3:4;
then A98: Integral (M,(lim_sup F)) >= lim_sup I by XXREAL_3:38;
now__::_thesis:_(_(_for_x_being_Element_of_X_st_x_in_E_holds_
F_#_x_is_convergent_)_implies_(_I_is_convergent_&_lim_I_=_Integral_(M,(lim_F))_)_)
A99: lim_inf I <= lim_sup I by RINFSUP2:39;
A100: dom (lim F) = dom (F . 0) by MESFUNC8:def_9;
assume A101: for x being Element of X st x in E holds
F # x is convergent ; ::_thesis: ( I is convergent & lim I = Integral (M,(lim F)) )
A102: for x being Element of X st x in dom (lim F) holds
(lim F) . x = (lim_inf F) . x
proof
let x be Element of X; ::_thesis: ( x in dom (lim F) implies (lim F) . x = (lim_inf F) . x )
assume A103: x in dom (lim F) ; ::_thesis: (lim F) . x = (lim_inf F) . x
then F # x is convergent by A1, A101, A100;
hence (lim F) . x = (lim_inf F) . x by A103, MESFUNC8:14; ::_thesis: verum
end;
A104: for x being Element of X st x in dom (lim F) holds
(lim F) . x = (lim_sup F) . x
proof
let x be Element of X; ::_thesis: ( x in dom (lim F) implies (lim F) . x = (lim_sup F) . x )
assume A105: x in dom (lim F) ; ::_thesis: (lim F) . x = (lim_sup F) . x
then F # x is convergent by A1, A101, A100;
hence (lim F) . x = (lim_sup F) . x by A105, MESFUNC8:14; ::_thesis: verum
end;
A106: dom (lim F) = dom (lim_sup F) by A100, MESFUNC8:def_8;
then A107: lim F = lim_sup F by A104, PARTFUN1:5;
A108: dom (lim F) = dom (lim_inf F) by A100, MESFUNC8:def_7;
then Integral (M,(lim F)) <= lim_inf I by A57, A102, PARTFUN1:5;
then lim_sup I <= lim_inf I by A98, A107, XXREAL_0:2;
then lim_inf I = lim_sup I by A99, XXREAL_0:1;
hence A109: I is convergent by RINFSUP2:40; ::_thesis: lim I = Integral (M,(lim F))
then lim I = lim_sup I by RINFSUP2:41;
then A110: lim I <= Integral (M,(lim F)) by A98, A106, A104, PARTFUN1:5;
lim I = lim_inf I by A109, RINFSUP2:41;
then Integral (M,(lim F)) <= lim I by A57, A108, A102, PARTFUN1:5;
hence lim I = Integral (M,(lim F)) by A110, XXREAL_0:1; ::_thesis: verum
end;
hence ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) by A49, A57, A98; ::_thesis: verum
end;
theorem Th17: :: MESFUN10:17
for X being non empty set
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 P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
proof
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 P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim 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 P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let M be sigma_Measure of S; ::_thesis: for E being Element of S
for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let E be Element of S; ::_thesis: for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
let P be PartFunc of X,ExtREAL; ::_thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ) implies ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) )
assume that
A1: E = dom (F . 0) and
A2: E = dom P and
A3: for n being Nat holds F . n is_measurable_on E and
A4: P is_integrable_on M and
A5: P is nonnegative and
A6: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= P . x ; ::_thesis: ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )
for x being set st x in eq_dom (P,+infty) holds
x in E by A2, MESFUNC1:def_15;
then eq_dom (P,+infty) c= E by TARSKI:def_3;
then A7: eq_dom (P,+infty) = E /\ (eq_dom (P,+infty)) by XBOOLE_1:28;
ex A being Element of S st
( A = dom P & P is_measurable_on A ) by A4, MESFUNC5:def_17;
then reconsider E0 = eq_dom (P,+infty) as Element of S by A2, A7, MESFUNC1:33;
reconsider E1 = E \ E0 as Element of S ;
deffunc H1( Nat) -> Element of K6(K7(X,ExtREAL)) = (F . $1) | E1;
consider F1 being Functional_Sequence of X,ExtREAL such that
A8: for n being Nat holds F1 . n = H1(n) from SEQFUNC:sch_1();
A9: now__::_thesis:_for_n_being_Nat_holds_dom_(F1_._n)_=_E1
let n be Nat; ::_thesis: dom (F1 . n) = E1
dom (F . n) = E by A1, MESFUNC8:def_2;
then dom ((F . n) | E1) = E1 by RELAT_1:62, XBOOLE_1:36;
hence dom (F1 . n) = E1 by A8; ::_thesis: verum
end;
then A10: E1 = dom (F1 . 0) ;
now__::_thesis:_for_n,_m_being_Nat_holds_dom_(F1_._n)_=_dom_(F1_._m)
let n, m be Nat; ::_thesis: dom (F1 . n) = dom (F1 . m)
thus dom (F1 . n) = E1 by A9
.= dom (F1 . m) by A9 ; ::_thesis: verum
end;
then reconsider F1 = F1 as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def_2;
set P1 = P | E1;
A11: P | E1 is nonnegative by A5, MESFUNC5:15;
A12: E1 c= E by XBOOLE_1:36;
A13: now__::_thesis:_for_x_being_Element_of_X
for_n_being_Nat_st_x_in_E1_holds_
|.(F1_._n).|_._x_<=_(P_|_E1)_._x
let x be Element of X; ::_thesis: for n being Nat st x in E1 holds
|.(F1 . n).| . x <= (P | E1) . x
let n be Nat; ::_thesis: ( x in E1 implies |.(F1 . n).| . x <= (P | E1) . x )
assume A14: x in E1 ; ::_thesis: |.(F1 . n).| . x <= (P | E1) . x
then A15: (P | E1) . x = P . x by FUNCT_1:49;
x in E by A12, A14;
then x in dom (F . n) by A1, MESFUNC8:def_2;
then x in dom |.(F . n).| by MESFUNC1:def_10;
then A16: |.(F . n).| . x = |.((F . n) . x).| by MESFUNC1:def_10;
E1 = dom (F1 . n) by A9;
then A17: E1 = dom |.(F1 . n).| by MESFUNC1:def_10;
F1 . n = (F . n) | E1 by A8;
then (F1 . n) . x = (F . n) . x by A14, FUNCT_1:49;
then |.(F . n).| . x = |.(F1 . n).| . x by A14, A16, A17, MESFUNC1:def_10;
hence |.(F1 . n).| . x <= (P | E1) . x by A6, A12, A14, A15; ::_thesis: verum
end;
A18: dom (lim F) = dom (F . 0) by MESFUNC8:def_9;
then A19: dom (lim F) = dom (lim_inf F) by MESFUNC8:def_7;
A20: dom (lim_inf F) = E by A1, MESFUNC8:def_7;
A21: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_inf_F1)_holds_
((lim_inf_F)_|_(E_\_E0))_._x_=_(lim_inf_F1)_._x
let x be Element of X; ::_thesis: ( x in dom (lim_inf F1) implies ((lim_inf F) | (E \ E0)) . x = (lim_inf F1) . x )
assume A22: x in dom (lim_inf F1) ; ::_thesis: ((lim_inf F) | (E \ E0)) . x = (lim_inf F1) . x
then A23: x in E1 by A10, MESFUNC8:def_7;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(F1_#_x)_._n_=_(F_#_x)_._n
let n be Element of NAT ; ::_thesis: (F1 # x) . n = (F # x) . n
((F . n) | E1) . x = (F . n) . x by A23, FUNCT_1:49;
then (F1 . n) . x = (F . n) . x by A8;
then (F1 # x) . n = (F . n) . x by MESFUNC5:def_13;
hence (F1 # x) . n = (F # x) . n by MESFUNC5:def_13; ::_thesis: verum
end;
then A24: F1 # x = F # x by FUNCT_2:63;
E1 = dom (lim_inf F1) by A10, MESFUNC8:def_7;
then lim_inf (F # x) = (lim_inf F) . x by A12, A20, A22, MESFUNC8:def_7;
then (lim_inf F1) . x = (lim_inf F) . x by A22, A24, MESFUNC8:def_7;
hence ((lim_inf F) | (E \ E0)) . x = (lim_inf F1) . x by A23, FUNCT_1:49; ::_thesis: verum
end;
E1 = dom ((lim_inf F) | (E \ E0)) by A20, RELAT_1:62, XBOOLE_1:36;
then dom ((lim_inf F) | (E \ E0)) = dom (lim_inf F1) by A10, MESFUNC8:def_7;
then A25: (lim_inf F) | (E \ E0) = lim_inf F1 by A21, PARTFUN1:5;
A26: dom (lim_sup F) = E by A1, MESFUNC8:def_8;
A27: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_sup_F1)_holds_
((lim_sup_F)_|_(E_\_E0))_._x_=_(lim_sup_F1)_._x
let x be Element of X; ::_thesis: ( x in dom (lim_sup F1) implies ((lim_sup F) | (E \ E0)) . x = (lim_sup F1) . x )
assume A28: x in dom (lim_sup F1) ; ::_thesis: ((lim_sup F) | (E \ E0)) . x = (lim_sup F1) . x
then A29: x in E1 by A10, MESFUNC8:def_8;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(F1_#_x)_._n_=_(F_#_x)_._n
let n be Element of NAT ; ::_thesis: (F1 # x) . n = (F # x) . n
((F . n) | E1) . x = (F . n) . x by A29, FUNCT_1:49;
then (F1 . n) . x = (F . n) . x by A8;
then (F1 # x) . n = (F . n) . x by MESFUNC5:def_13;
hence (F1 # x) . n = (F # x) . n by MESFUNC5:def_13; ::_thesis: verum
end;
then A30: F1 # x = F # x by FUNCT_2:63;
E1 = dom (lim_sup F1) by A10, MESFUNC8:def_8;
then lim_sup (F # x) = (lim_sup F) . x by A12, A26, A28, MESFUNC8:def_8;
then (lim_sup F1) . x = (lim_sup F) . x by A28, A30, MESFUNC8:def_8;
hence ((lim_sup F) | (E \ E0)) . x = (lim_sup F1) . x by A29, FUNCT_1:49; ::_thesis: verum
end;
E1 = dom ((lim_sup F) | (E \ E0)) by A26, RELAT_1:62, XBOOLE_1:36;
then dom ((lim_sup F) | (E \ E0)) = dom (lim_sup F1) by A10, MESFUNC8:def_8;
then A31: (lim_sup F) | (E \ E0) = lim_sup F1 by A27, PARTFUN1:5;
A32: dom (P | E1) = E1 by A2, RELAT_1:62, XBOOLE_1:36;
A33: now__::_thesis:_not_eq_dom_((P_|_E1),+infty)_<>_{}
assume eq_dom ((P | E1),+infty) <> {} ; ::_thesis: contradiction
then consider x being set such that
A34: x in eq_dom ((P | E1),+infty) by XBOOLE_0:def_1;
reconsider x = x as Element of X by A34;
(P | E1) . x = +infty by A34, MESFUNC1:def_15;
then consider y being R_eal such that
A35: y = (P | E1) . x and
A36: +infty = y ;
A37: x in E1 by A32, A34, MESFUNC1:def_15;
then y = P . x by A35, FUNCT_1:49;
then x in eq_dom (P,+infty) by A2, A12, A36, A37, MESFUNC1:def_15;
hence contradiction by A37, XBOOLE_0:def_5; ::_thesis: verum
end;
A38: for n being Nat holds F1 . n is_measurable_on E1
proof
let n be Nat; ::_thesis: F1 . n is_measurable_on E1
dom (F . n) = E by A1, MESFUNC8:def_2;
then A39: E1 = (dom (F . n)) /\ E1 by XBOOLE_1:28, XBOOLE_1:36;
F . n is_measurable_on E by A3;
then F . n is_measurable_on E1 by MESFUNC1:30, XBOOLE_1:36;
then (F . n) | E1 is_measurable_on E1 by A39, MESFUNC5:42;
hence F1 . n is_measurable_on E1 by A8; ::_thesis: verum
end;
P | E1 is_integrable_on M by A4, MESFUNC5:112;
then consider I being ExtREAL_sequence such that
A40: for n being Nat holds I . n = Integral (M,(F1 . n)) and
A41: lim_inf I >= Integral (M,(lim_inf F1)) and
A42: lim_sup I <= Integral (M,(lim_sup F1)) and
( ( for x being Element of X st x in E1 holds
F1 # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F1)) ) ) by A32, A10, A11, A13, A38, A33, Lm1;
P " {+infty} = E0 by MESFUNC5:30;
then A43: M . E0 = 0 by A4, MESFUNC5:105;
A44: for n being Nat holds I . n = Integral (M,(F . n))
proof
let n be Nat; ::_thesis: I . n = Integral (M,(F . n))
A45: E = dom (F . n) by A1, MESFUNC8:def_2;
A46: F . n is_measurable_on E by A3;
|.(F . n).| is_integrable_on M by A1, A2, A3, A4, A6, Th16;
then F . n is_integrable_on M by A45, A46, MESFUNC5:100;
then Integral (M,(F . n)) = (Integral (M,((F . n) | E0))) + (Integral (M,((F . n) | E1))) by A45, MESFUNC5:99;
then A47: Integral (M,(F . n)) = 0. + (Integral (M,((F . n) | E1))) by A3, A43, A45, MESFUNC5:94;
I . n = Integral (M,(F1 . n)) by A40;
then I . n = Integral (M,((F . n) | E1)) by A8;
hence I . n = Integral (M,(F . n)) by A47, XXREAL_3:4; ::_thesis: verum
end;
lim_inf F is_measurable_on E by A1, A3, MESFUNC8:24;
then A48: Integral (M,((lim_inf F) | (E \ E0))) = Integral (M,(lim_inf F)) by A43, A20, MESFUNC5:95;
lim_sup F is_measurable_on E by A1, A3, MESFUNC8:23;
then A49: Integral (M,((lim_sup F) | (E \ E0))) = Integral (M,(lim_sup F)) by A43, A26, MESFUNC5:95;
A50: dom (lim F) = dom (lim_sup F) by A18, MESFUNC8:def_8;
now__::_thesis:_(_(_for_x_being_Element_of_X_st_x_in_E_holds_
F_#_x_is_convergent_)_implies_(_I_is_convergent_&_lim_I_=_Integral_(M,(lim_F))_)_)
assume A51: for x being Element of X st x in E holds
F # x is convergent ; ::_thesis: ( I is convergent & lim I = Integral (M,(lim F)) )
A52: for x being Element of X st x in dom (lim F) holds
(lim F) . x = (lim_inf F) . x
proof
let x be Element of X; ::_thesis: ( x in dom (lim F) implies (lim F) . x = (lim_inf F) . x )
assume A53: x in dom (lim F) ; ::_thesis: (lim F) . x = (lim_inf F) . x
then F # x is convergent by A1, A18, A51;
hence (lim F) . x = (lim_inf F) . x by A53, MESFUNC8:14; ::_thesis: verum
end;
then A54: lim F = lim_inf F by A19, PARTFUN1:5;
A55: lim_inf I <= lim_sup I by RINFSUP2:39;
A56: for x being Element of X st x in dom (lim F) holds
(lim F) . x = (lim_sup F) . x
proof
let x be Element of X; ::_thesis: ( x in dom (lim F) implies (lim F) . x = (lim_sup F) . x )
assume A57: x in dom (lim F) ; ::_thesis: (lim F) . x = (lim_sup F) . x
then F # x is convergent by A1, A18, A51;
hence (lim F) . x = (lim_sup F) . x by A57, MESFUNC8:14; ::_thesis: verum
end;
then lim F = lim_sup F by A50, PARTFUN1:5;
then lim_sup I <= lim_inf I by A41, A42, A25, A31, A54, XXREAL_0:2;
then lim_inf I = lim_sup I by A55, XXREAL_0:1;
hence A58: I is convergent by RINFSUP2:40; ::_thesis: lim I = Integral (M,(lim F))
then lim I = lim_sup I by RINFSUP2:41;
then A59: lim I <= Integral (M,(lim F)) by A42, A49, A31, A50, A56, PARTFUN1:5;
lim I = lim_inf I by A58, RINFSUP2:41;
then Integral (M,(lim F)) <= lim I by A41, A48, A25, A19, A52, PARTFUN1:5;
hence lim I = Integral (M,(lim F)) by A59, XXREAL_0:1; ::_thesis: verum
end;
hence ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) by A41, A42, A44, A48, A49, A25, A31; ::_thesis: verum
end;
theorem :: MESFUN10:18
for X being non empty set
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 st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )
proof
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 st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim 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 st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )
let M be sigma_Measure of S; ::_thesis: for E being Element of S st E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )
let E be Element of S; ::_thesis: ( E = dom (F . 0) & ( for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty implies ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) )
assume that
A1: E = dom (F . 0) and
A2: for n being Nat holds
( F . n is nonnegative & F . n is_measurable_on E ) and
A3: for x being Element of X
for n, m being Nat st x in E & n <= m holds
(F . n) . x >= (F . m) . x and
A4: Integral (M,((F . 0) | E)) < +infty ; ::_thesis: ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) )
A5: F . 0 is nonnegative by A2;
A6: dom (F . 0) = dom |.(F . 0).| by MESFUNC1:def_10;
A7: for x being Element of X st x in dom (F . 0) holds
(F . 0) . x = |.(F . 0).| . x
proof
let x be Element of X; ::_thesis: ( x in dom (F . 0) implies (F . 0) . x = |.(F . 0).| . x )
0 <= (F . 0) . x by A5, SUPINF_2:51;
then A8: |.((F . 0) . x).| = (F . 0) . x by EXTREAL1:def_1;
assume x in dom (F . 0) ; ::_thesis: (F . 0) . x = |.(F . 0).| . x
hence (F . 0) . x = |.(F . 0).| . x by A6, A8, MESFUNC1:def_10; ::_thesis: verum
end;
A9: F . 0 is_measurable_on E by A2;
then Integral (M,(F . 0)) = integral+ (M,(F . 0)) by A1, A5, MESFUNC5:88;
then integral+ (M,(F . 0)) < +infty by A1, A4, RELAT_1:68;
then A10: integral+ (M,|.(F . 0).|) < +infty by A6, A7, PARTFUN1:5;
A11: max+ (F . 0) is_measurable_on E by A2, MESFUNC2:25;
for x being set st x in dom (max- (F . 0)) holds
0. <= (max- (F . 0)) . x by MESFUNC2:13;
then A12: max- (F . 0) is nonnegative by SUPINF_2:52;
A13: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= (F . 0) . x
proof
let x be Element of X; ::_thesis: for n being Nat st x in E holds
|.(F . n).| . x <= (F . 0) . x
let n be Nat; ::_thesis: ( x in E implies |.(F . n).| . x <= (F . 0) . x )
assume A14: x in E ; ::_thesis: |.(F . n).| . x <= (F . 0) . x
F . n is nonnegative by A2;
then 0 <= (F . n) . x by SUPINF_2:51;
then |.((F . n) . x).| = (F . n) . x by EXTREAL1:def_1;
then A15: |.((F . n) . x).| <= (F . 0) . x by A3, A14;
dom (F . n) = dom |.(F . n).| by MESFUNC1:def_10;
then x in dom |.(F . n).| by A1, A14, MESFUNC8:def_2;
hence |.(F . n).| . x <= (F . 0) . x by A15, MESFUNC1:def_10; ::_thesis: verum
end;
A16: for x being Element of X st x in E holds
F # x is convergent
proof
let x be Element of X; ::_thesis: ( x in E implies F # x is convergent )
assume A17: x in E ; ::_thesis: F # x is convergent
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_
(F_#_x)_._n_<=_(F_#_x)_._m
let n, m be Element of NAT ; ::_thesis: ( m <= n implies (F # x) . n <= (F # x) . m )
assume m <= n ; ::_thesis: (F # x) . n <= (F # x) . m
then (F . n) . x <= (F . m) . x by A3, A17;
then (F # x) . n <= (F . m) . x by MESFUNC5:def_13;
hence (F # x) . n <= (F # x) . m by MESFUNC5:def_13; ::_thesis: verum
end;
then F # x is non-increasing by RINFSUP2:7;
hence F # x is convergent by RINFSUP2:36; ::_thesis: verum
end;
A18: dom (max+ (F . 0)) = dom (F . 0) by MESFUNC2:def_2;
then A19: (max+ (F . 0)) | E = max+ (F . 0) by A1, RELAT_1:68;
for x being set st x in dom (max+ (F . 0)) holds
0. <= (max+ (F . 0)) . x by MESFUNC2:12;
then A20: max+ (F . 0) is nonnegative by SUPINF_2:52;
then A21: dom ((max+ (F . 0)) + (max- (F . 0))) = (dom (max+ (F . 0))) /\ (dom (max- (F . 0))) by A12, MESFUNC5:22;
A22: dom (max- (F . 0)) = dom (F . 0) by MESFUNC2:def_3;
then A23: (max- (F . 0)) | E = max- (F . 0) by A1, RELAT_1:68;
max- (F . 0) is_measurable_on E by A1, A2, MESFUNC2:26;
then ex C being Element of S st
( C = dom ((max+ (F . 0)) + (max- (F . 0))) & integral+ (M,((max+ (F . 0)) + (max- (F . 0)))) = (integral+ (M,((max+ (F . 0)) | C))) + (integral+ (M,((max- (F . 0)) | C))) ) by A1, A18, A22, A20, A12, A11, MESFUNC5:78;
then A24: (integral+ (M,(max+ (F . 0)))) + (integral+ (M,(max- (F . 0)))) < +infty by A1, A18, A22, A21, A19, A23, A10, MESFUNC2:24;
0 <= integral+ (M,(max- (F . 0))) by A1, A9, A22, A12, MESFUNC2:26, MESFUNC5:79;
then integral+ (M,(max+ (F . 0))) <> +infty by A24, XXREAL_3:def_2;
then A25: integral+ (M,(max+ (F . 0))) < +infty by XXREAL_0:4;
0 <= integral+ (M,(max+ (F . 0))) by A1, A9, A18, A20, MESFUNC2:25, MESFUNC5:79;
then integral+ (M,(max- (F . 0))) <> +infty by A24, XXREAL_3:def_2;
then integral+ (M,(max- (F . 0))) < +infty by XXREAL_0:4;
then F . 0 is_integrable_on M by A1, A9, A25, MESFUNC5:def_17;
then ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) by A1, A2, A13, Th17;
hence ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) by A16; ::_thesis: verum
end;
definition
let X be set ;
let F be Functional_Sequence of X,ExtREAL;
attrF is uniformly_bounded means :Def1: :: MESFUN10:def 1
ex K being real number st
for n being Nat
for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= K;
end;
:: deftheorem Def1 defines uniformly_bounded MESFUN10:def_1_:_
for X being set
for F being Functional_Sequence of X,ExtREAL holds
( F is uniformly_bounded iff ex K being real number st
for n being Nat
for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= K );
theorem :: MESFUN10:19
for X being non empty set
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 st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) )
proof
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 st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim 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 st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for E being Element of S st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) )
let M be sigma_Measure of S; ::_thesis: for E being Element of S st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) holds
( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) )
let E be Element of S; ::_thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds
F # x is convergent ) implies ( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) ) )
assume that
A1: M . E < +infty and
A2: E = dom (F . 0) and
A3: for n being Nat holds F . n is_measurable_on E and
A4: F is uniformly_bounded and
A5: for x being Element of X st x in E holds
F # x is convergent ; ::_thesis: ( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) )
consider K1 being real number such that
A6: for n being Nat
for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= K1 by A4, Def1;
set K = max (K1,1);
max (K1,1) in REAL by XREAL_0:def_1;
then consider h being PartFunc of X,ExtREAL such that
A7: h is_simple_func_in S and
A8: dom h = E and
A9: for x being set st x in E holds
h . x = max (K1,1) by MESFUNC5:41, NUMBERS:31;
A10: dom h = dom |.h.| by MESFUNC1:def_10;
A11: max (K1,1) > 0 by XXREAL_0:30;
then A12: (R_EAL (max (K1,1))) * +infty = +infty by XXREAL_3:def_5;
for x being set st x in E holds
h . x >= 0. by A11, A9;
then A13: h is nonnegative by A8, SUPINF_2:52;
then A14: Integral (M,h) = integral' (M,h) by A7, MESFUNC5:89;
max (K1,1) is Real by XREAL_0:def_1;
then A15: integral' (M,h) = (R_EAL (max (K1,1))) * (M . (dom h)) by A11, A8, A9, MESFUNC5:104;
A16: for x being Element of X st x in dom h holds
h . x = |.h.| . x
proof
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 A17: x in dom |.h.| by MESFUNC1:def_10;
0 <= h . x by A13, SUPINF_2:51;
then |.(h . x).| = h . x by EXTREAL1:def_1;
hence h . x = |.h.| . x by A17, MESFUNC1:def_10; ::_thesis: verum
end;
Integral (M,h) = integral+ (M,h) by A7, A13, MESFUNC5:89;
then integral+ (M,h) < +infty by A1, A11, A8, A15, A12, A14, XXREAL_3:72;
then A18: integral+ (M,|.h.|) < +infty by A10, A16, PARTFUN1:5;
A19: dom (max+ h) = dom h by MESFUNC2:def_2;
then A20: (max+ h) | E = max+ h by A8, RELAT_1:68;
A21: max+ h is_measurable_on E by A7, MESFUNC2:25, MESFUNC2:34;
for x being set st x in dom (max- h) holds
0. <= (max- h) . x by MESFUNC2:13;
then A22: max- h is nonnegative by SUPINF_2:52;
A23: max (K1,1) >= K1 by XXREAL_0:25;
A24: for n being Nat
for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= max (K1,1)
proof
let n be Nat; ::_thesis: for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= max (K1,1)
let x be set ; ::_thesis: ( x in dom (F . 0) implies |.((F . n) . x).| <= max (K1,1) )
assume x in dom (F . 0) ; ::_thesis: |.((F . n) . x).| <= max (K1,1)
then |.((F . n) . x).| <= K1 by A6;
hence |.((F . n) . x).| <= max (K1,1) by A23, XXREAL_0:2; ::_thesis: verum
end;
A25: for x being Element of X
for n being Nat st x in E holds
|.(F . n).| . x <= h . x
proof
let x be Element of X; ::_thesis: for n being Nat st x in E holds
|.(F . n).| . x <= h . x
let n be Nat; ::_thesis: ( x in E implies |.(F . n).| . x <= h . x )
assume A26: x in E ; ::_thesis: |.(F . n).| . x <= h . x
dom (F . n) = dom |.(F . n).| by MESFUNC1:def_10;
then x in dom |.(F . n).| by A2, A26, MESFUNC8:def_2;
then A27: |.(F . n).| . x = |.((F . n) . x).| by MESFUNC1:def_10;
|.((F . n) . x).| <= max (K1,1) by A2, A24, A26;
hence |.(F . n).| . x <= h . x by A9, A26, A27; ::_thesis: verum
end;
for x being set st x in dom (max+ h) holds
0. <= (max+ h) . x by MESFUNC2:12;
then A28: max+ h is nonnegative by SUPINF_2:52;
then A29: dom ((max+ h) + (max- h)) = (dom (max+ h)) /\ (dom (max- h)) by A22, MESFUNC5:22;
A30: dom (max- h) = dom h by MESFUNC2:def_3;
then A31: (max- h) | E = max- h by A8, RELAT_1:68;
max- h is_measurable_on E by A7, A8, MESFUNC2:26, MESFUNC2:34;
then ex C being Element of S st
( C = dom ((max+ h) + (max- h)) & integral+ (M,((max+ h) + (max- h))) = (integral+ (M,((max+ h) | C))) + (integral+ (M,((max- h) | C))) ) by A8, A19, A30, A21, A28, A22, MESFUNC5:78;
then A32: (integral+ (M,(max+ h))) + (integral+ (M,(max- h))) < +infty by A8, A19, A30, A29, A20, A31, A18, MESFUNC2:24;
A33: for x being Element of X st x in dom (lim F) holds
(lim F) . x = (lim_inf F) . x
proof
let x be Element of X; ::_thesis: ( x in dom (lim F) implies (lim F) . x = (lim_inf F) . x )
assume A34: x in dom (lim F) ; ::_thesis: (lim F) . x = (lim_inf F) . x
then x in E by A2, MESFUNC8:def_9;
then F # x is convergent by A5;
hence (lim F) . x = (lim_inf F) . x by A34, MESFUNC8:14; ::_thesis: verum
end;
A35: dom (lim_inf F) = dom (F . 0) by MESFUNC8:def_7;
A36: h is_measurable_on E by A7, MESFUNC2:34;
then 0 <= integral+ (M,(max- h)) by A8, A30, A22, MESFUNC2:26, MESFUNC5:79;
then integral+ (M,(max+ h)) <> +infty by A32, XXREAL_3:def_2;
then A37: integral+ (M,(max+ h)) < +infty by XXREAL_0:4;
0 <= integral+ (M,(max+ h)) by A8, A36, A19, A28, MESFUNC2:25, MESFUNC5:79;
then integral+ (M,(max- h)) <> +infty by A32, XXREAL_3:def_2;
then integral+ (M,(max- h)) < +infty by XXREAL_0:4;
then A38: h is_integrable_on M by A8, A36, A37, MESFUNC5:def_17;
then A39: ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds
F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) by A2, A3, A8, A13, A25, Th17;
A40: now__::_thesis:_for_n_being_Nat_holds_F_._n_is_integrable_on_M
let n be Nat; ::_thesis: F . n is_integrable_on M
A41: E = dom (F . n) by A2, MESFUNC8:def_2;
A42: F . n is_measurable_on E by A3;
|.(F . n).| is_integrable_on M by A2, A3, A8, A38, A25, Th16;
hence F . n is_integrable_on M by A41, A42, MESFUNC5:100; ::_thesis: verum
end;
A43: |.(lim_inf F).| is_integrable_on M by A2, A3, A8, A38, A25, Th16;
dom (lim F) = dom (F . 0) by MESFUNC8:def_9;
then A44: lim F = lim_inf F by A35, A33, PARTFUN1:5;
then lim F is_measurable_on E by A2, A3, MESFUNC8:24;
hence ( ( for n being Nat holds F . n is_integrable_on M ) & lim 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,(lim F)) ) ) by A2, A5, A43, A40, A35, A44, A39, MESFUNC5:100; ::_thesis: verum
end;
definition
let X be set ;
let F be Functional_Sequence of X,ExtREAL;
let f be PartFunc of X,ExtREAL;
predF is_uniformly_convergent_to f means :Def2: :: MESFUN10:def 2
( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being real number st e > 0 holds
ex N being Nat st
for n being Nat
for x being set st n >= N & x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < e ) );
end;
:: deftheorem Def2 defines is_uniformly_convergent_to MESFUN10:def_2_:_
for X being set
for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL holds
( F is_uniformly_convergent_to f iff ( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being real number st e > 0 holds
ex N being Nat st
for n being Nat
for x being set st n >= N & x in dom (F . 0) holds
|.(((F . n) . x) - (f . x)).| < e ) ) );
theorem Th20: :: MESFUN10:20
for X being non empty set
for F1 being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st F1 is_uniformly_convergent_to f holds
for x being Element of X st x in dom (F1 . 0) holds
( F1 # x is convergent & lim (F1 # x) = f . x )
proof
let X be non empty set ; ::_thesis: for F1 being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st F1 is_uniformly_convergent_to f holds
for x being Element of X st x in dom (F1 . 0) holds
( F1 # x is convergent & lim (F1 # x) = f . x )
let F1 be Functional_Sequence of X,ExtREAL; ::_thesis: for f being PartFunc of X,ExtREAL st F1 is_uniformly_convergent_to f holds
for x being Element of X st x in dom (F1 . 0) holds
( F1 # x is convergent & lim (F1 # x) = f . x )
let f be PartFunc of X,ExtREAL; ::_thesis: ( F1 is_uniformly_convergent_to f implies for x being Element of X st x in dom (F1 . 0) holds
( F1 # x is convergent & lim (F1 # x) = f . x ) )
assume A1: F1 is_uniformly_convergent_to f ; ::_thesis: for x being Element of X st x in dom (F1 . 0) holds
( F1 # x is convergent & lim (F1 # x) = f . x )
let x be Element of X; ::_thesis: ( x in dom (F1 . 0) implies ( F1 # x is convergent & lim (F1 # x) = f . x ) )
assume A2: x in dom (F1 . 0) ; ::_thesis: ( F1 # x is convergent & lim (F1 # x) = f . x )
percases ( f . x in REAL or f . x = +infty or f . x = -infty ) by XXREAL_0:14;
suppose f . x in REAL ; ::_thesis: ( F1 # x is convergent & lim (F1 # x) = f . x )
then reconsider g = f . x as real number ;
A3: now__::_thesis:_for_e_being_real_number_st_0_<_e_holds_
ex_N_being_Nat_st_
for_m_being_Nat_st_N_<=_m_holds_
|.(((F1_#_x)_._m)_-_(R_EAL_g)).|_<_e
let e be real number ; ::_thesis: ( 0 < e implies ex N being Nat st
for m being Nat st N <= m holds
|.(((F1 # x) . m) - (R_EAL g)).| < e )
assume 0 < e ; ::_thesis: ex N being Nat st
for m being Nat st N <= m holds
|.(((F1 # x) . m) - (R_EAL g)).| < e
then consider N being Nat such that
A4: for n being Nat
for x being set st n >= N & x in dom (F1 . 0) holds
|.(((F1 . n) . x) - (f . x)).| < e by A1, Def2;
take N = N; ::_thesis: for m being Nat st N <= m holds
|.(((F1 # x) . m) - (R_EAL g)).| < e
hereby ::_thesis: verum
let m be Nat; ::_thesis: ( N <= m implies |.(((F1 # x) . m) - (R_EAL g)).| < e )
assume N <= m ; ::_thesis: |.(((F1 # x) . m) - (R_EAL g)).| < e
then |.(((F1 . m) . x) - (f . x)).| < e by A2, A4;
hence |.(((F1 # x) . m) - (R_EAL g)).| < e by MESFUNC5:def_13; ::_thesis: verum
end;
end;
then A5: F1 # x is convergent_to_finite_number by MESFUNC5:def_8;
then F1 # x is convergent by MESFUNC5:def_11;
hence ( F1 # x is convergent & lim (F1 # x) = f . x ) by A3, A5, MESFUNC5:def_12; ::_thesis: verum
end;
supposeA6: f . x = +infty ; ::_thesis: ( F1 # x is convergent & lim (F1 # x) = f . x )
now__::_thesis:_for_e_being_real_number_st_0_<_e_holds_
ex_N_being_Nat_st_
for_n_being_Nat_st_n_>=_N_holds_
e_<=_(F1_#_x)_._n
let e be real number ; ::_thesis: ( 0 < e implies ex N being Nat st
for n being Nat st n >= N holds
e <= (F1 # x) . n )
assume 0 < e ; ::_thesis: ex N being Nat st
for n being Nat st n >= N holds
e <= (F1 # x) . n
then consider N being Nat such that
A7: for n being Nat
for x being set st n >= N & x in dom (F1 . 0) holds
|.(((F1 . n) . x) - (f . x)).| < e by A1, Def2;
take N = N; ::_thesis: for n being Nat st n >= N holds
e <= (F1 # x) . n
hereby ::_thesis: verum
let n be Nat; ::_thesis: ( n >= N implies e <= (F1 # x) . n )
assume n >= N ; ::_thesis: e <= (F1 # x) . n
then |.(((F1 . n) . x) - (f . x)).| < e by A2, A7;
then A8: |.(- (((F1 . n) . x) - (f . x))).| < e by EXTREAL2:18;
(F1 . n) . x = (F1 # x) . n by MESFUNC5:def_13;
then - (((F1 # x) . n) - (f . x)) < R_EAL e by A8, EXTREAL2:10;
then (f . x) - ((F1 # x) . n) < R_EAL e by XXREAL_3:26;
then (F1 # x) . n = +infty by A6, XXREAL_3:54;
hence e <= (F1 # x) . n by XXREAL_0:3; ::_thesis: verum
end;
end;
then A9: F1 # x is convergent_to_+infty by MESFUNC5:def_9;
then F1 # x is convergent by MESFUNC5:def_11;
hence ( F1 # x is convergent & lim (F1 # x) = f . x ) by A6, A9, MESFUNC5:def_12; ::_thesis: verum
end;
supposeA10: f . x = -infty ; ::_thesis: ( F1 # x is convergent & lim (F1 # x) = f . x )
now__::_thesis:_for_e_being_real_number_st_e_<_0_holds_
ex_N_being_Nat_st_
for_n_being_Nat_st_n_>=_N_holds_
e_>=_(F1_#_x)_._n
let e be real number ; ::_thesis: ( e < 0 implies ex N being Nat st
for n being Nat st n >= N holds
e >= (F1 # x) . n )
assume e < 0 ; ::_thesis: ex N being Nat st
for n being Nat st n >= N holds
e >= (F1 # x) . n
then - 0 < - e by XREAL_1:24;
then consider N being Nat such that
A11: for n being Nat
for x being set st n >= N & x in dom (F1 . 0) holds
|.(((F1 . n) . x) - (f . x)).| < - e by A1, Def2;
take N = N; ::_thesis: for n being Nat st n >= N holds
e >= (F1 # x) . n
hereby ::_thesis: verum
let n be Nat; ::_thesis: ( n >= N implies e >= (F1 # x) . n )
assume n >= N ; ::_thesis: e >= (F1 # x) . n
then A12: |.(((F1 . n) . x) - (f . x)).| < - e by A2, A11;
(F1 . n) . x = (F1 # x) . n by MESFUNC5:def_13;
then ((F1 # x) . n) - (f . x) < R_EAL (- e) by A12, EXTREAL2:10;
then (F1 # x) . n = -infty by A10, XXREAL_3:54;
hence e >= (F1 # x) . n by XXREAL_0:5; ::_thesis: verum
end;
end;
then A13: F1 # x is convergent_to_-infty by MESFUNC5:def_10;
then F1 # x is convergent by MESFUNC5:def_11;
hence ( F1 # x is convergent & lim (F1 # x) = f . x ) by A10, A13, MESFUNC5:def_12; ::_thesis: verum
end;
end;
end;
theorem :: MESFUN10:21
for X being non empty set
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) ) )
proof
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_12;
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:41;
A9: max- h is_measurable_on E by A6, A7, MESFUNC2:26, MESFUNC2:34;
for x being set st x in E holds
h . x >= 0. by A8;
then A10: h is nonnegative by A7, SUPINF_2:52;
then A11: Integral (M,h) = integral' (M,h) by A6, MESFUNC5:89;
set AFN = |.(F . N).|;
A12: dom (F . N) = dom |.(F . N).| by MESFUNC1:def_10;
now__::_thesis:_for_x_being_set_st_x_in_dom_|.(F_._N).|_holds_
0_<=_|.(F_._N).|_._x
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:3; ::_thesis: verum
end;
then A13: |.(F . N).| is nonnegative by SUPINF_2:52;
then A14: dom (|.(F . N).| + h) = (dom |.(F . N).|) /\ (dom h) by A10, MESFUNC5:22;
A15: for x being set st x in dom (F . 0) holds
|.(((F . N) . x) - (f . x)).| < 1 / 2 by A5;
A16: now__::_thesis:_for_x_being_set_
for_n_being_Nat_st_n_>=_N_&_x_in_dom_(F_._0)_holds_
|.(F_._n).|_._x_<=_(|.(F_._N).|_+_h)_._x
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__::_thesis:_(_(_f_._x_=_+infty_or_f_._x_=_-infty_)_implies_|.((F_._n)_._x).|_<=_|.((F_._N)_._x).|_+_1._)
A22: |.(((F . n) . x) - (f . x)).| < 1. by A19, XXREAL_0:2;
then A23: ((F . n) . x) - (f . x) < 1. by EXTREAL2:10;
A24: |.(((F . N) . x) - (f . x)).| < 1. by A20, XXREAL_0:2;
then A25: - 1. < ((F . N) . x) - (f . x) by EXTREAL2:10;
A26: ((F . N) . x) - (f . x) < 1. by A24, EXTREAL2:10;
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:10;
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:53, XXREAL_3:54;
hence |.((F . n) . x).| <= |.((F . N) . x).| + 1. by EXTREAL2:19, XXREAL_3:52; ::_thesis: verum
end;
dom (|.(F . N).| + h) = (dom |.(F . N).|) /\ (dom h) by A10, A13, MESFUNC5:22;
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__::_thesis:_(_f_._x_in_REAL_implies_|.((F_._n)_._x).|_<=_|.((F_._N)_._x).|_+_1._)
A31: 0 <= |.(((F . n) . x) - (f . x)).| by EXTREAL2:3;
|.(((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:3;
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__::_thesis:_(_not_(F_._N)_._x_=_+infty_&_not_(F_._N)_._x_=_-infty_)
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:19, XXREAL_0:9;
hence contradiction by A15, A18, XXREAL_0:2; ::_thesis: verum
end;
A35: now__::_thesis:_(_not_(F_._n)_._x_=_+infty_&_not_(F_._n)_._x_=_-infty_)
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:19, 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:20;
b <= 1 / 2 by A20, MESFUNC5:1;
then a + b < (1 / 2) + (1 / 2) by A19, XREAL_1:8;
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:29;
then ((F . n) . x) - ((F . N) . x) = (((F . n) . x) - (f . x)) + ((f . x) - ((F . N) . x)) by A33, A34, XXREAL_3:30;
then |.(((F . n) . x) - ((F . N) . x)).| <= |.(((F . n) . x) - (f . x)).| + |.((f . x) - ((F . N) . x)).| by EXTREAL2:13;
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:52; ::_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:25, MESFUNC2:34;
for x being set st x in dom (max- h) holds
0. <= (max- h) . x by MESFUNC2:13;
then A41: max- h is nonnegative by SUPINF_2:52;
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__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_f_holds_
(lim_F)_._x_=_f_._x
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_9;
lim (F # x) = f . x by A4, A46, Th20;
hence (lim F) . x = f . x by A47, MESFUNC8:def_9; ::_thesis: verum
end;
dom f = dom (F . 0) by A4, Def2;
then dom (lim F) = dom f by MESFUNC8:def_9;
then A48: lim F = f by A45, PARTFUN1:5;
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:100;
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__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_h_holds_
|.h.|_._x_=_h_._x
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:51;
then |.(h . x).| = h . x by EXTREAL1:def_1;
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:5;
Integral (M,h) = integral+ (M,h) by A6, A10, MESFUNC5:89;
then integral+ (M,h) = (R_EAL 1) * (M . (dom h)) by A7, A8, A11, MESFUNC5:104;
then A55: integral+ (M,|.h.|) < +infty by A1, A7, A54, A51, XXREAL_3:72;
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__::_thesis:_for_n_being_Element_of_NAT_holds_((F_^\_N1)_#_x)_._n_=_((F_#_x)_^\_N1)_._n
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, Th20;
then (F # x) ^\ N1 is convergent by RINFSUP2:21;
hence (F ^\ N1) # x is convergent by A58, FUNCT_2:63; ::_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:63; ::_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_9;
then A61: dom (lim F) = dom (lim (F ^\ N1)) by A2, MESFUNC8:def_9;
A62: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_F)_holds_
(lim_F)_._x_=_(lim_(F_^\_N1))_._x
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_9;
then A64: lim (F # x) = lim ((F ^\ N1) # x) by A57;
lim ((F ^\ N1) # x) = (lim (F ^\ N1)) . x by A61, A63, MESFUNC8:def_9;
hence (lim F) . x = (lim (F ^\ N1)) . x by A63, A64, MESFUNC8:def_9; ::_thesis: verum
end;
A65: dom (max- h) = dom h by MESFUNC2:def_3;
then A66: (max- h) | E = max- h by A7, RELAT_1:68;
A67: dom (max+ h) = dom h by MESFUNC2:def_2;
then A68: (max+ h) | E = max+ h by A7, RELAT_1:68;
for x being set st x in dom (max+ h) holds
0. <= (max+ h) . x by MESFUNC2:12;
then A69: max+ h is nonnegative by SUPINF_2:52;
then dom ((max+ h) + (max- h)) = (dom (max+ h)) /\ (dom (max- h)) by A41, MESFUNC5:22;
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:78;
then A70: integral+ (M,|.h.|) = (integral+ (M,(max+ h))) + (integral+ (M,(max- h))) by A68, A66, MESFUNC2:24;
A71: h is_measurable_on E by A6, MESFUNC2:34;
then 0 <= integral+ (M,(max- h)) by A7, A41, A65, MESFUNC2:26, MESFUNC5:79;
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:25, MESFUNC5:79;
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:108;
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, Th16;
|.(F . N).| + h is nonnegative by A10, A13, MESFUNC5:22;
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, Th17;
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_7;
A80: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_(F_^\_N1))_holds_
(lim_(F_^\_N1))_._x_=_(lim_inf_(F_^\_N1))_._x
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_9;
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_9;
then lim (F ^\ N1) = lim_inf (F ^\ N1) by A79, A80, PARTFUN1:5;
then A82: lim (F ^\ N1) is_integrable_on M by A44, A75, A79, A60, MESFUNC5:100;
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_12;
hence I . n = Integral (M,(F . n)) by A78; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_J_._n_=_(I_^\_N1)_._n
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:63;
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:5;
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:5; ::_thesis: verum
end;