:: Egoroff's Theorem
:: by Noboru Endou , Yasunari Shidama and Keiko Narita
::
:: Received October 30, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, PROB_1, MEASURE1, FUNCT_1, SUBSET_1, XXREAL_0,
ARYTM_3, RELAT_1, SETFAM_1, TARSKI, MEASURE2, ARYTM_1, SETLIM_1, NAT_1,
ORDINAL2, CARD_3, CARD_1, SEQ_2, SEQFUNC, PARTFUN1, PBOOLE, RINFSUP1,
MESFUNC1, XXREAL_2, ZFMISC_1, MESFUNC5, VALUED_0, COMPLEX1, REAL_1,
SUPINF_2, SEQ_1, FUNCOP_1, VALUED_1, PREPOWER, NEWTON, SERIES_1,
MESFUNC8, SEQ_4, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, COMPLEX1, XXREAL_0, XXREAL_2, VALUED_0, PROB_1, REAL_1,
SETFAM_1, MEASURE1, KURATO_0, SETLIM_1, MEASURE2, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, RFUNCT_3, FUNCT_2, SUPINF_2, RINFSUP1, SEQFUNC,
MEASURE6, VALUED_1, NAT_1, SEQ_1, SEQ_2, SEQ_4, NEWTON, PREPOWER,
SERIES_1, EXTREAL1, MESFUNC1, MESFUNC5, RINFSUP2, CARD_3, FUNCOP_1;
constructors REAL_1, NAT_1, EXTREAL1, NEWTON, PREPOWER, SERIES_1, MESFUNC1,
PROB_2, MEASURE6, MEASURE3, PARTFUN3, KURATO_0, RINFSUP1, SETLIM_1,
MESFUNC5, RINFSUP2, SUPINF_1, SEQFUNC, SEQ_4, RELSET_1, BINOP_2, RVSUM_1,
COMSEQ_2;
registrations SUBSET_1, XREAL_0, MEMBERED, ORDINAL1, PARTFUN1, FUNCT_2,
RELAT_1, XXREAL_0, XBOOLE_0, FUNCT_1, NUMBERS, VALUED_0, VALUED_1,
SETLIM_1, SEQ_4, NAT_1, XXREAL_3, RELSET_1, NEWTON, SEQ_2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
reserve n,k for Nat,
X for non empty set,
S for SigmaField of X;
theorem :: MESFUNC8:1
for M be sigma_Measure of S, F be sequence of S, n holds
{x where x is Element of X : for k st n <= k holds x in F.k}
is Element of S;
theorem :: MESFUNC8:2
for F be SetSequence of X, n be Nat holds
(superior_setsequence F).n = union rng (F^\n) &
(inferior_setsequence F).n = meet rng (F^\n);
theorem :: MESFUNC8:3
for M be sigma_Measure of S, F be SetSequence of S
ex G be sequence of S st
G = inferior_setsequence F & M.(lim_inf F) = sup rng(M*G);
theorem :: MESFUNC8:4
for M be sigma_Measure of S, F be SetSequence of S st
M.(Union F) < +infty holds
ex G be sequence of S st G= superior_setsequence F &
M.(lim_sup F) = inf rng(M*G);
theorem :: MESFUNC8:5
for M be sigma_Measure of S, F be SetSequence of S st F is convergent
holds ex G be sequence of S st
G = inferior_setsequence F & M.(lim F) = sup rng (M*G);
theorem :: MESFUNC8:6
for M be sigma_Measure of S, F be SetSequence of S st F is convergent
& M.(Union F) < +infty holds ex G be sequence of S st
G = superior_setsequence F & M.(lim F) = inf rng(M*G);
definition
let X,Y be set, F be Functional_Sequence of X,Y;
attr F is with_the_same_dom means
:: MESFUNC8:def 1
rng F is with_common_domain;
end;
definition
let X,Y be set, F be Functional_Sequence of X,Y;
redefine attr F is with_the_same_dom means
:: MESFUNC8:def 2
for n,m be Nat holds dom(F.n) = dom(F.m);
end;
registration
let X,Y be set;
cluster with_the_same_dom for Functional_Sequence of X,Y;
end;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func inf f -> PartFunc of X,ExtREAL means
:: MESFUNC8:def 3
dom it = dom(f.0) &
for x be Element of X st x in dom it holds it.x = inf(f#x);
end;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func sup f -> PartFunc of X,ExtREAL means
:: MESFUNC8:def 4
dom it = dom(f.0) &
for x be Element of X st x in dom it holds it.x = sup(f#x);
end;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func inferior_realsequence f -> with_the_same_dom Functional_Sequence of X,
ExtREAL means
:: MESFUNC8:def 5
for n be Nat holds dom(it.n) = dom(f.0) &
for x be Element of X st x in dom(it.n) holds
(it.n).x=(inferior_realsequence(f#x)).n;
end;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func superior_realsequence f -> with_the_same_dom Functional_Sequence of X,
ExtREAL means
:: MESFUNC8:def 6
for n be Nat holds dom(it.n) = dom(f.0) &
for x be Element of X st x in dom(it.n) holds
(it.n).x = (superior_realsequence(f#x))
.n;
end;
theorem :: MESFUNC8:7
for f be Functional_Sequence of X,ExtREAL holds
for x be Element of X st x in dom (f.0) holds
(inferior_realsequence f)#x = inferior_realsequence(f#x);
registration
let X,Y be set;
let f be with_the_same_dom Functional_Sequence of X,Y;
let n be Nat;
cluster f^\n -> with_the_same_dom for Functional_Sequence of X,Y;
end;
theorem :: MESFUNC8:8
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
n be Nat holds (inferior_realsequence f).n = inf(f^\n);
theorem :: MESFUNC8:9
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
n be Nat holds (superior_realsequence f).n = sup(f^\n);
theorem :: MESFUNC8:10
for f be Functional_Sequence of X,ExtREAL, x be Element of X st
x in dom(f.0) holds (superior_realsequence f)#x = superior_realsequence(f#x);
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func lim_inf f -> PartFunc of X,ExtREAL means
:: MESFUNC8:def 7
dom it = dom (f.0) &
for x be Element of X st x in dom it holds it.x = lim_inf(f#x);
end;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func lim_sup f -> PartFunc of X,ExtREAL means
:: MESFUNC8:def 8
dom it = dom (f.0) &
for x be Element of X st x in dom it holds it.x = lim_sup(f#x);
end;
theorem :: MESFUNC8:11
for f be Functional_Sequence of X,ExtREAL holds
(for x be Element of X st x in dom lim_inf f holds
(lim_inf f).x=sup inferior_realsequence(f#x) &
(lim_inf f).x=sup ((inferior_realsequence f)#x) &
(lim_inf f).x=sup (inferior_realsequence f).x) &
lim_inf f = sup inferior_realsequence f;
theorem :: MESFUNC8:12
for f be Functional_Sequence of X,ExtREAL holds
(for x be Element of X st x in dom lim_sup f holds
(lim_sup f).x=inf superior_realsequence(f#x) &
(lim_sup f).x=inf ((superior_realsequence f)#x) &
(lim_sup f).x=inf (superior_realsequence f).x ) &
lim_sup f = inf superior_realsequence f;
theorem :: MESFUNC8:13
for f be Functional_Sequence of X,ExtREAL, x be Element of X st
x in dom (f.0) holds f#x is convergent iff (lim_sup f).x = (lim_inf f).x;
definition
let X be non empty set, f be Functional_Sequence of X,ExtREAL;
func lim f -> PartFunc of X,ExtREAL means
:: MESFUNC8:def 9
dom it = dom (f.0) & for x
be Element of X st x in dom it holds it.x=lim(f#x);
end;
theorem :: MESFUNC8:14
for f be Functional_Sequence of X,ExtREAL, x be Element of X st
x in dom lim f & f#x is convergent holds
(lim f).x = (lim_sup f).x &
(lim f).x = (lim_inf f).x;
theorem :: MESFUNC8:15
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be Real st
(for n be Nat holds F.n = dom(f.0) /\ great_dom(f.n,r)) holds
union rng F = dom(f.0) /\ great_dom(sup f,r);
theorem :: MESFUNC8:16
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be Real st
(for n be Nat holds F.n = dom(f.0) /\ great_eq_dom(f.n,r)) holds
meet rng F = dom(f.0) /\ great_eq_dom(inf f,r);
theorem :: MESFUNC8:17
for f be with_the_same_dom Functional_Sequence of X,ExtREAL, F
be SetSequence of S, r be Real st (for n be Nat holds F.n =
dom(f.0) /\ great_dom(f.n,r)) holds for n be Nat holds (
superior_setsequence F).n = dom(f.0) /\ great_dom((superior_realsequence f).n,
r);
theorem :: MESFUNC8:18
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
F be SetSequence of S, r be Real st
(for n be Nat holds F.n = dom(f.0) /\ great_eq_dom(f.n,r))
holds for n be Nat holds
(inferior_setsequence F).n = dom(f.0) /\
great_eq_dom((inferior_realsequence f).n,r);
theorem :: MESFUNC8:19
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S st dom (f.0) = E &
(for n be Nat holds f.n is E-measurable) holds
for n holds (superior_realsequence f).n is E-measurable;
theorem :: MESFUNC8:20
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S st dom (f.0) = E &
(for n be Nat holds f.n is E-measurable) holds
for n be Nat holds (inferior_realsequence f).n is E-measurable;
theorem :: MESFUNC8:21
for f be Functional_Sequence of X,ExtREAL, F be SetSequence of S,
r be Real st
(for n be Nat holds F.n = dom(f.0) /\
great_eq_dom((superior_realsequence f).n,r)) holds
meet F = dom(f.0) /\ great_eq_dom(lim_sup f,r);
theorem :: MESFUNC8:22
for f be Functional_Sequence of X,ExtREAL, F be SetSequence of S,
r be Real st (for n be Nat holds F.n = dom(f.0) /\ great_dom
((inferior_realsequence f).n,r)) holds
union rng F = dom(f.0) /\ great_dom(lim_inf f,r);
theorem :: MESFUNC8:23
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S st dom (f.0) = E &
(for n be Nat holds f.n is E-measurable) holds lim_sup f is E-measurable;
theorem :: MESFUNC8:24
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S st dom(f.0) = E &
(for n be Nat holds f.n is E-measurable) holds lim_inf f is E-measurable;
theorem :: MESFUNC8:25
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
E be Element of S st dom(f.0) = E &
(for n be Nat holds f.n is E-measurable) &
(for x be Element of X st x in E holds f#x is convergent) holds
lim f is E-measurable;
theorem :: MESFUNC8:26
for f be with_the_same_dom Functional_Sequence of X,ExtREAL,
g be PartFunc of X,ExtREAL, E be Element of S st
dom(f.0) = E &
(for n be Nat holds f.n is E-measurable) & dom g = E &
for x be Element of X st x in E holds f#x is convergent &
g.x = lim(f#x) holds g is E-measurable;
theorem :: MESFUNC8:27
for f be Functional_Sequence of X,ExtREAL, g be PartFunc of X,ExtREAL st
for x be Element of X st x in dom g holds
f#x is convergent_to_finite_number &
g.x = lim (f#x) holds g is real-valued;
begin :: Egoroff's Theorem
theorem :: MESFUNC8:28
for M be sigma_Measure of S,
f be with_the_same_dom Functional_Sequence of X,ExtREAL,
g be PartFunc of X,ExtREAL, E be Element of S st
M.E < +infty & dom(f.0) = E &
(for n be Nat holds f.n is E-measurable & f.n is real-valued) &
dom g = E & for x be Element of X st x in E holds
f#x is convergent_to_finite_number & g.x = lim(f#x) holds
for r,e be Real st 0 < r & 0 < e ex H be Element of S, N be Nat st
H c= E & M.H < r & for k be Nat st N < k holds
for x be Element of X st x in E\H holds |. (f.k).x - g.x .| < e;
theorem :: MESFUNC8:29
for X,Y be non empty set, E be set, F,G be Function of X,Y st
for x be Element of X holds G.x = E \ F.x holds
union rng G = E \ meet rng F;
::$N Egorov's theorem
theorem :: MESFUNC8:30
for M be sigma_Measure of S,
f be with_the_same_dom Functional_Sequence of X,ExtREAL,
g be PartFunc of X,ExtREAL, E be Element of S st
(dom (f.0) = E & for n be Nat holds f.n is E-measurable) &
M.E < +infty &
(for n be Nat holds ex L be Element of S st L c= E &
M.(E\L) = 0 &
for x be Element of X st x in L holds |. (f.n).x .| < +infty) &
ex G be Element of S st G c= E & M.(E\G) = 0 &
(for x be Element of X st x in E holds
f#x is convergent_to_finite_number) & dom g = E &
(for x be Element of X st x in G holds g.x = lim (f#x)) holds
for e be Real st 0 < e ex F be Element of S st
F c= E & M.(E\F) <= e & for p be Real st 0 < p ex N be Nat st
for n be Nat st N < n holds
for x be Element of X st x in F holds |. (f.n).x - g.x .| < p;