begin
theorem Th1:
theorem Th2:
:: deftheorem Def1 defines geq_than_1 LPSPACE2:def 1 :
for r being real number holds
( r is geq_than_1 iff 1 <= r );
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
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:
theorem Th13:
theorem Th14:
theorem Th15:
:: 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:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
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 )
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 )
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
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:
theorem Th30:
theorem Th31:
:: 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 )
theorem Th32:
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 Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem Th41:
theorem Th42:
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 Th45:
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 Th47:
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 :
Def8:
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 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) );
:: 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:
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 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:
( 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 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) ) );
begin
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
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:
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 Th51;
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 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
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 Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
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)) )
theorem Th62:
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 )
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 Th63:
theorem Th64:
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 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 Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
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 ) )
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
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)
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)
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)
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem