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