:: On $L^1$ Space Formed by Real-valued Partial Functions :: by Yasushige Watase , Noboru Endou and Yasunari Shidama :: :: Received August 26, 2008 :: Copyright (c) 2008-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, RLVECT_1, SUBSET_1, REAL_1, RELAT_1, RLSUB_1, IDEAL_1, ARYTM_3, STRUCT_0, RSSPACE, FUNCT_1, ZFMISC_1, TARSKI, BINOP_1, SUPINF_2, ALGSTR_0, REALSET1, FUNCT_7, PARTFUN1, VALUED_1, FUNCOP_1, CARD_1, RFUNCT_3, ARYTM_1, PROB_1, MEASURE1, NAT_1, INTEGRA5, MESFUNC5, MESFUNC2, XXREAL_0, MESFUNC1, SUPINF_1, MEASURE6, VECTSP10, SETFAM_1, COMPLEX1, PRE_TOPC, NORMSP_1, LPSPACE1, XCMPLX_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XXREAL_3, XCMPLX_0, NUMBERS, COMPLEX1, XXREAL_0, XREAL_0, SUPINF_1, SUPINF_2, EXTREAL1, REALSET1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, VALUED_1, RFUNCT_3, BINOP_1, NAT_1, FUNCOP_1, REAL_1, STRUCT_0, ALGSTR_0, RLVECT_1, RLSUB_1, IDEAL_1, SETFAM_1, DOMAIN_1, PRE_TOPC, NORMSP_0, NORMSP_1, PROB_1, MEASURE1, MEASURE2, MEASURE3, MEASURE6, MESFUNC1, MESFUNC2, MESFUNC5, MESFUNC6, FUNCT_7; constructors COMPLEX1, EXTREAL1, BINOP_1, REAL_1, RLSUB_1, IDEAL_1, NORMSP_1, MEASURE3, MEASURE6, MESFUNC2, MESFUNC5, MESFUNC6, SUPINF_1, FUNCT_7, REALSET1, MESFUNC1, RELSET_1, BINOP_2, NUMBERS; registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, NAT_1, SUBSET_1, PARTFUN1, XXREAL_0, RLVECT_1, STRUCT_0, NORMSP_1, MEASURE1, MESFUNC7, XXREAL_3; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin :: Preliminaries of Real Linear Space definition let V be non empty RLSStruct, V1 be Subset of V; attr V1 is multi-closed means :: LPSPACE1:def 1 for a be Real, v be VECTOR of V st v in V1 holds a*v in V1; end; theorem :: LPSPACE1:1 for V be RealLinearSpace, V1 be Subset of V holds V1 is linearly-closed iff V1 is add-closed multi-closed; registration let V be non empty RLSStruct; cluster add-closed multi-closed non empty for Subset of V; end; definition let X be non empty RLSStruct; let X1 be multi-closed non empty Subset of X; func Mult_X1 -> Function of [:REAL,X1:], X1 equals :: LPSPACE1:def 2 (the Mult of X) | [:REAL, X1:]; end; reserve a,b,r for Real; theorem :: LPSPACE1:2 for V be Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, V1 be non empty Subset of V, d1 be Element of V1, A be BinOp of V1, M be Function of [:REAL,V1:],V1 st d1 = 0.V & A = (the addF of V)|| V1 & M = (the Mult of V)|[:REAL,V1:] holds RLSStruct(# V1 ,d1,A,M #) is Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital; theorem :: LPSPACE1:3 for V be Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct, V1 be add-closed multi-closed non empty Subset of V st 0.V in V1 holds RLSStruct (# V1,In (0.V, V1), add|(V1,V), Mult_ V1 #) is Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital; theorem :: LPSPACE1:4 for V be non empty RLSStruct, V1 be add-closed multi-closed non empty Subset of V, v,u be VECTOR of V, w1,w2 be VECTOR of RLSStruct (# V1,In(0. V,V1), add|(V1,V), Mult_ V1 #) st w1 = v & w2 = u holds w1 + w2 = v + u; theorem :: LPSPACE1:5 for V be non empty RLSStruct, V1 be add-closed multi-closed non empty Subset of V, a be Real, v be VECTOR of V, w be VECTOR of RLSStruct (# V1, In (0.V, V1), add|(V1,V), Mult_ V1 #) st w = v holds a*w = a*v; begin :: Quasi-Real Linear Space of Partial Functions reserve A,B for non empty set; reserve f,g,h for Element of PFuncs(A,REAL); definition let A,B; let F be BinOp of PFuncs(A,B), f,g be Element of PFuncs(A,B); redefine func F.(f,g) -> Element of PFuncs(A,B); end; definition let A; func multpfunc A -> BinOp of PFuncs(A,REAL) means :: LPSPACE1:def 3 for f,g being Element of PFuncs(A,REAL) holds it.(f,g) = f(#)g; end; definition let A; func multrealpfunc A -> Function of [:REAL,PFuncs(A,REAL):],PFuncs(A,REAL) means :: LPSPACE1:def 4 for a being Real, f being Element of PFuncs(A,REAL) holds it.(a,f) = a(#)f; end; definition let A; func RealPFuncZero A -> Element of PFuncs(A,REAL) equals :: LPSPACE1:def 5 A --> 0; end; definition let A; func RealPFuncUnit A -> Element of PFuncs(A,REAL) equals :: LPSPACE1:def 6 A --> 1; end; theorem :: LPSPACE1:6 h = (addpfunc A).(f,g) iff (dom h= dom f /\ dom g & for x being Element of A st x in dom h holds h.x = f.x + g.x); theorem :: LPSPACE1:7 h = (multpfunc A).(f,g) iff dom h = dom f /\ dom g & for x being Element of A st x in dom h holds h.x = f.x * g.x; theorem :: LPSPACE1:8 RealPFuncZero A <> RealPFuncUnit A; theorem :: LPSPACE1:9 h = (multrealpfunc A).(a,f) iff dom h = dom f & for x being Element of A st x in dom f holds h.x = a * f.x; theorem :: LPSPACE1:10 (addpfunc A).(f,g) = (addpfunc A).(g,f); theorem :: LPSPACE1:11 (addpfunc A).(f,(addpfunc A).(g,h)) = (addpfunc A).((addpfunc A) .(f,g),h); theorem :: LPSPACE1:12 (multpfunc A).(f,g) = (multpfunc A).(g,f); theorem :: LPSPACE1:13 (multpfunc A).(f,(multpfunc A).(g,h)) = (multpfunc A).((multpfunc A).( f,g),h); theorem :: LPSPACE1:14 (multpfunc A).(RealPFuncUnit A,f) = f; theorem :: LPSPACE1:15 (addpfunc A).(RealPFuncZero A,f) = f; theorem :: LPSPACE1:16 (addpfunc A).(f,(multrealpfunc A).(-1,f)) = (RealPFuncZero A)|( dom f); theorem :: LPSPACE1:17 (multrealpfunc A).(1,f) = f; theorem :: LPSPACE1:18 (multrealpfunc A).(a,(multrealpfunc A).(b,f)) = (multrealpfunc A ).(a*b,f); theorem :: LPSPACE1:19 (addpfunc A).((multrealpfunc A).(a,f),(multrealpfunc A).(b,f)) = (multrealpfunc A).(a+b,f); theorem :: LPSPACE1:20 (multpfunc A).(f,(addpfunc A).(g,h)) = (addpfunc A).((multpfunc A).(f, g),(multpfunc A).(f,h)); theorem :: LPSPACE1:21 (multpfunc A).((multrealpfunc A).(a,f),g) = (multrealpfunc A).(a,( multpfunc A).(f,g)); definition let A; func RLSp_PFunctA -> non empty RLSStruct equals :: LPSPACE1:def 7 RLSStruct(#PFuncs(A,REAL), RealPFuncZero A, addpfunc A, multrealpfunc A#); end; reserve u,v,w for VECTOR of RLSp_PFunctA; registration let A; cluster RLSp_PFunctA -> strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital; end; begin :: Quasi-Real Linear Space of Integrable Functions reserve X for non empty set, x for Element of X, S for SigmaField of X, M for sigma_Measure of S, E,E1,E2 for Element of S, f,g,h,f1,g1 for PartFunc of X ,REAL; theorem :: LPSPACE1:22 for X,S,M for f be PartFunc of X,ExtREAL st (ex E st E = dom f) & for x st x in dom f holds 0= f.x holds f is_integrable_on M & Integral(M,f) = 0; definition let X be non empty set, r be Real; redefine func X --> r -> PartFunc of X,REAL; end; definition let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; func L1_Functions M -> non empty Subset of RLSp_PFunctX equals :: LPSPACE1:def 8 { f where f is PartFunc of X,REAL : ex ND be Element of S st M.ND=0 & dom f = ND` & f is_integrable_on M }; end; theorem :: LPSPACE1:23 f in L1_Functions M & g in L1_Functions M implies f + g in L1_Functions M; theorem :: LPSPACE1:24 f in L1_Functions M implies a(#)f in L1_Functions M; registration let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; cluster L1_Functions M -> multi-closed add-closed; end; definition let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; func RLSp_L1Funct M -> non empty RLSStruct equals :: LPSPACE1:def 9 RLSStruct (# L1_Functions M, In (0.(RLSp_PFunctX), L1_Functions M), add|(L1_Functions M,RLSp_PFunctX), Mult_(L1_Functions M) #); end; registration let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; cluster RLSp_L1Funct M -> strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital; end; begin :: Quotient Space of Quasi-Real Linear Space of Integrable Functions reserve v,u for VECTOR of RLSp_L1Funct M; theorem :: LPSPACE1:25 f=v & g=u implies f+g=v+u; theorem :: LPSPACE1:26 f=u implies a(#)f=a*u; definition let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g be PartFunc of X,REAL; pred f a.e.= g,M means :: LPSPACE1:def 10 ex E be Element of S st M.E = 0 & f|E` = g|E`; end; theorem :: LPSPACE1:27 f=u implies u+(-1)*u = (X --> 0)|dom f & ex v,g be PartFunc of X ,REAL st v in L1_Functions M & g in L1_Functions M & v = u+(-1)*u & g = X --> 0 & v a.e.= g,M; theorem :: LPSPACE1:28 f a.e.= f,M; theorem :: LPSPACE1:29 f a.e.= g,M implies g a.e.= f,M; theorem :: LPSPACE1:30 f a.e.= g,M & g a.e.= h,M implies f a.e.= h,M; theorem :: LPSPACE1:31 f a.e.= f1,M & g a.e.= g1,M implies (f+g) a.e.= (f1+g1),M; theorem :: LPSPACE1:32 f a.e.= g,M implies a(#)f a.e.= a(#)g,M; definition let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; func AlmostZeroFunctions M -> non empty Subset of RLSp_L1Funct M equals :: LPSPACE1:def 11 { f where f is PartFunc of X,REAL : f in L1_Functions M & f a.e.= X-->0,M }; end; theorem :: LPSPACE1:33 (X-->0) + (X-->0) = X-->0 & a(#)(X-->0) = X-->0; registration let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; cluster AlmostZeroFunctions M -> add-closed multi-closed; end; theorem :: LPSPACE1:34 0.(RLSp_L1Funct M) = X-->0 & 0.(RLSp_L1Funct M) in AlmostZeroFunctions M; definition let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; func RLSp_AlmostZeroFunct M -> non empty RLSStruct equals :: LPSPACE1:def 12 RLSStruct (# AlmostZeroFunctions M, In(0.(RLSp_L1Funct M),AlmostZeroFunctions M), add|( AlmostZeroFunctions M,RLSp_L1Funct M), Mult_(AlmostZeroFunctions M) #); end; registration let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; cluster RLSp_L1Funct M -> strict strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital; end; reserve v,u for VECTOR of RLSp_AlmostZeroFunct M; theorem :: LPSPACE1:35 f=v & g=u implies f+g=v+u; theorem :: LPSPACE1:36 f=u implies a(#)f=a*u; definition let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be PartFunc of X,REAL; func a.e-eq-class(f,M) -> Subset of L1_Functions M equals :: LPSPACE1:def 13 {g where g is PartFunc of X,REAL : g in L1_Functions M & f in L1_Functions M & f a.e.= g,M }; end; theorem :: LPSPACE1:37 f in L1_Functions M & g in L1_Functions M implies (g a.e.= f,M iff g in a.e-eq-class(f,M)); theorem :: LPSPACE1:38 f in L1_Functions M implies f in a.e-eq-class(f,M); theorem :: LPSPACE1:39 f in L1_Functions M & g in L1_Functions M implies (a.e-eq-class( f,M) = a.e-eq-class(g,M) iff f a.e.= g,M); theorem :: LPSPACE1:40 f in L1_Functions M & g in L1_Functions M implies (a.e-eq-class(f,M) = a.e-eq-class(g,M) iff g in a.e-eq-class(f,M)); theorem :: LPSPACE1:41 f in L1_Functions M & f1 in L1_Functions M & g in L1_Functions M & g1 in L1_Functions M & a.e-eq-class(f,M) = a.e-eq-class(f1,M) & a.e-eq-class( g,M) = a.e-eq-class(g1,M) implies a.e-eq-class(f+g,M) = a.e-eq-class(f1+g1,M) ; theorem :: LPSPACE1:42 f in L1_Functions M & g in L1_Functions M & a.e-eq-class(f,M) = a.e-eq-class(g,M) implies a.e-eq-class(a(#)f,M) = a.e-eq-class(a(#)g,M); definition let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; func CosetSet M -> non empty Subset-Family of L1_Functions M equals :: LPSPACE1:def 14 { a.e-eq-class(f,M) where f is PartFunc of X,REAL : f in L1_Functions M}; end; definition let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; func addCoset M -> BinOp of CosetSet M means :: LPSPACE1:def 15 for A,B be Element of CosetSet M, a,b be PartFunc of X,REAL st a in A & b in B holds it.(A,B) = a.e-eq-class(a+b,M); end; definition let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; func zeroCoset M -> Element of CosetSet M means :: LPSPACE1:def 16 ex f be PartFunc of X,REAL st f = X --> 0 & f in L1_Functions M & it = a.e-eq-class(f,M); end; definition let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; func lmultCoset M -> Function of [:REAL, CosetSet M:],CosetSet M means :: LPSPACE1:def 17 for z be Real, A be Element of CosetSet M, f be PartFunc of X ,REAL st f in A holds it.(z,A) = a.e-eq-class(z(#)f,M); end; definition let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; func Pre-L-Space M -> strict Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLSStruct means :: LPSPACE1:def 18 the carrier of it = CosetSet M & the addF of it = addCoset M & 0.it = zeroCoset M & the Mult of it = lmultCoset M; end; begin :: Real Normed Space of Integrable Functions theorem :: LPSPACE1:43 f in L1_Functions M & g in L1_Functions M & f a.e.= g,M implies Integral(M,f) = Integral(M,g); theorem :: LPSPACE1:44 f is_integrable_on M implies Integral(M,f) in REAL & Integral(M, abs f) in REAL & abs f is_integrable_on M; theorem :: LPSPACE1:45 f in L1_Functions M & g in L1_Functions M & f a.e.= g,M implies abs f a.e.= (abs g),M & Integral(M,abs f) = Integral(M,abs g); theorem :: LPSPACE1:46 (ex x be VECTOR of Pre-L-Space M st f in x & g in x) implies f a.e.= g,M & f in L1_Functions M & g in L1_Functions M; reserve x for Point of Pre-L-Space M; theorem :: LPSPACE1:47 f in x implies f is_integrable_on M & f in L1_Functions M & abs f is_integrable_on M; theorem :: LPSPACE1:48 f in x & g in x implies f a.e.= g,M & Integral(M,f) = Integral(M ,g) & Integral(M,abs f) = Integral(M,abs g); definition let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; func L-1-Norm M -> Function of the carrier of Pre-L-Space M,REAL means :: LPSPACE1:def 19 for x be Point of Pre-L-Space M ex f be PartFunc of X,REAL st f in x & it.x = Integral(M,abs f); end; definition let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; func L-1-Space M -> non empty NORMSTR equals :: LPSPACE1:def 20 NORMSTR (# the carrier of Pre-L-Space M, the ZeroF of Pre-L-Space M, the addF of Pre-L-Space M, the Mult of Pre-L-Space M, L-1-Norm M #); end; reserve x,y for Point of L-1-Space M; theorem :: LPSPACE1:49 ( ex f be PartFunc of X,REAL st f in L1_Functions M & x= a.e-eq-class(f,M) & ||.x.|| = Integral(M,abs f) ) & for f be PartFunc of X,REAL st f in x holds Integral(M,abs f) = ||.x.||; theorem :: LPSPACE1:50 f in x implies x= a.e-eq-class(f,M) & ||.x.|| = Integral(M,abs f ); theorem :: LPSPACE1:51 (f in x & g in y implies f+g in x+y) & (f in x implies a(#)f in a*x); theorem :: LPSPACE1:52 E = dom f & (for x be set st x in dom f holds f.x=r) implies f is E-measurable; theorem :: LPSPACE1:53 f in L1_Functions M & Integral(M,abs f) = 0 implies f a.e.= X--> 0,M; theorem :: LPSPACE1:54 Integral(M,abs(X-->0)) = 0; theorem :: LPSPACE1:55 f is_integrable_on M & g is_integrable_on M implies Integral(M, abs(f+g)) <= Integral(M,abs f) + Integral(M,abs g); registration let X be non empty set, S be SigmaField of X, M be sigma_Measure of S; cluster L-1-Space M -> RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable; end;