:: 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-2021 Association of Mizar Users


theorem Th1: :: LPSPACE2:1
for m, n being positive Real st (1 / m) + (1 / n) = 1 holds
m > 1
proof end;

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 A -measurable & f is nonnegative holds
( Integral (M,f) in REAL iff f is_integrable_on M )
proof end;

definition
let r be Real;
attr r 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 holds
( r is geq_than_1 iff 1 <= r );

registration
cluster V97() geq_than_1 -> positive for object ;
coherence
for b1 being Real st b1 is geq_than_1 holds
b1 is positive
;
end;

reconsider jj = 1 as Real ;

registration
cluster ext-real complex V97() geq_than_1 for object ;
existence
ex b1 being Real st b1 is geq_than_1
by Def1;
end;

registration
cluster ext-real complex V97() geq_than_1 for object ;
existence
ex b1 being Real st b1 is geq_than_1
by Def1;
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
proof end;

theorem Th4: :: LPSPACE2:4
for a, b being Real st a >= 0 & b > 0 holds
a to_power b >= 0
proof end;

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

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

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

theorem Th8: :: LPSPACE2:8
for X being non empty set
for f being PartFunc of X,REAL holds f to_power 1 = f
proof end;

theorem Th9: :: LPSPACE2:9
for seq1, seq2 being Real_Sequence
for k being positive Real st ( for n being Nat holds
( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ) holds
( seq1 is convergent iff seq2 is convergent )
proof end;

theorem Th10: :: LPSPACE2:10
for seq being Real_Sequence
for n, m being Nat st m <= n holds
( |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) & |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= (Partial_Sums (abs seq)) . n )
proof end;

theorem Th11: :: LPSPACE2:11
for seq, seq2 being Real_Sequence
for k being positive Real st seq is convergent & ( for n being Nat holds seq2 . n = |.((lim seq) - (seq . n)).| to_power k ) holds
( seq2 is convergent & lim seq2 = 0 )
proof end;

Lm1: for seq being Real_Sequence
for n being Nat holds |.((Partial_Sums seq) . n).| <= (Partial_Sums (abs seq)) . n

by NAGATA_2:13;

theorem Th12: :: LPSPACE2:12
for k being positive Real
for X being non empty set holds (X --> 0) to_power k = X --> 0
proof end;

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

registration
let X be non empty set ;
let f be PartFunc of X,REAL;
cluster |.f.| -> nonnegative ;
coherence
abs f is nonnegative
proof end;
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
proof end;

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 )
proof 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 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 Ef -measurable & (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 Ef -measurable & (abs f) to_power k is_integrable_on M )
}
is non empty Subset of (RLSp_PFunct X)
;
proof end;
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 Ef -measurable & (abs f) to_power k is_integrable_on M )
}
;

theorem Th16: :: LPSPACE2:16
for a, b, k being Real st k > 0 holds
( |.(a + b).| to_power k <= (|.a.| + |.b.|) to_power k & (|.a.| + |.b.|) to_power k <= (2 * (max (|.a.|,|.b.|))) to_power k & |.(a + b).| to_power k <= (2 * (max (|.a.|,|.b.|))) to_power k )
proof end;

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

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
(|.a.| to_power b) (#) ((abs f) to_power b) = (abs (a (#) f)) to_power b
proof end;

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

theorem Th20: :: LPSPACE2:20
for X being non empty set
for f being PartFunc of X,REAL
for k being Real
for E being set holds (f | E) to_power k = (f to_power k) | E
proof end;

theorem Th21: :: LPSPACE2:21
for a, b, k being Real st k > 0 holds
|.(a + b).| to_power k <= (2 to_power k) * ((|.a.| to_power k) + (|.b.| to_power k))
proof end;

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

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

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

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

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

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

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

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 )

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

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

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

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

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

proof 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 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 :: 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) )
proof 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_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
proof end;

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

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))
;
proof end;
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 E -measurable )
proof end;

theorem Th36: :: LPSPACE2:36
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 g in Lp_Functions (M,k) & g a.e.= f,M holds
g in a.e-eq-class_Lp (f,M,k)
proof end;

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 E -measurable ) & g in a.e-eq-class_Lp (f,M,k) holds
( g a.e.= f,M & f in Lp_Functions (M,k) )
proof end;

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

theorem Th39: :: LPSPACE2:39
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 g & g is E -measurable ) & 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
proof end;

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 E -measurable ) & a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) holds
f a.e.= g,M
proof end;

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

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

theorem :: LPSPACE2:44
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g, f1, 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 E -measurable ) & ex E being Element of S st
( M . (E `) = 0 & E = dom f1 & f1 is E -measurable ) & ex E being Element of S st
( M . (E `) = 0 & E = dom g & g is E -measurable ) & ex E being Element of S st
( M . (E `) = 0 & E = dom g1 & g1 is E -measurable ) & 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)
proof end;

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, g, f1, 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)
proof end;

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 E -measurable ) & ex E being Element of S st
( M . (E `) = 0 & dom g = E & g is E -measurable ) & 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)
proof end;

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)
proof 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 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))
;
proof end;
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)
proof end;
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
proof end;
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)
;
proof end;
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 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 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)
proof end;
uniqueness
for b1, b2 being Function of [:REAL,(CosetSet (M,k)):],(CosetSet (M,k)) st ( for z being 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 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
proof end;
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 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) )
proof end;
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
proof end;
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 )
proof end;
end;

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

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

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

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

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

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

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

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

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

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

:: 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 )
proof end;

:: 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)) ) )
proof end;

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

proof end;

:: 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 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))
proof end;

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 )

proof end;

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;

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

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

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

proof end;

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

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 V174() sequence of NAT st
for i, j being Nat st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i)
proof end;

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

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

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

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

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

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

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

proof end;

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

proof end;

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 E -measurable ) holds
a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)

proof end;

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)

proof end;

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 E -measurable ) holds
a.e-eq-class_Lp (f,M,1) = a.e-eq-class (f,M)

by Lm10, Lm11;

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

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

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

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

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

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

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