:: by Yasushige Watase , Noboru Endou and Yasunari Shidama

::

:: Received February 4, 2010

:: Copyright (c) 2010-2016 Association of Mizar Users

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_measurable_on A & f is nonnegative holds

( Integral (M,f) in REAL iff f is_integrable_on M )

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_measurable_on A & f is nonnegative holds

( Integral (M,f) in REAL iff f is_integrable_on M )

proof end;

:: deftheorem Def1 defines geq_than_1 LPSPACE2:def 1 :

for r being Real holds

( r is geq_than_1 iff 1 <= r );

for r being Real holds

( r is geq_than_1 iff 1 <= r );

reconsider jj = 1 as Real ;

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)

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

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)

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

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 )

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 )

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

for f being PartFunc of X,REAL

for D being set holds abs (f | D) = (abs f) | D

proof end;

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

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;

coherence

{ 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 ) } is non empty Subset of (RLSp_PFunct X);

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

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

coherence

{ 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 ) } is non empty Subset of (RLSp_PFunct X);

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

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

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

(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

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

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

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

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

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

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

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)

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)

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)

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)

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;

coherence

( Lp_Functions (M,k) is multi-closed & Lp_Functions (M,k) is add-closed ) by Lm2;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let k be positive Real;

coherence

( Lp_Functions (M,k) is multi-closed & Lp_Functions (M,k) is add-closed ) by Lm2;

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;

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

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;

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

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 ;

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

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

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

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

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;

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

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

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

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

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;

coherence

( AlmostZeroLpFunctions (M,k) is add-closed & AlmostZeroLpFunctions (M,k) is multi-closed ) by Lm4;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let k be positive Real;

coherence

( AlmostZeroLpFunctions (M,k) is add-closed & AlmostZeroLpFunctions (M,k) is multi-closed ) by Lm4;

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

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;

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

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 ;

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

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;

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

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

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

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;

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;
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 { h where h is PartFunc of X,REAL : ( h in Lp_Functions (M,k) & f a.e.= h,M ) } ;

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;

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

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

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

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

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)

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

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

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)

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;

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)

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

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

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

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)

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;

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;
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 { (a.e-eq-class_Lp (f,M,k)) where f is PartFunc of X,REAL : f in Lp_Functions (M,k) } ;

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;

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

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;

ex b_{1} 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

b_{1} . (A,B) = a.e-eq-class_Lp ((a + b),M,k)

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (A,B) = a.e-eq-class_Lp ((a + b),M,k) ) holds

b_{1} = b_{2}

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

ex b

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

b

proof end;

uniqueness for b

for a, b being PartFunc of X,REAL st a in A & b in B holds

b

for a, b being PartFunc of X,REAL st a in A & b in B holds

b

b

proof 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 b_{5} being BinOp of (CosetSet (M,k)) holds

( b_{5} = 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

b_{5} . (A,B) = a.e-eq-class_Lp ((a + b),M,k) );

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 b

( b

for a, b being PartFunc of X,REAL st a in A & b in B holds

b

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;

coherence

a.e-eq-class_Lp ((X --> 0),M,k) is Element of CosetSet (M,k);

end;
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 a.e-eq-class_Lp ((X --> 0),M,k);

coherence

a.e-eq-class_Lp ((X --> 0),M,k) is Element of CosetSet (M,k);

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

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;

ex b_{1} 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

b_{1} . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k)

for b_{1}, b_{2} 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

b_{1} . (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

b_{2} . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k) ) holds

b_{1} = b_{2}

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

ex b

for z being Real

for A being Element of CosetSet (M,k)

for f being PartFunc of X,REAL st f in A holds

b

proof end;

uniqueness for b

for A being Element of CosetSet (M,k)

for f being PartFunc of X,REAL st f in A holds

b

for A being Element of CosetSet (M,k)

for f being PartFunc of X,REAL st f in A holds

b

b

proof 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 b_{5} being Function of [:REAL,(CosetSet (M,k)):],(CosetSet (M,k)) holds

( b_{5} = 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

b_{5} . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k) );

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 b

( b

for A being Element of CosetSet (M,k)

for f being PartFunc of X,REAL st f in A holds

b

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;

ex b_{1} being strict RLSStruct st

( the carrier of b_{1} = CosetSet (M,k) & the addF of b_{1} = addCoset (M,k) & 0. b_{1} = zeroCoset (M,k) & the Mult of b_{1} = lmultCoset (M,k) )

for b_{1}, b_{2} being strict RLSStruct st the carrier of b_{1} = CosetSet (M,k) & the addF of b_{1} = addCoset (M,k) & 0. b_{1} = zeroCoset (M,k) & the Mult of b_{1} = lmultCoset (M,k) & the carrier of b_{2} = CosetSet (M,k) & the addF of b_{2} = addCoset (M,k) & 0. b_{2} = zeroCoset (M,k) & the Mult of b_{2} = lmultCoset (M,k) holds

b_{1} = b_{2}
;

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

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: 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 b_{5} being strict RLSStruct holds

( b_{5} = Pre-Lp-Space (M,k) iff ( the carrier of b_{5} = CosetSet (M,k) & the addF of b_{5} = addCoset (M,k) & 0. b_{5} = zeroCoset (M,k) & the Mult of b_{5} = lmultCoset (M,k) ) );

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 b

( b

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;

coherence

not Pre-Lp-Space (M,k) is empty

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let k be positive Real;

coherence

not Pre-Lp-Space (M,k) is empty

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;

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

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

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

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

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

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

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

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;

ex b_{1} 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)) & b_{1} . x = r to_power (1 / k) ) )

for b_{1}, b_{2} 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)) & b_{1} . 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)) & b_{2} . x = r to_power (1 / k) ) ) ) holds

b_{1} = b_{2}

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

ex b

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

proof end;

uniqueness for b

( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & b

( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & b

b

proof 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 b_{5} being Function of the carrier of (Pre-Lp-Space (M,k)),REAL holds

( b_{5} = 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)) & b_{5} . x = r to_power (1 / k) ) ) );

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 b

( b

( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & b

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;

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

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 ;

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

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

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

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

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

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

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

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 )

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

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

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;

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

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

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

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 )

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)

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)

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

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

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

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

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;

coherence

Lp-Space (M,k) is complete

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let k be geq_than_1 Real;

coherence

Lp-Space (M,k) is complete

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

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

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)

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)

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)

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)

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)

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)

for S being SigmaField of X

for M being sigma_Measure of S holds L-1-Space M = Lp-Space (M,1)

proof end;