LPSPACE2: On $L^p$ Space Formed by Real-valued Partial Functions

proof end;

end;

registration

cluster ext-real V38() real geq_than_1 for Element of REAL ;

proof end;

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 Element of 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 Element of NAT st m <= n holds
( abs (((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)) <= ((Partial_Sums (abs seq)) . n) - ((Partial_Sums (abs seq)) . m) & abs (((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)) <= (Partial_Sums (abs seq)) . n )

proof end;

theorem Th11: :: LPSPACE2:11

for seq, seq2 being Real_Sequence
for k being positive Real st seq is convergent & ( for n being Element of NAT holds seq2 . n = |.((lim seq) - (seq . n)).| to_power k ) holds
( seq2 is convergent & lim seq2 = 0 )

proof end;

Lm1: for seq being Real_Sequence
for n being Element of NAT holds abs ((Partial_Sums seq) . n) <= (Partial_Sums (abs seq)) . n
by NAGATA_2:13;

begin

theorem Th12: :: LPSPACE2:12

for k being positive Real
for X being non empty set holds (X --> 0) to_power k = X --> 0

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 ;

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_measurable_on Ef & (abs f) to_power k is_integrable_on M ) } ;

proof end;

end;

:: deftheorem defines Lp_Functions LPSPACE2:def 2 :

theorem Th16: :: LPSPACE2:16

for a, b, k being Real st k > 0 holds
( (abs (a + b)) to_power k <= ((abs a) + (abs b)) to_power k & ((abs a) + (abs b)) to_power k <= (2 * (max ((abs a),(abs b)))) to_power k & (abs (a + b)) to_power k <= (2 * (max ((abs a),(abs b)))) to_power k )

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
((abs 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 number
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
(abs (a + b)) to_power k <= (2 to_power k) * (((abs a) to_power k) + ((abs 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

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 by Lm2;

end;

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

end;

:: deftheorem defines RLSp_LpFunct LPSPACE2:def 3 :

begin

theorem Th29: :: LPSPACE2:29

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for k being positive Real
for v, u being VECTOR of (RLSp_LpFunct (M,k)) st f = v & g = u holds
f + g = v + u

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

proof end;

end;

:: deftheorem defines AlmostZeroLpFunctions LPSPACE2:def 4 :

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 by Lm4;

end;

theorem Th32: :: LPSPACE2:32

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real holds
( 0. (RLSp_LpFunct (M,k)) = X --> 0 & 0. (RLSp_LpFunct (M,k)) in AlmostZeroLpFunctions (M,k) )

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

end;

:: deftheorem defines RLSp_AlmostZeroLpFunct LPSPACE2:def 5 :

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 ;

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

proof end;

end;

:: deftheorem defines a.e-eq-class_Lp LPSPACE2:def 6 :

theorem Th35: :: LPSPACE2:35

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for k being positive Real st f in Lp_Functions (M,k) holds
ex E being Element of S st
( M . (E `) = 0 & dom f = E & f is_measurable_on E )

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 g, f being PartFunc of X,REAL
for k being positive Real st g in Lp_Functions (M,k) & g a.e.= f,M holds
g in a.e-eq-class_Lp (f,M,k)

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

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 g, f being PartFunc of X,REAL
for k being positive Real st ex E being Element of S st
( M . (E `) = 0 & E = dom g & g is_measurable_on E ) & a.e-eq-class_Lp (f,M,k) <> {} & a.e-eq-class_Lp (f,M,k) = a.e-eq-class_Lp (g,M,k) holds
f a.e.= g,M

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

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

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

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

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

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

proof end;

end;

:: deftheorem defines CosetSet LPSPACE2:def 7 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines addCoset LPSPACE2:def 8 :

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

proof end;

end;

:: deftheorem defines zeroCoset LPSPACE2:def 9 :

definition

let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let k be positive Real;

func lmultCoset (M,k) -> Function of [:REAL,(CosetSet (M,k)):],(CosetSet (M,k)) means :Def10: :: LPSPACE2:def 10
for z being Element of REAL
for A being Element of CosetSet (M,k)
for f being PartFunc of X,REAL st f in A holds
it . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k);

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines lmultCoset LPSPACE2:def 10 :

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

proof end;

uniqueness ;

end;

:: deftheorem Def11 defines Pre-Lp-Space LPSPACE2:def 11 :

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 ;

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 ;

proof end;

end;

begin

theorem Th48: :: LPSPACE2:48

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines Lp-Norm LPSPACE2:def 12 :

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

end;

:: deftheorem defines Lp-Space LPSPACE2:def 13 :

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

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 Element of REAL st 1 <= m & f in Lp_Functions (M,m) & g in Lp_Functions (M,m) & r1 = Integral (M,((abs f) to_power m)) & r2 = Integral (M,((abs g) to_power m)) & r3 = Integral (M,((abs (f + g)) to_power m)) holds
r3 to_power (1 / m) <= (r1 to_power (1 / m)) + (r2 to_power (1 / m))

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 by Lm6;

end;

begin

theorem Th62: :: LPSPACE2:62

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real
for Sq being sequence of (Lp-Space (M,k)) ex Fsq being Functional_Sequence of X,REAL st
for n being Element of NAT holds
( Fsq . n in Lp_Functions (M,k) & Fsq . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq . n),M,k) & ex r being Real st
( r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

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 Element of NAT holds
( Fsq . n in Lp_Functions (M,k) & Fsq . n in Sq . n & Sq . n = a.e-eq-class_Lp ((Fsq . n),M,k) & ex r being Real st
( 0 <= r & r = Integral (M,((abs (Fsq . n)) to_power k)) & ||.(Sq . n).|| = r to_power (1 / k) ) )

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 V167() sequence of NAT st Sq is Cauchy_sequence_by_Norm & ( for i being Nat holds R1 . i = ||.(Sq0 - (Sq . (N . i))).|| ) & R1 is convergent & lim R1 = 0 holds
( Sq is convergent & lim Sq = Sq0 & ||.(Sq - Sq0).|| is convergent & lim ||.(Sq - Sq0).|| = 0 )

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 V167() sequence of NAT st
for i, j being Element of NAT st j >= N . i holds
||.((Sq . j) - (Sq . (N . i))).|| < 2 to_power (- i)

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 ;