:: On $L^p$ Space Formed by Real-valued Partial Functions :: by Yasushige Watase , Noboru Endou and Yasunari Shidama :: :: Received February 4, 2010 :: Copyright (c) 2010-2012 Association of Mizar Users begin theorem Th1: :: LPSPACE2:1 for m, n being positive real number st (1 / m) + (1 / n) = 1 holds m > 1 proofend; theorem Th2: :: LPSPACE2:2 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for A being Element of S for f being PartFunc of X,ExtREAL st A = dom f & f is_measurable_on A & f is nonnegative holds ( Integral (M,f) in REAL iff f is_integrable_on M ) proofend; definition let r be real number ; attrr is geq_than_1 means :Def1: :: LPSPACE2:def 1 1 <= r; end; :: deftheorem Def1 defines geq_than_1 LPSPACE2:def_1_:_ for r being real number holds ( r is geq_than_1 iff 1 <= r ); registration cluster real geq_than_1 -> positive real for set ; coherence for b1 being real number st b1 is geq_than_1 holds b1 is positive proofend; end; registration cluster ext-real V38() real geq_than_1 for Element of REAL ; existence ex b1 being Real st b1 is geq_than_1 proofend; end; theorem Th3: :: LPSPACE2:3 for a, b, p being Real st 0 < p & 0 <= a & a < b holds a to_power p < b to_power p proofend; theorem Th4: :: LPSPACE2:4 for a, b being Real st a >= 0 & b > 0 holds a to_power b >= 0 proofend; theorem Th5: :: LPSPACE2:5 for a, b, c being Real st a >= 0 & b >= 0 & c > 0 holds (a * b) to_power c = (a to_power c) * (b to_power c) proofend; theorem Th6: :: LPSPACE2:6 for X being non empty set for a, b being Real for f being PartFunc of X,REAL st f is nonnegative & a > 0 & b > 0 holds (f to_power a) to_power b = f to_power (a * b) proofend; theorem Th7: :: LPSPACE2:7 for X being non empty set for a, b being Real for f being PartFunc of X,REAL st f is nonnegative & a > 0 & b > 0 holds (f to_power a) (#) (f to_power b) = f to_power (a + b) proofend; theorem Th8: :: LPSPACE2:8 for X being non empty set for f being PartFunc of X,REAL holds f to_power 1 = f proofend; theorem Th9: :: LPSPACE2:9 for seq1, seq2 being Real_Sequence for k being positive Real st ( for n being Element of NAT holds ( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ) holds ( seq1 is convergent iff seq2 is convergent ) proofend; theorem Th10: :: LPSPACE2:10 for seq being Real_Sequence for n, m being Element of NAT st m <= n holds ( abs (((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)) <= ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) & abs (((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)) <= (Partial_Sums (abs seq)) . n ) proofend; theorem Th11: :: LPSPACE2:11 for seq, seq2 being Real_Sequence for k being positive Real st seq is convergent & ( for n being Element of NAT holds seq2 . n = |.((lim seq) - (seq . n)).| to_power k ) holds ( seq2 is convergent & lim seq2 = 0 ) proofend; Lm1: for seq being Real_Sequence for n being Element of NAT holds abs ((Partial_Sums seq) . n) <= (Partial_Sums (abs seq)) . n by NAGATA_2:13; begin theorem Th12: :: LPSPACE2:12 for k being positive Real for X being non empty set holds (X --> 0) to_power k = X --> 0 proofend; theorem Th13: :: LPSPACE2:13 for X being non empty set for f being PartFunc of X,REAL for D being set holds abs (f | D) = (abs f) | D proofend; registration let X be non empty set ; let f be PartFunc of X,REAL; cluster|.f.| -> nonnegative ; coherence abs f is nonnegative proofend; end; theorem Th14: :: LPSPACE2:14 for X being non empty set for f being PartFunc of X,REAL st f is nonnegative holds abs f = f proofend; theorem Th15: :: LPSPACE2:15 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL st X = dom f & ( for x being Element of X st x in dom f holds 0 = f . x ) holds ( f is_integrable_on M & Integral (M,f) = 0 ) proofend; definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; func Lp_Functions (M,k) -> non empty Subset of (RLSp_PFunct X) equals :: LPSPACE2:def 2 { f where f is PartFunc of X,REAL : ex Ef being Element of S st ( M . (Ef `) = 0 & dom f = Ef & f is_measurable_on Ef & (abs f) to_power k is_integrable_on M ) } ; correctness coherence { f where f is PartFunc of X,REAL : ex Ef being Element of S st ( M . (Ef `) = 0 & dom f = Ef & f is_measurable_on Ef & (abs f) to_power k is_integrable_on M ) } is non empty Subset of (RLSp_PFunct X); proofend; end; :: deftheorem defines Lp_Functions LPSPACE2:def_2_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real holds Lp_Functions (M,k) = { f where f is PartFunc of X,REAL : ex Ef being Element of S st ( M . (Ef `) = 0 & dom f = Ef & f is_measurable_on Ef & (abs f) to_power k is_integrable_on M ) } ; theorem Th16: :: LPSPACE2:16 for a, b, k being Real st k > 0 holds ( (abs (a + b)) to_power k <= ((abs a) + (abs b)) to_power k & ((abs a) + (abs b)) to_power k <= (2 * (max ((abs a),(abs b)))) to_power k & (abs (a + b)) to_power k <= (2 * (max ((abs a),(abs b)))) to_power k ) proofend; theorem Th17: :: LPSPACE2:17 for a, b, k being Real st a >= 0 & b >= 0 & k > 0 holds (max (a,b)) to_power k <= (a to_power k) + (b to_power k) proofend; theorem Th18: :: LPSPACE2:18 for X being non empty set for f being PartFunc of X,REAL for a, b being Real st b > 0 holds ((abs a) to_power b) (#) ((abs f) to_power b) = (abs (a (#) f)) to_power b proofend; theorem Th19: :: LPSPACE2:19 for X being non empty set for f being PartFunc of X,REAL for a, b being Real st a > 0 & b > 0 holds (a to_power b) (#) ((abs f) to_power b) = (a (#) (abs f)) to_power b proofend; theorem Th20: :: LPSPACE2:20 for X being non empty set for f being PartFunc of X,REAL for k being real number for E being set holds (f | E) to_power k = (f to_power k) | E proofend; theorem Th21: :: LPSPACE2:21 for a, b, k being Real st k > 0 holds (abs (a + b)) to_power k <= (2 to_power k) * (((abs a) to_power k) + ((abs b) to_power k)) proofend; theorem Th22: :: LPSPACE2:22 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real for f, g being PartFunc of X,REAL st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) holds ( (abs f) to_power k is_integrable_on M & (abs g) to_power k is_integrable_on M & ((abs f) to_power k) + ((abs g) to_power k) is_integrable_on M ) proofend; theorem Th23: :: LPSPACE2:23 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real holds ( X --> 0 is PartFunc of X,REAL & X --> 0 in Lp_Functions (M,k) ) proofend; theorem Th24: :: LPSPACE2:24 for X being non empty set for k being Real st k > 0 holds for f, g being PartFunc of X,REAL for x being Element of X st x in (dom f) /\ (dom g) holds ((abs (f + g)) to_power k) . x <= ((2 to_power k) (#) (((abs f) to_power k) + ((abs g) to_power k))) . x proofend; theorem Th25: :: LPSPACE2:25 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,REAL for k being positive Real st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) holds f + g in Lp_Functions (M,k) proofend; theorem Th26: :: LPSPACE2:26 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for a being Real for k being positive Real st f in Lp_Functions (M,k) holds a (#) f in Lp_Functions (M,k) proofend; theorem Th27: :: LPSPACE2:27 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,REAL for k being positive Real st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) holds f - g in Lp_Functions (M,k) proofend; theorem Th28: :: LPSPACE2:28 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for k being positive Real st f in Lp_Functions (M,k) holds abs f in Lp_Functions (M,k) proofend; Lm2: for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real holds ( Lp_Functions (M,k) is add-closed & Lp_Functions (M,k) is multi-closed ) proofend; registration let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; cluster Lp_Functions (M,k) -> non empty add-closed multi-closed ; coherence ( Lp_Functions (M,k) is multi-closed & Lp_Functions (M,k) is add-closed ) by Lm2; end; Lm3: for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real holds ( RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is Abelian & RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is add-associative & RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is right_zeroed & RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is vector-distributive & RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is scalar-distributive & RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is scalar-associative & RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is scalar-unital ) proofend; registration let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; cluster RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) -> Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is Abelian & RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is add-associative & RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is right_zeroed & RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is vector-distributive & RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is scalar-distributive & RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is scalar-associative & RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is scalar-unital ) by Lm3; end; definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; func RLSp_LpFunct (M,k) -> non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct equals :: LPSPACE2:def 3 RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #); coherence RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #) is non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; end; :: deftheorem defines RLSp_LpFunct LPSPACE2:def_3_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real holds RLSp_LpFunct (M,k) = RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #); begin theorem Th29: :: LPSPACE2:29 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,REAL for k being positive Real for v, u being VECTOR of (RLSp_LpFunct (M,k)) st f = v & g = u holds f + g = v + u proofend; theorem Th30: :: LPSPACE2:30 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for a being Real for k being positive Real for u being VECTOR of (RLSp_LpFunct (M,k)) st f = u holds a (#) f = a * u proofend; theorem Th31: :: LPSPACE2:31 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for k being positive Real for u being VECTOR of (RLSp_LpFunct (M,k)) st f = u holds ( u + ((- 1) * u) = (X --> 0) | (dom f) & ex v, g being PartFunc of X,REAL st ( v in Lp_Functions (M,k) & g in Lp_Functions (M,k) & v = u + ((- 1) * u) & g = X --> 0 & v a.e.= g,M ) ) proofend; definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; func AlmostZeroLpFunctions (M,k) -> non empty Subset of (RLSp_LpFunct (M,k)) equals :: LPSPACE2:def 4 { f where f is PartFunc of X,REAL : ( f in Lp_Functions (M,k) & f a.e.= X --> 0,M ) } ; coherence { f where f is PartFunc of X,REAL : ( f in Lp_Functions (M,k) & f a.e.= X --> 0,M ) } is non empty Subset of (RLSp_LpFunct (M,k)) proofend; end; :: deftheorem defines AlmostZeroLpFunctions LPSPACE2:def_4_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real holds AlmostZeroLpFunctions (M,k) = { f where f is PartFunc of X,REAL : ( f in Lp_Functions (M,k) & f a.e.= X --> 0,M ) } ; Lm4: for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real holds ( AlmostZeroLpFunctions (M,k) is add-closed & AlmostZeroLpFunctions (M,k) is multi-closed ) proofend; registration let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; cluster AlmostZeroLpFunctions (M,k) -> non empty add-closed multi-closed ; coherence ( AlmostZeroLpFunctions (M,k) is add-closed & AlmostZeroLpFunctions (M,k) is multi-closed ) by Lm4; end; theorem Th32: :: LPSPACE2:32 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real holds ( 0. (RLSp_LpFunct (M,k)) = X --> 0 & 0. (RLSp_LpFunct (M,k)) in AlmostZeroLpFunctions (M,k) ) proofend; definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; func RLSp_AlmostZeroLpFunct (M,k) -> non empty RLSStruct equals :: LPSPACE2:def 5 RLSStruct(# (AlmostZeroLpFunctions (M,k)),(In ((0. (RLSp_LpFunct (M,k))),(AlmostZeroLpFunctions (M,k)))),(add| ((AlmostZeroLpFunctions (M,k)),(RLSp_LpFunct (M,k)))),(Mult_ (AlmostZeroLpFunctions (M,k))) #); coherence RLSStruct(# (AlmostZeroLpFunctions (M,k)),(In ((0. (RLSp_LpFunct (M,k))),(AlmostZeroLpFunctions (M,k)))),(add| ((AlmostZeroLpFunctions (M,k)),(RLSp_LpFunct (M,k)))),(Mult_ (AlmostZeroLpFunctions (M,k))) #) is non empty RLSStruct ; end; :: deftheorem defines RLSp_AlmostZeroLpFunct LPSPACE2:def_5_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real holds RLSp_AlmostZeroLpFunct (M,k) = RLSStruct(# (AlmostZeroLpFunctions (M,k)),(In ((0. (RLSp_LpFunct (M,k))),(AlmostZeroLpFunctions (M,k)))),(add| ((AlmostZeroLpFunctions (M,k)),(RLSp_LpFunct (M,k)))),(Mult_ (AlmostZeroLpFunctions (M,k))) #); registration let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; cluster RLSp_LpFunct (M,k) -> non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( RLSp_LpFunct (M,k) is strict & RLSp_LpFunct (M,k) is Abelian & RLSp_LpFunct (M,k) is add-associative & RLSp_LpFunct (M,k) is right_zeroed & RLSp_LpFunct (M,k) is vector-distributive & RLSp_LpFunct (M,k) is scalar-distributive & RLSp_LpFunct (M,k) is scalar-associative & RLSp_LpFunct (M,k) is scalar-unital ) ; end; theorem :: LPSPACE2:33 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,REAL for k being positive Real for v, u being VECTOR of (RLSp_AlmostZeroLpFunct (M,k)) st f = v & g = u holds f + g = v + u proofend; theorem :: LPSPACE2:34 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for a being Real for k being positive Real for u being VECTOR of (RLSp_AlmostZeroLpFunct (M,k)) st f = u holds a (#) f = a * u proofend; definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let f be PartFunc of X,REAL; let k be positive Real; func a.e-eq-class_Lp (f,M,k) -> Subset of (Lp_Functions (M,k)) equals :: LPSPACE2:def 6 { h where h is PartFunc of X,REAL : ( h in Lp_Functions (M,k) & f a.e.= h,M ) } ; correctness coherence { h where h is PartFunc of X,REAL : ( h in Lp_Functions (M,k) & f a.e.= h,M ) } is Subset of (Lp_Functions (M,k)); proofend; end; :: deftheorem defines a.e-eq-class_Lp LPSPACE2:def_6_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for k being positive Real holds a.e-eq-class_Lp (f,M,k) = { h where h is PartFunc of X,REAL : ( h in Lp_Functions (M,k) & f a.e.= h,M ) } ; theorem Th35: :: LPSPACE2:35 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for k being positive Real st f in Lp_Functions (M,k) holds ex E being Element of S st ( M . (E `) = 0 & dom f = E & f is_measurable_on E ) proofend; theorem Th36: :: LPSPACE2:36 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for g, f being PartFunc of X,REAL for k being positive Real st g in Lp_Functions (M,k) & g a.e.= f,M holds g in a.e-eq-class_Lp (f,M,k) proofend; theorem Th37: :: LPSPACE2:37 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,REAL for k being positive Real st ex E being Element of S st ( M . (E `) = 0 & E = dom f & f is_measurable_on E ) & g in a.e-eq-class_Lp (f,M,k) holds ( g a.e.= f,M & f in Lp_Functions (M,k) ) proofend; theorem Th38: :: LPSPACE2:38 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for k being positive Real st f in Lp_Functions (M,k) holds f in a.e-eq-class_Lp (f,M,k) proofend; theorem Th39: :: LPSPACE2:39 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for g, f being PartFunc of X,REAL for k being positive Real st ex E being Element of S st ( M . (E `) = 0 & E = dom g & g is_measurable_on E ) & a.e-eq-class_Lp (f,M,k) <> {} & a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) holds f a.e.= g,M proofend; theorem :: LPSPACE2:40 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,REAL for k being positive Real st f in Lp_Functions (M,k) & ex E being Element of S st ( M . (E `) = 0 & E = dom g & g is_measurable_on E ) & a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) holds f a.e.= g,M proofend; theorem Th41: :: LPSPACE2:41 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,REAL for k being positive Real st f a.e.= g,M holds a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) proofend; theorem Th42: :: LPSPACE2:42 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,REAL for k being positive Real st f a.e.= g,M holds a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) by Th41; theorem :: LPSPACE2:43 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,REAL for k being positive Real st f in Lp_Functions (M,k) & g in a.e-eq-class_Lp (f,M,k) holds a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) proofend; theorem :: LPSPACE2:44 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f, f1, g, g1 being PartFunc of X,REAL for k being positive Real st ex E being Element of S st ( M . (E `) = 0 & E = dom f & f is_measurable_on E ) & ex E being Element of S st ( M . (E `) = 0 & E = dom f1 & f1 is_measurable_on E ) & ex E being Element of S st ( M . (E `) = 0 & E = dom g & g is_measurable_on E ) & ex E being Element of S st ( M . (E `) = 0 & E = dom g1 & g1 is_measurable_on E ) & not a.e-eq-class_Lp (f,M,k) is empty & not a.e-eq-class_Lp (g,M,k) is empty & a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (f1,M,k) & a.e-eq-class_Lp (g,M,k) = a.e-eq-class_Lp (g1,M,k) holds a.e-eq-class_Lp ((f + g),M,k) = a.e-eq-class_Lp ((f1 + g1),M,k) proofend; theorem Th45: :: LPSPACE2:45 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f, f1, g, g1 being PartFunc of X,REAL for k being positive Real st f in Lp_Functions (M,k) & f1 in Lp_Functions (M,k) & g in Lp_Functions (M,k) & g1 in Lp_Functions (M,k) & a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (f1,M,k) & a.e-eq-class_Lp (g,M,k) = a.e-eq-class_Lp (g1,M,k) holds a.e-eq-class_Lp ((f + g),M,k) = a.e-eq-class_Lp ((f1 + g1),M,k) proofend; theorem :: LPSPACE2:46 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,REAL for a being Real for k being positive Real st ex E being Element of S st ( M . (E `) = 0 & dom f = E & f is_measurable_on E ) & ex E being Element of S st ( M . (E `) = 0 & dom g = E & g is_measurable_on E ) & not a.e-eq-class_Lp (f,M,k) is empty & a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) holds a.e-eq-class_Lp ((a (#) f),M,k) = a.e-eq-class_Lp ((a (#) g),M,k) proofend; theorem Th47: :: LPSPACE2:47 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,REAL for a being Real for k being positive Real st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) & a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) holds a.e-eq-class_Lp ((a (#) f),M,k) = a.e-eq-class_Lp ((a (#) g),M,k) proofend; definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; func CosetSet (M,k) -> non empty Subset-Family of (Lp_Functions (M,k)) equals :: LPSPACE2:def 7 { (a.e-eq-class_Lp (f,M,k)) where f is PartFunc of X,REAL : f in Lp_Functions (M,k) } ; correctness coherence { (a.e-eq-class_Lp (f,M,k)) where f is PartFunc of X,REAL : f in Lp_Functions (M,k) } is non empty Subset-Family of (Lp_Functions (M,k)); proofend; end; :: deftheorem defines CosetSet LPSPACE2:def_7_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real holds CosetSet (M,k) = { (a.e-eq-class_Lp (f,M,k)) where f is PartFunc of X,REAL : f in Lp_Functions (M,k) } ; definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; func addCoset (M,k) -> BinOp of (CosetSet (M,k)) means :Def8: :: LPSPACE2:def 8 for A, B being Element of CosetSet (M,k) for a, b being PartFunc of X,REAL st a in A & b in B holds it . (A,B) = a.e-eq-class_Lp ((a + b),M,k); existence ex b1 being BinOp of (CosetSet (M,k)) st for A, B being Element of CosetSet (M,k) for a, b being PartFunc of X,REAL st a in A & b in B holds b1 . (A,B) = a.e-eq-class_Lp ((a + b),M,k) proofend; uniqueness for b1, b2 being BinOp of (CosetSet (M,k)) st ( for A, B being Element of CosetSet (M,k) for a, b being PartFunc of X,REAL st a in A & b in B holds b1 . (A,B) = a.e-eq-class_Lp ((a + b),M,k) ) & ( for A, B being Element of CosetSet (M,k) for a, b being PartFunc of X,REAL st a in A & b in B holds b2 . (A,B) = a.e-eq-class_Lp ((a + b),M,k) ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines addCoset LPSPACE2:def_8_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real for b5 being BinOp of (CosetSet (M,k)) holds ( b5 = addCoset (M,k) iff for A, B being Element of CosetSet (M,k) for a, b being PartFunc of X,REAL st a in A & b in B holds b5 . (A,B) = a.e-eq-class_Lp ((a + b),M,k) ); definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; func zeroCoset (M,k) -> Element of CosetSet (M,k) equals :: LPSPACE2:def 9 a.e-eq-class_Lp ((X --> 0),M,k); correctness coherence a.e-eq-class_Lp ((X --> 0),M,k) is Element of CosetSet (M,k); proofend; end; :: deftheorem defines zeroCoset LPSPACE2:def_9_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real holds zeroCoset (M,k) = a.e-eq-class_Lp ((X --> 0),M,k); definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; func lmultCoset (M,k) -> Function of [:REAL,(CosetSet (M,k)):],(CosetSet (M,k)) means :Def10: :: LPSPACE2:def 10 for z being Element of REAL for A being Element of CosetSet (M,k) for f being PartFunc of X,REAL st f in A holds it . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k); existence ex b1 being Function of [:REAL,(CosetSet (M,k)):],(CosetSet (M,k)) st for z being Element of REAL for A being Element of CosetSet (M,k) for f being PartFunc of X,REAL st f in A holds b1 . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k) proofend; uniqueness for b1, b2 being Function of [:REAL,(CosetSet (M,k)):],(CosetSet (M,k)) st ( for z being Element of REAL for A being Element of CosetSet (M,k) for f being PartFunc of X,REAL st f in A holds b1 . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k) ) & ( for z being Element of REAL for A being Element of CosetSet (M,k) for f being PartFunc of X,REAL st f in A holds b2 . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k) ) holds b1 = b2 proofend; end; :: deftheorem Def10 defines lmultCoset LPSPACE2:def_10_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real for b5 being Function of [:REAL,(CosetSet (M,k)):],(CosetSet (M,k)) holds ( b5 = lmultCoset (M,k) iff for z being Element of REAL for A being Element of CosetSet (M,k) for f being PartFunc of X,REAL st f in A holds b5 . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k) ); definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; func Pre-Lp-Space (M,k) -> strict RLSStruct means :Def11: :: LPSPACE2:def 11 ( the carrier of it = CosetSet (M,k) & the addF of it = addCoset (M,k) & 0. it = zeroCoset (M,k) & the Mult of it = lmultCoset (M,k) ); existence ex b1 being strict RLSStruct st ( the carrier of b1 = CosetSet (M,k) & the addF of b1 = addCoset (M,k) & 0. b1 = zeroCoset (M,k) & the Mult of b1 = lmultCoset (M,k) ) proofend; uniqueness for b1, b2 being strict RLSStruct st the carrier of b1 = CosetSet (M,k) & the addF of b1 = addCoset (M,k) & 0. b1 = zeroCoset (M,k) & the Mult of b1 = lmultCoset (M,k) & the carrier of b2 = CosetSet (M,k) & the addF of b2 = addCoset (M,k) & 0. b2 = zeroCoset (M,k) & the Mult of b2 = lmultCoset (M,k) holds b1 = b2 ; end; :: deftheorem Def11 defines Pre-Lp-Space LPSPACE2:def_11_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real for b5 being strict RLSStruct holds ( b5 = Pre-Lp-Space (M,k) iff ( the carrier of b5 = CosetSet (M,k) & the addF of b5 = addCoset (M,k) & 0. b5 = zeroCoset (M,k) & the Mult of b5 = lmultCoset (M,k) ) ); registration let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; cluster Pre-Lp-Space (M,k) -> non empty strict ; coherence not Pre-Lp-Space (M,k) is empty proofend; end; registration let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; cluster Pre-Lp-Space (M,k) -> right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( Pre-Lp-Space (M,k) is Abelian & Pre-Lp-Space (M,k) is add-associative & Pre-Lp-Space (M,k) is right_zeroed & Pre-Lp-Space (M,k) is right_complementable & Pre-Lp-Space (M,k) is vector-distributive & Pre-Lp-Space (M,k) is scalar-distributive & Pre-Lp-Space (M,k) is scalar-associative & Pre-Lp-Space (M,k) is scalar-unital ) proofend; end; begin theorem Th48: :: LPSPACE2:48 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,REAL for k being positive Real st f in Lp_Functions (M,k) & g in Lp_Functions (M,k) & f a.e.= g,M holds Integral (M,((abs f) to_power k)) = Integral (M,((abs g) to_power k)) proofend; theorem Th49: :: LPSPACE2:49 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for k being positive Real st f in Lp_Functions (M,k) holds ( Integral (M,((abs f) to_power k)) in REAL & 0 <= Integral (M,((abs f) to_power k)) ) proofend; theorem Th50: :: LPSPACE2:50 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,REAL for k being positive Real st ex x being VECTOR of (Pre-Lp-Space (M,k)) st ( f in x & g in x ) holds ( f a.e.= g,M & f in Lp_Functions (M,k) & g in Lp_Functions (M,k) ) proofend; theorem Th51: :: LPSPACE2:51 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for k being positive Real for x being Point of (Pre-Lp-Space (M,k)) st f in x holds ( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) ) proofend; theorem Th52: :: LPSPACE2:52 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,REAL for k being positive Real for x being Point of (Pre-Lp-Space (M,k)) st f in x & g in x holds ( f a.e.= g,M & Integral (M,((abs f) to_power k)) = Integral (M,((abs g) to_power k)) ) proofend; definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; func Lp-Norm (M,k) -> Function of the carrier of (Pre-Lp-Space (M,k)),REAL means :Def12: :: LPSPACE2:def 12 for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st ( f in x & ex r being Real st ( r = Integral (M,((abs f) to_power k)) & it . x = r to_power (1 / k) ) ); existence ex b1 being Function of the carrier of (Pre-Lp-Space (M,k)),REAL st for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st ( f in x & ex r being Real st ( r = Integral (M,((abs f) to_power k)) & b1 . x = r to_power (1 / k) ) ) proofend; uniqueness for b1, b2 being Function of the carrier of (Pre-Lp-Space (M,k)),REAL st ( for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st ( f in x & ex r being Real st ( r = Integral (M,((abs f) to_power k)) & b1 . x = r to_power (1 / k) ) ) ) & ( for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st ( f in x & ex r being Real st ( r = Integral (M,((abs f) to_power k)) & b2 . x = r to_power (1 / k) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def12 defines Lp-Norm LPSPACE2:def_12_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real for b5 being Function of the carrier of (Pre-Lp-Space (M,k)),REAL holds ( b5 = Lp-Norm (M,k) iff for x being Point of (Pre-Lp-Space (M,k)) ex f being PartFunc of X,REAL st ( f in x & ex r being Real st ( r = Integral (M,((abs f) to_power k)) & b5 . x = r to_power (1 / k) ) ) ); definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be positive Real; func Lp-Space (M,k) -> non empty NORMSTR equals :: LPSPACE2:def 13 NORMSTR(# the carrier of (Pre-Lp-Space (M,k)), the ZeroF of (Pre-Lp-Space (M,k)), the addF of (Pre-Lp-Space (M,k)), the Mult of (Pre-Lp-Space (M,k)),(Lp-Norm (M,k)) #); coherence NORMSTR(# the carrier of (Pre-Lp-Space (M,k)), the ZeroF of (Pre-Lp-Space (M,k)), the addF of (Pre-Lp-Space (M,k)), the Mult of (Pre-Lp-Space (M,k)),(Lp-Norm (M,k)) #) is non empty NORMSTR ; end; :: deftheorem defines Lp-Space LPSPACE2:def_13_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real holds Lp-Space (M,k) = NORMSTR(# the carrier of (Pre-Lp-Space (M,k)), the ZeroF of (Pre-Lp-Space (M,k)), the addF of (Pre-Lp-Space (M,k)), the Mult of (Pre-Lp-Space (M,k)),(Lp-Norm (M,k)) #); theorem Th53: :: LPSPACE2:53 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real for x being Point of (Lp-Space (M,k)) holds ( ex f being PartFunc of X,REAL st ( f in Lp_Functions (M,k) & x = a.e-eq-class_Lp (f,M,k) ) & ( for f being PartFunc of X,REAL st f in x holds ex r being Real st ( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) ) proofend; theorem Th54: :: LPSPACE2:54 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,REAL for a being Real for k being positive Real for x, y being Point of (Lp-Space (M,k)) holds ( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) ) proofend; theorem Th55: :: LPSPACE2:55 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for k being positive Real for x being Point of (Lp-Space (M,k)) st f in x holds ( x = a.e-eq-class_Lp (f,M,k) & ex r being Real st ( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) proofend; theorem Th56: :: LPSPACE2:56 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S holds X --> 0 in L1_Functions M proofend; theorem Th57: :: LPSPACE2:57 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for k being positive Real st f in Lp_Functions (M,k) & Integral (M,((abs f) to_power k)) = 0 holds f a.e.= X --> 0,M proofend; theorem Th58: :: LPSPACE2:58 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real holds Integral (M,((abs (X --> 0)) to_power k)) = 0 proofend; :: lemma for Holder theorem Th59: :: LPSPACE2:59 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,REAL for m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions (M,m) & g in Lp_Functions (M,n) holds ( f (#) g in L1_Functions M & f (#) g is_integrable_on M ) proofend; :: Holder theorem Th60: :: LPSPACE2:60 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,REAL for m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions (M,m) & g in Lp_Functions (M,n) holds ex r1 being Real st ( r1 = Integral (M,((abs f) to_power m)) & ex r2 being Real st ( r2 = Integral (M,((abs g) to_power n)) & Integral (M,(abs (f (#) g))) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) ) proofend; Lm5: 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,REAL for m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions (M,m) & g in Lp_Functions (M,m) holds ex r1, r2, r3 being Real st ( r1 = Integral (M,((abs f) to_power m)) & r2 = Integral (M,((abs g) to_power m)) & r3 = Integral (M,((abs (f + g)) to_power m)) & r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) ) proofend; :: Minkowski theorem Th61: :: LPSPACE2:61 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,REAL for m being positive Real for r1, r2, r3 being Element of REAL st 1 <= m & f in Lp_Functions (M,m) & g in Lp_Functions (M,m) & r1 = Integral (M,((abs f) to_power m)) & r2 = Integral (M,((abs g) to_power m)) & r3 = Integral (M,((abs (f + g)) to_power m)) holds r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m)) proofend; Lm6: for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being geq_than_1 Real holds ( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable ) proofend; registration let k be geq_than_1 Real; let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; cluster Lp-Space (M,k) -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ; coherence ( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable ) by Lm6; end; begin theorem Th62: :: LPSPACE2:62 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real for Sq being sequence of (Lp-Space (M,k)) ex Fsq being Functional_Sequence of X,REAL st for n being Element of NAT holds ( Fsq . n in Lp_Functions (M,k) & Fsq . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq . n),M,k) & ex r being Real st ( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) ) proofend; theorem Th63: :: LPSPACE2:63 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real for Sq being sequence of (Lp-Space (M,k)) ex Fsq being with_the_same_dom Functional_Sequence of X,REAL st for n being Element of NAT holds ( Fsq . n in Lp_Functions (M,k) & Fsq . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq . n),M,k) & ex r being Real st ( 0 <= r & r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) ) proofend; Lm7: for X being RealNormSpace for Sq being sequence of X for Sq0 being Point of X for R1 being Real_Sequence for N being V167() sequence of NAT st Sq is Cauchy_sequence_by_Norm & ( for i being Nat holds R1 . i = ||.(Sq0 - (Sq . (N . i))).|| ) & R1 is convergent & lim R1 = 0 holds ( Sq is convergent & lim Sq = Sq0 & ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 ) proofend; theorem :: LPSPACE2:64 for X being RealNormSpace for Sq being sequence of X for Sq0 being Point of X st ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 holds ( Sq is convergent & lim Sq = Sq0 ) proofend; theorem Th65: :: LPSPACE2:65 for X being RealNormSpace for Sq being sequence of X st Sq is Cauchy_sequence_by_Norm holds ex N being V167() sequence of NAT st for i, j being Element of NAT st j >= N . i holds ||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i) proofend; theorem Th66: :: LPSPACE2:66 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being positive Real for F being Functional_Sequence of X,REAL st ( for m being Nat holds F . m in Lp_Functions (M,k) ) holds for m being Nat holds (Partial_Sums F) . m in Lp_Functions (M,k) proofend; theorem Th67: :: LPSPACE2:67 for X being non empty set for F being Functional_Sequence of X,REAL st ( for m being Nat holds F . m is nonnegative ) holds for m being Nat holds (Partial_Sums F) . m is nonnegative proofend; theorem Th68: :: LPSPACE2:68 for X being non empty set for F being Functional_Sequence of X,REAL for x being Element of X for n, m being Nat st F is with_the_same_dom & x in dom (F . 0) & ( for k being Nat holds F . k is nonnegative ) & n <= m holds ((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x proofend; theorem Th69: :: LPSPACE2:69 for X being non empty set for F being Functional_Sequence of X,REAL st F is with_the_same_dom holds abs F is with_the_same_dom proofend; theorem Th70: :: LPSPACE2:70 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for k being geq_than_1 Real for Sq being sequence of (Lp-Space (M,k)) st Sq is Cauchy_sequence_by_Norm holds Sq is convergent proofend; registration let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let k be geq_than_1 Real; cluster Lp-Space (M,k) -> non empty complete ; coherence Lp-Space (M,k) is complete proofend; end; begin Lm8: for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL st f in L1_Functions M holds ( f is_integrable_on M & ex E being Element of S st ( M . (E `) = 0 & E = dom f & f is_measurable_on E ) ) proofend; Lm9: for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL for k being positive Real st f in Lp_Functions (M,k) holds (abs f) to_power k is_integrable_on M proofend; Lm10: for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL st ex E being Element of S st ( M . (E `) = 0 & E = dom f & f is_measurable_on E ) holds a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M) proofend; Lm11: for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL holds a.e-eq-class (f,M) c= a.e-eq-class_Lp (f,M,1) proofend; Lm12: for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,REAL st ex E being Element of S st ( M . (E `) = 0 & E = dom f & f is_measurable_on E ) holds a.e-eq-class_Lp (f,M,1) = a.e-eq-class (f,M) proofend; theorem Th71: :: LPSPACE2:71 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S holds CosetSet M = CosetSet (M,1) proofend; theorem Th72: :: LPSPACE2:72 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S holds addCoset M = addCoset (M,1) proofend; theorem Th73: :: LPSPACE2:73 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S holds zeroCoset M = zeroCoset (M,1) proofend; theorem Th74: :: LPSPACE2:74 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S holds lmultCoset M = lmultCoset (M,1) proofend; theorem Th75: :: LPSPACE2:75 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S holds Pre-L-Space M = Pre-Lp-Space (M,1) proofend; theorem Th76: :: LPSPACE2:76 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S holds L-1-Norm M = Lp-Norm (M,1) proofend; theorem :: LPSPACE2:77 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S holds L-1-Space M = Lp-Space (M,1) proofend;