:: by Noboru Endou , Keiko Narita and Yasunari Shidama

::

:: Received July 22, 2008

:: Copyright (c) 2008-2018 Association of Mizar Users

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)

inf (rng seq1) <= inf (rng seq2)

proof 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 )

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 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 )

( lim_inf seq1 <= lim_inf seq2 & lim_sup seq1 <= lim_sup seq2 )

proof 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

for a being R_eal st ( for n being Nat holds seq . n >= a ) holds

inf seq >= a

proof 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

for a being R_eal st ( for n being Nat holds seq . n <= a ) holds

sup seq <= a

proof 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)

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 end;

:: Fatou's Lemma

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 )

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 end;

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)

for r being R_eal st r in REAL holds

sup ({r} + Y) = (sup {r}) + (sup Y)

proof 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)

for r being R_eal st r in REAL holds

inf ({r} + Y) = (inf {r}) + (inf Y)

proof 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) )

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 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) )

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 end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

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

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 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))) )

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 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) )

( lim_inf seq2 = - (lim_sup seq1) & lim_sup seq2 = - (lim_inf seq1) )

proof 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) )

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 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 )

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 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 end;

:: Lebesgue's Convergence theorem

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)) ) ) )

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 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)) )

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 end;

:: deftheorem 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 st

for n being Nat

for x being set st x in dom (F . 0) holds

|.((F . n) . x).| <= K );

for X being set

for F being Functional_Sequence of X,ExtREAL holds

( F is uniformly_bounded iff ex K being Real 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)) ) )

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 end;

definition
end;

:: deftheorem 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 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 ) ) );

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 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 )

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 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) ) )

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 end;