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