begin
theorem Lm300:
theorem MPreLm8:
:: deftheorem defH defines geq_than_1 LPSPACE2:def 1 :
for r being real number holds
( r is geq_than_1 iff 1 <= r );
theorem HOLDER13:
theorem LmPW001:
theorem LmPW003:
theorem LmPW004:
theorem LmPW005:
theorem LmPW006:
theorem LMSQ1:
theorem LMSQ4:
theorem LMSQ5:
LMSQ6:
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 Lm001:
theorem Lm001x:
theorem Lm002b:
theorem Lm2:
:: 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 Lm003:
theorem Lm004:
theorem Lm001e:
theorem Lm001f:
theorem Lm001g:
theorem Lm005:
theorem Lm007:
theorem LmDef1Lp:
theorem Lm008:
theorem Th01aLp:
theorem Th01bLp:
theorem Th01cLp:
theorem Th01dLp:
Th01Lp:
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 )
Th02Lp:
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 )
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 Th02Lp;
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
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 ThB10:
theorem ThB11:
theorem ThB11Z:
:: 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 ) } ;
Th09:
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 )
theorem Th09a:
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
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)) #);
theorem
theorem
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
{ 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);
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 EQC00a:
theorem EQC00b:
theorem EQC00c:
theorem EQC01:
theorem EQC02a:
theorem
theorem EQC02b:
theorem EQC02bx:
theorem
theorem
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
theorem EQC03b:
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
theorem
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
theorem EQC04b:
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
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
{ (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);
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 :
VSPDef3X:
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
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
end;
:: deftheorem VSPDef3X 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 );
:: 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 :
VSPDef5X:
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
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
end;
:: deftheorem VSPDef5X 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 :
VSPDef6X:
( 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 )
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 VSPDef6X 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 ) );
begin
theorem Th14:
theorem Lm15:
theorem Lm10:
theorem Th15:
theorem Lm16:
theorem Lm17:
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 :
DefLpNORM:
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) ) )
by Th15;
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
end;
:: deftheorem DefLpNORM 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
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 Lm17x:
theorem Lm17Y:
theorem Lm17z:
theorem LmDef1:
theorem Lm261:
theorem Lm262:
theorem Th001a:
theorem Th001:
Th002:
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)) )
theorem Th002X:
Th003:
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 )
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 Th003;
end;
begin
theorem Th004X:
theorem Th004:
LM005X:
for X being RealNormSpace
for Sq being sequence of X
for Sq0 being Point of X
for R1 being Real_Sequence
for N being V161() sequence of NAT st Sq is CCauchy & ( 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 )
theorem
theorem Th005:
theorem C935:
theorem C936:
theorem C937:
theorem C938:
theorem Th006:
begin
Lem00:
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 ) )
Lem00a:
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
Lem01:
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
Lem02:
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
Lem03:
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
theorem Th9a:
theorem Th9b:
theorem Th9c:
theorem Th9d:
theorem Th009:
theorem Th10a:
theorem