:: On $L^1$ Space Formed by Real-valued Partial Functions
:: by Yasushige Watase , Noboru Endou and Yasunari Shidama
::
:: Received August 26, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

definition
let V be non empty RLSStruct ;
let V1 be Subset of V;
attrV1 is multi-closed  means :Def1: :: LPSPACE1:def 1
 for a being Real
for v being VECTOR of V st v in V1 holds
a * v in V1;
end;

:: deftheorem Def1 defines multi-closed LPSPACE1:def_1_:_
 for V being non empty RLSStruct
for V1 being Subset of V holds
( V1 is multi-closed iff for a being Real
for v being VECTOR of V st v in V1 holds
a * v in V1 );

theorem :: LPSPACE1:1
for V being RealLinearSpace
for V1 being Subset of V holds
( V1 is linearly-closed iff ( V1 is add-closed & V1 is multi-closed ) )
proofend;

registration
let V be non empty RLSStruct ;
cluster non empty add-closed multi-closed for Element of bool the carrier of V;
existence
 ex b1 being Subset of V st
( b1 is add-closed & b1 is multi-closed & not b1 is empty )
proofend;
end;

definition
let X be non empty RLSStruct ;
let X1 be non empty multi-closed Subset of X;
func Mult_ X1 ->  Function of [:REAL,X1:],X1 equals :: LPSPACE1:def 2
 the Mult of X | [:REAL,X1:];
correctness
coherence
the Mult of X | [:REAL,X1:] is Function of [:REAL,X1:],X1;
proofend;
end;

:: deftheorem  defines Mult_ LPSPACE1:def_2_:_
 for X being non empty RLSStruct
for X1 being non empty multi-closed Subset of X holds Mult_ X1 = the Mult of X | [:REAL,X1:];

theorem Th2: :: LPSPACE1:2
for V being non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for V1 being non empty Subset of V
for d1 being Element of V1
for A being BinOp of V1
for M being Function of [:REAL,V1:],V1 st d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] holds
( RLSStruct(# V1,d1,A,M #) is Abelian & RLSStruct(# V1,d1,A,M #) is add-associative & RLSStruct(# V1,d1,A,M #) is right_zeroed & RLSStruct(# V1,d1,A,M #) is vector-distributive & RLSStruct(# V1,d1,A,M #) is scalar-distributive & RLSStruct(# V1,d1,A,M #) is scalar-associative & RLSStruct(# V1,d1,A,M #) is scalar-unital )
proofend;

theorem Th3: :: LPSPACE1:3
for V being non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for V1 being non empty add-closed multi-closed Subset of V st 0. V in V1 holds
( RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is Abelian & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is add-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is right_zeroed & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is vector-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-distributive & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-associative & RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-unital )
proofend;

theorem Th4: :: LPSPACE1:4
for V being non empty RLSStruct
for V1 being non empty add-closed multi-closed Subset of V
for v, u being VECTOR of V
for w1, w2 being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w1 = v & w2 = u holds
w1 + w2 = v + u
proofend;

theorem Th5: :: LPSPACE1:5
for V being non empty RLSStruct
for V1 being non empty add-closed multi-closed Subset of V
for a being Real
for v being VECTOR of V
for w being VECTOR of RLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) st w = v holds
a * w = a * v
proofend;

begin

definition
let A, B be non empty set ;
let F be BinOp of (PFuncs (A,B));
let f, g be Element of PFuncs (A,B);
:: original:.
redefine funcF . (f,g) ->  Element of PFuncs (A,B);
coherence
 F . (f,g) is Element of PFuncs (A,B)
proofend;
end;

definition
let A be non empty set ;
func multpfunc A ->  BinOp of (PFuncs (A,REAL)) means :Def3: :: LPSPACE1:def 3
 for f, g being Element of PFuncs (A,REAL) holds it . (f,g) = f (#) g;
existence
 ex b1 being BinOp of (PFuncs (A,REAL)) st
for f, g being Element of PFuncs (A,REAL) holds b1 . (f,g) = f (#) g
proofend;
uniqueness
 for b1, b2 being BinOp of (PFuncs (A,REAL)) st ( for f, g being Element of PFuncs (A,REAL) holds b1 . (f,g) = f (#) g ) & ( for f, g being Element of PFuncs (A,REAL) holds b2 . (f,g) = f (#) g ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines multpfunc LPSPACE1:def_3_:_
 for A being non empty set
for b2 being BinOp of (PFuncs (A,REAL)) holds
( b2 = multpfunc A iff for f, g being Element of PFuncs (A,REAL) holds b2 . (f,g) = f (#) g );

definition
let A be non empty set ;
func multrealpfunc A ->  Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) means :Def4: :: LPSPACE1:def 4
 for a being Real
for f being Element of PFuncs (A,REAL) holds it . (a,f) = a (#) f;
existence
 ex b1 being Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) st
for a being Real
for f being Element of PFuncs (A,REAL) holds b1 . (a,f) = a (#) f
proofend;
uniqueness
 for b1, b2 being Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) st ( for a being Real
for f being Element of PFuncs (A,REAL) holds b1 . (a,f) = a (#) f ) & ( for a being Real
for f being Element of PFuncs (A,REAL) holds b2 . (a,f) = a (#) f ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines multrealpfunc LPSPACE1:def_4_:_
 for A being non empty set
for b2 being Function of [:REAL,(PFuncs (A,REAL)):],(PFuncs (A,REAL)) holds
( b2 = multrealpfunc A iff for a being Real
for f being Element of PFuncs (A,REAL) holds b2 . (a,f) = a (#) f );

definition
let A be non empty set ;
func RealPFuncZero A ->  Element of PFuncs (A,REAL) equals :: LPSPACE1:def 5
A --> 0;
coherence
 A --> 0 is Element of PFuncs (A,REAL)
proofend;
end;

:: deftheorem  defines RealPFuncZero LPSPACE1:def_5_:_
 for A being non empty set holds RealPFuncZero A = A --> 0;

definition
let A be non empty set ;
func RealPFuncUnit A ->  Element of PFuncs (A,REAL) equals :: LPSPACE1:def 6
A --> 1;
coherence
 A --> 1 is Element of PFuncs (A,REAL)
proofend;
end;

:: deftheorem  defines RealPFuncUnit LPSPACE1:def_6_:_
 for A being non empty set holds RealPFuncUnit A = A --> 1;

theorem Th6: :: LPSPACE1:6
for A being non empty set
for h, f, g being Element of PFuncs (A,REAL) holds
( h = (addpfunc A) . (f,g) iff ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) + (g . x) ) ) )
proofend;

theorem Th7: :: LPSPACE1:7
for A being non empty set
for h, f, g being Element of PFuncs (A,REAL) holds
( h = (multpfunc A) . (f,g) iff ( dom h = (dom f) /\ (dom g) & ( for x being Element of A st x in dom h holds
h . x = (f . x) * (g . x) ) ) )
proofend;

theorem :: LPSPACE1:8
for A being non empty set holds RealPFuncZero A <> RealPFuncUnit A
proofend;

theorem Th9: :: LPSPACE1:9
for a being Real
for A being non empty set
for h, f being Element of PFuncs (A,REAL) holds
( h = (multrealpfunc A) . (a,f) iff ( dom h = dom f &amp; ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) ) )
proofend;

theorem Th10: :: LPSPACE1:10
for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,g) = (addpfunc A) . (g,f)
proofend;

theorem Th11: :: LPSPACE1:11
for A being non empty set
for f, g, h being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((addpfunc A) . (f,g)),h)
proofend;

theorem :: LPSPACE1:12
for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (multpfunc A) . (f,g) = (multpfunc A) . (g,f)
proofend;

theorem :: LPSPACE1:13
for A being non empty set
for f, g, h being Element of PFuncs (A,REAL) holds (multpfunc A) . (f,((multpfunc A) . (g,h))) = (multpfunc A) . (((multpfunc A) . (f,g)),h)
proofend;

theorem :: LPSPACE1:14
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (multpfunc A) . ((RealPFuncUnit A),f) = f
proofend;

theorem Th15: :: LPSPACE1:15
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (addpfunc A) . ((RealPFuncZero A),f) = f
proofend;

theorem Th16: :: LPSPACE1:16
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (addpfunc A) . (f,((multrealpfunc A) . ((- 1),f))) = (RealPFuncZero A) | (dom f)
proofend;

theorem Th17: :: LPSPACE1:17
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (multrealpfunc A) . (1,f) = f
proofend;

theorem Th18: :: LPSPACE1:18
for a, b being Real
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (multrealpfunc A) . (a,((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a * b),f)
proofend;

theorem Th19: :: LPSPACE1:19
for a, b being Real
for A being non empty set
for f being Element of PFuncs (A,REAL) holds (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (b,f))) = (multrealpfunc A) . ((a + b),f)
proofend;

Lm1:  for a being Real
for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (addpfunc A) . (((multrealpfunc A) . (a,f)),((multrealpfunc A) . (a,g))) = (multrealpfunc A) . (a,((addpfunc A) . (f,g)))
proofend;

theorem :: LPSPACE1:20
for A being non empty set
for f, g, h being Element of PFuncs (A,REAL) holds (multpfunc A) . (f,((addpfunc A) . (g,h))) = (addpfunc A) . (((multpfunc A) . (f,g)),((multpfunc A) . (f,h)))
proofend;

theorem :: LPSPACE1:21
for a being Real
for A being non empty set
for f, g being Element of PFuncs (A,REAL) holds (multpfunc A) . (((multrealpfunc A) . (a,f)),g) = (multrealpfunc A) . (a,((multpfunc A) . (f,g)))
proofend;

definition
let A be non empty set ;
func RLSp_PFunct A ->  non empty RLSStruct  equals :: LPSPACE1:def 7
 RLSStruct(# (PFuncs (A,REAL)),(RealPFuncZero A),(addpfunc A),(multrealpfunc A) #);
coherence
 RLSStruct(# (PFuncs (A,REAL)),(RealPFuncZero A),(addpfunc A),(multrealpfunc A) #) is non empty RLSStruct ;
end;

:: deftheorem  defines RLSp_PFunct LPSPACE1:def_7_:_
 for A being non empty set holds RLSp_PFunct A = RLSStruct(# (PFuncs (A,REAL)),(RealPFuncZero A),(addpfunc A),(multrealpfunc A) #);

registration
let A be non empty set ;
cluster RLSp_PFunct A ->  non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( RLSp_PFunct A is strict &amp; RLSp_PFunct A is Abelian &amp; RLSp_PFunct A is add-associative &amp; RLSp_PFunct A is right_zeroed &amp; RLSp_PFunct A is vector-distributive &amp; RLSp_PFunct A is scalar-distributive &amp; RLSp_PFunct A is scalar-associative &amp; RLSp_PFunct A is scalar-unital )
proofend;
end;

begin

theorem Th22: :: LPSPACE1:22
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,ExtREAL st ex E being Element of S st E = dom f &amp; ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M &amp; Integral (M,f) = 0 )
proofend;

definition
let X be non empty set ;
let r be Real;
:: original:-->
redefine funcX --> r ->  PartFunc of X,REAL;
coherence
 X --> r is PartFunc of X,REAL
proofend;
end;

Lm2:  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 &amp; ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( f is_integrable_on M &amp; Integral (M,f) = 0 )
proofend;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func L1_Functions M ->  non empty Subset of (RLSp_PFunct X) equals :: LPSPACE1:def 8
 {  f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 &amp; dom f = ND ` &amp; f is_integrable_on M )  }  ;
correctness
coherence
{  f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 &amp; dom f = ND ` &amp; f is_integrable_on M )  }  is non empty Subset of (RLSp_PFunct X);
proofend;
end;

:: deftheorem  defines L1_Functions LPSPACE1:def_8_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds L1_Functions M =  {  f where f is PartFunc of X,REAL : ex ND being Element of S st
( M . ND = 0 &amp; dom f = ND ` &amp; f is_integrable_on M )  }  ;

Lm3:  for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( X --> 0 is PartFunc of X,REAL &amp; X --> 0 in L1_Functions M )
proofend;

Lm4:  for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S st M . E1 = 0 &amp; M . E2 = 0 holds
M . (E1 \/ E2) = 0
proofend;

theorem Th23: :: LPSPACE1:23
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 st f in L1_Functions M &amp; g in L1_Functions M holds
f + g in L1_Functions M
proofend;

theorem Th24: :: LPSPACE1:24
for a being Real
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
a (#) f in L1_Functions M
proofend;

Lm5:  for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( L1_Functions M is add-closed &amp; L1_Functions M is multi-closed )
proofend;

registration
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster L1_Functions M ->  non empty add-closed multi-closed ;
coherence
 ( L1_Functions M is multi-closed &amp; L1_Functions M is add-closed ) by Lm5;
end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func RLSp_L1Funct M ->  non empty RLSStruct  equals :: LPSPACE1:def 9
 RLSStruct(# (L1_Functions M),(In ((0. (RLSp_PFunct X)),(L1_Functions M))),(add| ((L1_Functions M),(RLSp_PFunct X))),(Mult_ (L1_Functions M)) #);
coherence
 RLSStruct(# (L1_Functions M),(In ((0. (RLSp_PFunct X)),(L1_Functions M))),(add| ((L1_Functions M),(RLSp_PFunct X))),(Mult_ (L1_Functions M)) #) is non empty RLSStruct ;
end;

:: deftheorem  defines RLSp_L1Funct LPSPACE1:def_9_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds RLSp_L1Funct M = RLSStruct(# (L1_Functions M),(In ((0. (RLSp_PFunct X)),(L1_Functions M))),(add| ((L1_Functions M),(RLSp_PFunct X))),(Mult_ (L1_Functions M)) #);

registration
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster RLSp_L1Funct M ->  non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( RLSp_L1Funct M is strict &amp; RLSp_L1Funct M is Abelian &amp; RLSp_L1Funct M is add-associative &amp; RLSp_L1Funct M is right_zeroed &amp; RLSp_L1Funct M is vector-distributive &amp; RLSp_L1Funct M is scalar-distributive &amp; RLSp_L1Funct M is scalar-associative &amp; RLSp_L1Funct M is scalar-unital )
proofend;
end;

begin

theorem Th25: :: LPSPACE1: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 v, u being VECTOR of (RLSp_L1Funct M) st f = v &amp; g = u holds
f + g = v + u
proofend;

theorem Th26: :: LPSPACE1:26
for a being Real
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 u being VECTOR of (RLSp_L1Funct M) st f = u holds
a (#) f = a * u
proofend;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f, g be PartFunc of X,REAL;
predf a.e.= g,M means :Def10: :: LPSPACE1:def 10
 ex E being Element of S st
( M . E = 0 &amp; f | (E `) = g | (E `) );
end;

:: deftheorem Def10 defines a.e.= LPSPACE1:def_10_:_
 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 holds
( f a.e.= g,M iff ex E being Element of S st
( M . E = 0 &amp; f | (E `) = g | (E `) ) );

theorem Th27: :: LPSPACE1:27
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 u being VECTOR of (RLSp_L1Funct M) st f = u holds
( u + ((- 1) * u) = (X --> 0) | (dom f) &amp; ex v, g being PartFunc of X,REAL st
( v in L1_Functions M &amp; g in L1_Functions M &amp; v = u + ((- 1) * u) &amp; g = X --> 0 &amp; v a.e.= g,M ) )
proofend;

theorem Th28: :: LPSPACE1: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 holds f a.e.= f,M
proofend;

theorem Th29: :: LPSPACE1: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 st f a.e.= g,M holds
g a.e.= f,M
proofend;

theorem Th30: :: LPSPACE1:30
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g, h being PartFunc of X,REAL st f a.e.= g,M &amp; g a.e.= h,M holds
f a.e.= h,M
proofend;

theorem Th31: :: LPSPACE1:31
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 st f a.e.= f1,M &amp; g a.e.= g1,M holds
f + g a.e.= f1 + g1,M
proofend;

theorem Th32: :: LPSPACE1:32
for a being Real
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 st f a.e.= g,M holds
a (#) f a.e.= a (#) g,M
proofend;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func AlmostZeroFunctions M ->  non empty Subset of (RLSp_L1Funct M) equals :: LPSPACE1:def 11
 {  f where f is PartFunc of X,REAL : ( f in L1_Functions M &amp; f a.e.= X --> 0,M )  }  ;
coherence
  {  f where f is PartFunc of X,REAL : ( f in L1_Functions M &amp; f a.e.= X --> 0,M )  }  is non empty Subset of (RLSp_L1Funct M)
proofend;
end;

:: deftheorem  defines AlmostZeroFunctions LPSPACE1:def_11_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds AlmostZeroFunctions M =  {  f where f is PartFunc of X,REAL : ( f in L1_Functions M &amp; f a.e.= X --> 0,M )  }  ;

theorem Th33: :: LPSPACE1:33
for a being Real
for X being non empty set holds
( (X --> 0) + (X --> 0) = X --> 0 &amp; a (#) (X --> 0) = X --> 0 )
proofend;

Lm6:  for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( AlmostZeroFunctions M is add-closed &amp; AlmostZeroFunctions M is multi-closed )
proofend;

registration
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster AlmostZeroFunctions M ->  non empty add-closed multi-closed ;
coherence
 ( AlmostZeroFunctions M is add-closed &amp; AlmostZeroFunctions M is multi-closed ) by Lm6;
end;

theorem Th34: :: LPSPACE1:34
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( 0. (RLSp_L1Funct M) = X --> 0 &amp; 0. (RLSp_L1Funct M) in AlmostZeroFunctions M )
proofend;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func RLSp_AlmostZeroFunct M ->  non empty RLSStruct  equals :: LPSPACE1:def 12
 RLSStruct(# (AlmostZeroFunctions M),(In ((0. (RLSp_L1Funct M)),(AlmostZeroFunctions M))),(add| ((AlmostZeroFunctions M),(RLSp_L1Funct M))),(Mult_ (AlmostZeroFunctions M)) #);
coherence
 RLSStruct(# (AlmostZeroFunctions M),(In ((0. (RLSp_L1Funct M)),(AlmostZeroFunctions M))),(add| ((AlmostZeroFunctions M),(RLSp_L1Funct M))),(Mult_ (AlmostZeroFunctions M)) #) is non empty RLSStruct ;
end;

:: deftheorem  defines RLSp_AlmostZeroFunct LPSPACE1:def_12_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds RLSp_AlmostZeroFunct M = RLSStruct(# (AlmostZeroFunctions M),(In ((0. (RLSp_L1Funct M)),(AlmostZeroFunctions M))),(add| ((AlmostZeroFunctions M),(RLSp_L1Funct M))),(Mult_ (AlmostZeroFunctions M)) #);

registration
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster RLSp_L1Funct M ->  non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( RLSp_L1Funct M is strict &amp; RLSp_L1Funct M is strict &amp; RLSp_L1Funct M is Abelian &amp; RLSp_L1Funct M is add-associative &amp; RLSp_L1Funct M is right_zeroed &amp; RLSp_L1Funct M is vector-distributive &amp; RLSp_L1Funct M is scalar-distributive &amp; RLSp_L1Funct M is scalar-associative &amp; RLSp_L1Funct M is scalar-unital ) ;
end;

theorem :: LPSPACE1:35
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 v, u being VECTOR of (RLSp_AlmostZeroFunct M) st f = v &amp; g = u holds
f + g = v + u
proofend;

theorem :: LPSPACE1:36
for a being Real
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 u being VECTOR of (RLSp_AlmostZeroFunct M) st f = u holds
a (#) f = a * u
proofend;

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;
func a.e-eq-class (f,M) ->  Subset of (L1_Functions M) equals :: LPSPACE1:def 13
 {  g where g is PartFunc of X,REAL : ( g in L1_Functions M &amp; f in L1_Functions M &amp; f a.e.= g,M )  }  ;
correctness
coherence
{  g where g is PartFunc of X,REAL : ( g in L1_Functions M &amp; f in L1_Functions M &amp; f a.e.= g,M )  }  is Subset of (L1_Functions M);
proofend;
end;

:: deftheorem  defines a.e-eq-class LPSPACE1:def_13_:_
 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) =  {  g where g is PartFunc of X,REAL : ( g in L1_Functions M &amp; f in L1_Functions M &amp; f a.e.= g,M )  }  ;

theorem Th37: :: LPSPACE1: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 st f in L1_Functions M &amp; g in L1_Functions M holds
( g a.e.= f,M iff g in a.e-eq-class (f,M) )
proofend;

theorem Th38: :: LPSPACE1: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 st f in L1_Functions M holds
f in a.e-eq-class (f,M)
proofend;

theorem Th39: :: LPSPACE1: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 st f in L1_Functions M &amp; g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff f a.e.= g,M )
proofend;

theorem :: LPSPACE1: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 st f in L1_Functions M &amp; g in L1_Functions M holds
( a.e-eq-class (f,M) = a.e-eq-class (g,M) iff g in a.e-eq-class (f,M) )
proofend;

theorem Th41: :: LPSPACE1:41
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 st f in L1_Functions M &amp; f1 in L1_Functions M &amp; g in L1_Functions M &amp; g1 in L1_Functions M &amp; a.e-eq-class (f,M) = a.e-eq-class (f1,M) &amp; a.e-eq-class (g,M) = a.e-eq-class (g1,M) holds
a.e-eq-class ((f + g),M) = a.e-eq-class ((f1 + g1),M)
proofend;

theorem Th42: :: LPSPACE1:42
for a being Real
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 st f in L1_Functions M &amp; g in L1_Functions M &amp; a.e-eq-class (f,M) = a.e-eq-class (g,M) holds
a.e-eq-class ((a (#) f),M) = a.e-eq-class ((a (#) g),M)
proofend;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func CosetSet M ->  non empty Subset-Family of (L1_Functions M) equals :: LPSPACE1:def 14
 {  (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M  }  ;
correctness
coherence
{  (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M  }  is non empty Subset-Family of (L1_Functions M);
proofend;
end;

:: deftheorem  defines CosetSet LPSPACE1:def_14_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds CosetSet M =  {  (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M  }  ;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func addCoset M ->  BinOp of (CosetSet M) means :Def15: :: LPSPACE1:def 15
 for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A &amp; b in B holds
it . (A,B) = a.e-eq-class ((a + b),M);
existence
 ex b1 being BinOp of (CosetSet M) st
for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A &amp; b in B holds
b1 . (A,B) = a.e-eq-class ((a + b),M)
proofend;
uniqueness
 for b1, b2 being BinOp of (CosetSet M) st ( for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A &amp; b in B holds
b1 . (A,B) = a.e-eq-class ((a + b),M) ) &amp; ( for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A &amp; b in B holds
b2 . (A,B) = a.e-eq-class ((a + b),M) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines addCoset LPSPACE1:def_15_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being BinOp of (CosetSet M) holds
( b4 = addCoset M iff for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A &amp; b in B holds
b4 . (A,B) = a.e-eq-class ((a + b),M) );

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func zeroCoset M ->  Element of CosetSet M means :Def16: :: LPSPACE1:def 16
 ex f being PartFunc of X,REAL st
( f = X --> 0 &amp; f in L1_Functions M &amp; it = a.e-eq-class (f,M) );
correctness
existence
ex b1 being Element of CosetSet M ex f being PartFunc of X,REAL st
( f = X --> 0 &amp; f in L1_Functions M &amp; b1 = a.e-eq-class (f,M) );
uniqueness
for b1, b2 being Element of CosetSet M st ex f being PartFunc of X,REAL st
( f = X --> 0 &amp; f in L1_Functions M &amp; b1 = a.e-eq-class (f,M) ) &amp; ex f being PartFunc of X,REAL st
( f = X --> 0 &amp; f in L1_Functions M &amp; b2 = a.e-eq-class (f,M) ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def16 defines zeroCoset LPSPACE1:def_16_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being Element of CosetSet M holds
( b4 = zeroCoset M iff ex f being PartFunc of X,REAL st
( f = X --> 0 &amp; f in L1_Functions M &amp; b4 = a.e-eq-class (f,M) ) );

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func lmultCoset M ->  Function of [:REAL,(CosetSet M):],(CosetSet M) means :Def17: :: LPSPACE1:def 17
 for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
it . (z,A) = a.e-eq-class ((z (#) f),M);
existence
 ex b1 being Function of [:REAL,(CosetSet M):],(CosetSet M) st
for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b1 . (z,A) = a.e-eq-class ((z (#) f),M)
proofend;
uniqueness
 for b1, b2 being Function of [:REAL,(CosetSet M):],(CosetSet M) st ( for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b1 . (z,A) = a.e-eq-class ((z (#) f),M) ) &amp; ( for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b2 . (z,A) = a.e-eq-class ((z (#) f),M) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines lmultCoset LPSPACE1:def_17_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being Function of [:REAL,(CosetSet M):],(CosetSet M) holds
( b4 = lmultCoset M iff for z being Element of REAL
for A being Element of CosetSet M
for f being PartFunc of X,REAL st f in A holds
b4 . (z,A) = a.e-eq-class ((z (#) f),M) );

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func Pre-L-Space M ->  non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct  means :Def18: :: LPSPACE1:def 18
( the carrier of it = CosetSet M &amp; the addF of it = addCoset M &amp; 0. it = zeroCoset M &amp; the Mult of it = lmultCoset M );
existence
 ex b1 being non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct st
( the carrier of b1 = CosetSet M &amp; the addF of b1 = addCoset M &amp; 0. b1 = zeroCoset M &amp; the Mult of b1 = lmultCoset M )
proofend;
uniqueness
 for b1, b2 being non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct st the carrier of b1 = CosetSet M &amp; the addF of b1 = addCoset M &amp; 0. b1 = zeroCoset M &amp; the Mult of b1 = lmultCoset M &amp; the carrier of b2 = CosetSet M &amp; the addF of b2 = addCoset M &amp; 0. b2 = zeroCoset M &amp; the Mult of b2 = lmultCoset M holds
b1 = b2 ;
end;

:: deftheorem Def18 defines Pre-L-Space LPSPACE1:def_18_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct holds
( b4 = Pre-L-Space M iff ( the carrier of b4 = CosetSet M &amp; the addF of b4 = addCoset M &amp; 0. b4 = zeroCoset M &amp; the Mult of b4 = lmultCoset M ) );

begin

theorem Th43: :: LPSPACE1: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 st f in L1_Functions M &amp; g in L1_Functions M &amp; f a.e.= g,M holds
Integral (M,f) = Integral (M,g)
proofend;

theorem Th44: :: LPSPACE1:44
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 is_integrable_on M holds
( Integral (M,f) in REAL &amp; Integral (M,(abs f)) in REAL &amp; abs f is_integrable_on M )
proofend;

theorem Th45: :: LPSPACE1:45
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 st f in L1_Functions M &amp; g in L1_Functions M &amp; f a.e.= g,M holds
( abs f a.e.= abs g,M &amp; Integral (M,(abs f)) = Integral (M,(abs g)) )
proofend;

theorem Th46: :: LPSPACE1: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 st ex x being VECTOR of (Pre-L-Space M) st
( f in x &amp; g in x ) holds
( f a.e.= g,M &amp; f in L1_Functions M &amp; g in L1_Functions M )
proofend;

theorem Th47: :: LPSPACE1:47
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 x being Point of (Pre-L-Space M) st f in x holds
( f is_integrable_on M &amp; f in L1_Functions M &amp; abs f is_integrable_on M )
proofend;

theorem Th48: :: LPSPACE1: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 x being Point of (Pre-L-Space M) st f in x &amp; g in x holds
( f a.e.= g,M &amp; Integral (M,f) = Integral (M,g) &amp; Integral (M,(abs f)) = Integral (M,(abs g)) )
proofend;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func L-1-Norm M ->  Function of the carrier of (Pre-L-Space M),REAL means :Def19: :: LPSPACE1:def 19
 for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x &amp; it . x = Integral (M,(abs f)) );
existence
 ex b1 being Function of the carrier of (Pre-L-Space M),REAL st
for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x &amp; b1 . x = Integral (M,(abs f)) )
proofend;
uniqueness
 for b1, b2 being Function of the carrier of (Pre-L-Space M),REAL st ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x &amp; b1 . x = Integral (M,(abs f)) ) ) &amp; ( for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x &amp; b2 . x = Integral (M,(abs f)) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def19 defines L-1-Norm LPSPACE1:def_19_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being Function of the carrier of (Pre-L-Space M),REAL holds
( b4 = L-1-Norm M iff for x being Point of (Pre-L-Space M) ex f being PartFunc of X,REAL st
( f in x &amp; b4 . x = Integral (M,(abs f)) ) );

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func L-1-Space M ->  non empty NORMSTR  equals :: LPSPACE1:def 20
 NORMSTR(# the carrier of (Pre-L-Space M), the ZeroF of (Pre-L-Space M), the addF of (Pre-L-Space M), the Mult of (Pre-L-Space M),(L-1-Norm M) #);
coherence
 NORMSTR(# the carrier of (Pre-L-Space M), the ZeroF of (Pre-L-Space M), the addF of (Pre-L-Space M), the Mult of (Pre-L-Space M),(L-1-Norm M) #) is non empty NORMSTR ;
end;

:: deftheorem  defines L-1-Space LPSPACE1:def_20_:_
 for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds L-1-Space M = NORMSTR(# the carrier of (Pre-L-Space M), the ZeroF of (Pre-L-Space M), the addF of (Pre-L-Space M), the Mult of (Pre-L-Space M),(L-1-Norm M) #);

theorem Th49: :: LPSPACE1:49
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for x being Point of (L-1-Space M) holds
( ex f being PartFunc of X,REAL st
( f in L1_Functions M &amp; x = a.e-eq-class (f,M) &amp; ||.x.|| = Integral (M,(abs f)) ) &amp; ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )
proofend;

theorem Th50: :: LPSPACE1:50
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 x being Point of (L-1-Space M) st f in x holds
( x = a.e-eq-class (f,M) &amp; ||.x.|| = Integral (M,(abs f)) )
proofend;

theorem Th51: :: LPSPACE1:51
for a being Real
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 x, y being Point of (L-1-Space M) holds
( ( f in x &amp; g in y implies f + g in x + y ) &amp; ( f in x implies a (#) f in a * x ) )
proofend;

theorem Th52: :: LPSPACE1:52
for r being Real
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st E = dom f &amp; ( for x being set st x in dom f holds
f . x = r ) holds
f is_measurable_on E
proofend;

theorem Th53: :: LPSPACE1:53
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 &amp; Integral (M,(abs f)) = 0 holds
f a.e.= X --> 0,M
proofend;

theorem Th54: :: LPSPACE1:54
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds Integral (M,(abs (X --> 0))) = 0
proofend;

theorem Th55: :: LPSPACE1:55
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 st f is_integrable_on M &amp; g is_integrable_on M holds
Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))
proofend;

Lm7:  for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( L-1-Space M is RealNormSpace-like &amp; L-1-Space M is vector-distributive &amp; L-1-Space M is scalar-distributive &amp; L-1-Space M is scalar-associative &amp; L-1-Space M is scalar-unital &amp; L-1-Space M is Abelian &amp; L-1-Space M is add-associative &amp; L-1-Space M is right_zeroed &amp; L-1-Space M is right_complementable )
proofend;

registration
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster L-1-Space M ->  non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealNormSpace-like ;
coherence
 ( L-1-Space M is RealNormSpace-like &amp; L-1-Space M is vector-distributive &amp; L-1-Space M is scalar-distributive &amp; L-1-Space M is scalar-associative &amp; L-1-Space M is scalar-unital &amp; L-1-Space M is Abelian &amp; L-1-Space M is add-associative &amp; L-1-Space M is right_zeroed &amp; L-1-Space M is right_complementable ) by Lm7;
end;