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

registration
let D be non empty set ;
let E be complex-membered set ;
cluster -> complex-valued for of ;
coherence
for b1 being Element of PFuncs (D,E) holds b1 is complex-valued
;
end;

definition
let D be non empty set ;
let E be complex-membered set ;
let F1, F2 be Element of PFuncs (D,E);
:: original: +
redefine func F1 + F2 -> Element of PFuncs (D,COMPLEX);
coherence
F1 + F2 is Element of PFuncs (D,COMPLEX)
proof end;
:: original: -
redefine func F1 - F2 -> Element of PFuncs (D,COMPLEX);
coherence
F1 - F2 is Element of PFuncs (D,COMPLEX)
proof end;
:: original: (#)
redefine func F1 (#) F2 -> Element of PFuncs (D,COMPLEX);
coherence
F1 (#) F2 is Element of PFuncs (D,COMPLEX)
proof end;
:: original: /"
redefine func F1 /" F2 -> Element of PFuncs (D,COMPLEX);
coherence
F1 /" F2 is Element of PFuncs (D,COMPLEX)
proof end;
end;

definition
let D be non empty set ;
let E be complex-membered set ;
let F be Element of PFuncs (D,E);
let a be Complex;
:: original: (#)
redefine func a (#) F -> Element of PFuncs (D,COMPLEX);
coherence
a (#) F is Element of PFuncs (D,COMPLEX)
proof end;
end;

definition
let V be non empty CLSStruct ;
let V1 be Subset of V;
attr V1 is multi-closed means :Def1: :: LPSPACC1:def 1
for a being Complex
for v being VECTOR of V st v in V1 holds
a * v in V1;
end;

:: deftheorem Def1 defines multi-closed LPSPACC1:def 1 :
for V being non empty CLSStruct
for V1 being Subset of V holds
( V1 is multi-closed iff for a being Complex
for v being VECTOR of V st v in V1 holds
a * v in V1 );

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

registration
let V be non empty CLSStruct ;
cluster non empty add-closed multi-closed for Subset of V;
existence
ex b1 being non empty Subset of V st
( b1 is add-closed & b1 is multi-closed )
proof end;
end;

definition
let X be non empty CLSStruct ;
let X1 be non empty multi-closed Subset of X;
func Mult_ X1 -> Function of [:COMPLEX,X1:],X1 equals :: LPSPACC1:def 2
the Mult of X | [:COMPLEX,X1:];
correctness
coherence
the Mult of X | [:COMPLEX,X1:] is Function of [:COMPLEX,X1:],X1
;
proof end;
end;

:: deftheorem defines Mult_ LPSPACC1:def 2 :
for X being non empty CLSStruct
for X1 being non empty multi-closed Subset of X holds Mult_ X1 = the Mult of X | [:COMPLEX,X1:];

theorem Th2: :: LPSPACC1:2
for V being non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
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 [:COMPLEX,V1:],V1 st d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX,V1:] holds
( CLSStruct(# V1,d1,A,M #) is Abelian & CLSStruct(# V1,d1,A,M #) is add-associative & CLSStruct(# V1,d1,A,M #) is right_zeroed & CLSStruct(# V1,d1,A,M #) is vector-distributive & CLSStruct(# V1,d1,A,M #) is scalar-distributive & CLSStruct(# V1,d1,A,M #) is scalar-associative & CLSStruct(# V1,d1,A,M #) is scalar-unital )
proof end;

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

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

:: deftheorem Def3 defines multcpfunc LPSPACC1:def 3 :
for A being non empty set
for b2 being BinOp of (PFuncs (A,COMPLEX)) holds
( b2 = multcpfunc A iff for f, g being Element of PFuncs (A,COMPLEX) holds b2 . (f,g) = f (#) g );

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

:: deftheorem Def4 defines multcomplexcpfunc LPSPACC1:def 4 :
for A being non empty set
for b2 being Function of [:COMPLEX,(PFuncs (A,COMPLEX)):],(PFuncs (A,COMPLEX)) holds
( b2 = multcomplexcpfunc A iff for a being Complex
for f being Element of PFuncs (A,COMPLEX) holds b2 . (a,f) = a (#) f );

definition
let D be non empty set ;
func addcpfunc D -> BinOp of (PFuncs (D,COMPLEX)) means :Def5: :: LPSPACC1:def 5
for F1, F2 being Element of PFuncs (D,COMPLEX) holds it . (F1,F2) = F1 + F2;
existence
ex b1 being BinOp of (PFuncs (D,COMPLEX)) st
for F1, F2 being Element of PFuncs (D,COMPLEX) holds b1 . (F1,F2) = F1 + F2
proof end;
uniqueness
for b1, b2 being BinOp of (PFuncs (D,COMPLEX)) st ( for F1, F2 being Element of PFuncs (D,COMPLEX) holds b1 . (F1,F2) = F1 + F2 ) & ( for F1, F2 being Element of PFuncs (D,COMPLEX) holds b2 . (F1,F2) = F1 + F2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines addcpfunc LPSPACC1:def 5 :
for D being non empty set
for b2 being BinOp of (PFuncs (D,COMPLEX)) holds
( b2 = addcpfunc D iff for F1, F2 being Element of PFuncs (D,COMPLEX) holds b2 . (F1,F2) = F1 + F2 );

definition
let A be set ;
func CPFuncZero A -> Element of PFuncs (A,COMPLEX) equals :: LPSPACC1:def 6
A --> 0c;
coherence
A --> 0c is Element of PFuncs (A,COMPLEX)
by PARTFUN1:45;
end;

:: deftheorem defines CPFuncZero LPSPACC1:def 6 :
for A being set holds CPFuncZero A = A --> 0c;

definition
let A be set ;
func CPFuncUnit A -> Element of PFuncs (A,COMPLEX) equals :: LPSPACC1:def 7
A --> 1r;
coherence
A --> 1r is Element of PFuncs (A,COMPLEX)
by PARTFUN1:45;
end;

:: deftheorem defines CPFuncUnit LPSPACC1:def 7 :
for A being set holds CPFuncUnit A = A --> 1r;

theorem Th4: :: LPSPACC1:4
for A being non empty set
for f, g, h being Element of PFuncs (A,COMPLEX) holds
( h = () . (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) ) ) )
proof end;

theorem Th5: :: LPSPACC1:5
for A being non empty set
for f, g, h being Element of PFuncs (A,COMPLEX) holds
( h = () . (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) ) ) )
proof end;

theorem :: LPSPACC1:6
for A being non empty set holds CPFuncZero A <> CPFuncUnit A
proof end;

theorem Th7: :: LPSPACC1:7
for a being Complex
for A being non empty set
for f, h being Element of PFuncs (A,COMPLEX) holds
( h = . (a,f) iff ( dom h = dom f & ( for x being Element of A st x in dom f holds
h . x = a * (f . x) ) ) )
proof end;

registration
let A be non empty set ;
coherence
proof end;
end;

registration
let A be non empty set ;
coherence
proof end;
end;

theorem :: LPSPACC1:8
for A being non empty set holds CPFuncUnit A is_a_unity_wrt multcpfunc A
proof end;

theorem Th9: :: LPSPACC1:9
for A being non empty set holds CPFuncZero A is_a_unity_wrt addcpfunc A
proof end;

reconsider R = - 1r as Element of COMPLEX by XCMPLX_0:def 2;

theorem Th10: :: LPSPACC1:10
for A being non empty set
for f being Element of PFuncs (A,COMPLEX) holds () . (f,( . ((),f))) = () | (dom f)
proof end;

theorem Th11: :: LPSPACC1:11
for A being non empty set
for f being Element of PFuncs (A,COMPLEX) holds . (1r,f) = f
proof end;

theorem Th12: :: LPSPACC1:12
for a, b being Complex
for A being non empty set
for f being Element of PFuncs (A,COMPLEX) holds . (a,( . (b,f))) = . ((a * b),f)
proof end;

theorem Th13: :: LPSPACC1:13
for a, b being Complex
for A being non empty set
for f being Element of PFuncs (A,COMPLEX) holds () . (( . (a,f)),( . (b,f))) = . ((a + b),f)
proof end;

Lm1: for a being Complex
for A being non empty set
for f, g being Element of PFuncs (A,COMPLEX) holds () . (( . (a,f)),( . (a,g))) = . (a,(() . (f,g)))

proof end;

theorem :: LPSPACC1:14
for A being non empty set
for f, g, h being Element of PFuncs (A,COMPLEX) holds () . (f,(() . (g,h))) = () . ((() . (f,g)),(() . (f,h)))
proof end;

theorem :: LPSPACC1:15
for a being Complex
for A being non empty set
for f, g being Element of PFuncs (A,COMPLEX) holds () . (( . (a,f)),g) = . (a,(() . (f,g)))
proof end;

definition
let A be non empty set ;
func CLSp_PFunct A -> non empty CLSStruct equals :: LPSPACC1:def 8
CLSStruct(# (PFuncs (A,COMPLEX)),(),(), #);
coherence
CLSStruct(# (PFuncs (A,COMPLEX)),(),(), #) is non empty CLSStruct
;
end;

:: deftheorem defines CLSp_PFunct LPSPACC1:def 8 :
for A being non empty set holds CLSp_PFunct A = CLSStruct(# (PFuncs (A,COMPLEX)),(),(), #);

registration
let A be non empty set ;
coherence
proof end;
end;

registration
let X be non empty set ;
let f be PartFunc of X,COMPLEX;
cluster K342(f) -> nonnegative ;
coherence
proof end;
end;

theorem Th16: :: LPSPACC1:16
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,COMPLEX st dom f in S & ( 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;

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,COMPLEX 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;
func L1_CFunctions M -> non empty Subset of () equals :: LPSPACC1:def 9
{ f where f is PartFunc of X,COMPLEX : ex ND being Element of S st
( M . ND = 0 & dom f = ND  & f is_integrable_on M )
}
;
correctness
coherence
{ f where f is PartFunc of X,COMPLEX : ex ND being Element of S st
( M . ND = 0 & dom f = ND  & f is_integrable_on M )
}
is non empty Subset of ()
;
proof end;
end;

:: deftheorem defines L1_CFunctions LPSPACC1:def 9 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds L1_CFunctions M = { f where f is PartFunc of X,COMPLEX : ex ND being Element of S st
( M . ND = 0 & dom f = ND  & 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 in L1_CFunctions M

proof end;

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 & M . E2 = 0 holds
M . (E1 \/ E2) = 0

proof end;

theorem Th17: :: LPSPACC1:17
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,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M holds
f + g in L1_CFunctions M
proof end;

theorem Th18: :: LPSPACC1:18
for a being Complex
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,COMPLEX st f in L1_CFunctions M holds
a (#) f in L1_CFunctions M
proof end;

Lm5: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( L1_CFunctions M is add-closed & L1_CFunctions M 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;
coherence by Lm5;
end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func CLSp_L1Funct M -> non empty CLSStruct equals :: LPSPACC1:def 10
CLSStruct(# (),(In ((0. ()),())),(add| ((),())),() #);
coherence
CLSStruct(# (),(In ((0. ()),())),(add| ((),())),() #) is non empty CLSStruct
;
end;

:: deftheorem defines CLSp_L1Funct LPSPACC1:def 10 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds CLSp_L1Funct M = CLSStruct(# (),(In ((0. ()),())),(add| ((),())),() #);

registration
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
coherence
proof end;
end;

theorem Th19: :: LPSPACC1:19
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,COMPLEX
for v, u being VECTOR of () st f = v & g = u holds
f + g = v + u
proof end;

theorem Th20: :: LPSPACC1:20
for a being Complex
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,COMPLEX
for u being VECTOR of () 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, g be PartFunc of X,COMPLEX;
pred f a.e.cpfunc= g,M means :Def11: :: LPSPACC1:def 11
ex E being Element of S st
( M . E = 0 & f | (E ) = g | (E ) );
end;

:: deftheorem Def11 defines a.e.cpfunc= LPSPACC1:def 11 :
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,COMPLEX holds
( f a.e.cpfunc= g,M iff ex E being Element of S st
( M . E = 0 & f | (E ) = g | (E `) ) );

theorem Th21: :: LPSPACC1:21
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,COMPLEX
for u being VECTOR of () st f = u holds
( u + (() * u) = () | (dom f) & ex v, g being PartFunc of X,COMPLEX st
( v in L1_CFunctions M & g in L1_CFunctions M & v = u + (() * u) & g = X --> 0c & v a.e.cpfunc= g,M ) )
proof end;

theorem Th22: :: LPSPACC1: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,COMPLEX holds f a.e.cpfunc= f,M
proof end;

theorem :: LPSPACC1: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,COMPLEX st f a.e.cpfunc= g,M holds
g a.e.cpfunc= f,M ;

theorem Th24: :: LPSPACC1:24
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,COMPLEX st f a.e.cpfunc= g,M & g a.e.cpfunc= h,M holds
f a.e.cpfunc= h,M
proof end;

theorem Th25: :: LPSPACC1:25
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,COMPLEX st f a.e.cpfunc= f1,M & g a.e.cpfunc= g1,M holds
f + g a.e.cpfunc= f1 + g1,M
proof end;

theorem Th26: :: LPSPACC1:26
for a being Complex
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,COMPLEX st f a.e.cpfunc= g,M holds
a (#) f a.e.cpfunc= a (#) g,M
proof end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func AlmostZeroCFunctions M -> non empty Subset of () equals :: LPSPACC1:def 12
{ f where f is PartFunc of X,COMPLEX : ( f in L1_CFunctions M & f a.e.cpfunc= X --> 0c,M ) } ;
coherence
{ f where f is PartFunc of X,COMPLEX : ( f in L1_CFunctions M & f a.e.cpfunc= X --> 0c,M ) } is non empty Subset of ()
proof end;
end;

:: deftheorem defines AlmostZeroCFunctions LPSPACC1:def 12 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds AlmostZeroCFunctions M = { f where f is PartFunc of X,COMPLEX : ( f in L1_CFunctions M & f a.e.cpfunc= X --> 0c,M ) } ;

theorem Th27: :: LPSPACC1:27
for a being Complex
for X being non empty set holds
( () + () = X --> 0c & a (#) () = X --> 0c )
proof end;

Lm6: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( AlmostZeroCFunctions M is add-closed & AlmostZeroCFunctions M 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;
coherence by Lm6;
end;

theorem :: LPSPACC1:28
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( 0. () = X --> 0c & 0. () in AlmostZeroCFunctions M )
proof end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func CLSp_AlmostZeroFunct M -> non empty CLSStruct equals :: LPSPACC1:def 13
CLSStruct(# ,(In ((0. ()),)),(add| (,())),() #);
coherence
CLSStruct(# ,(In ((0. ()),)),(add| (,())),() #) is non empty CLSStruct
;
end;

:: deftheorem defines CLSp_AlmostZeroFunct LPSPACC1:def 13 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds CLSp_AlmostZeroFunct M = CLSStruct(# ,(In ((0. ()),)),(add| (,())),() #);

registration
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
coherence ;
end;

theorem :: LPSPACC1: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,COMPLEX
for v, u being VECTOR of st f = v & g = u holds
f + g = v + 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,COMPLEX;
func a.e-Ceq-class (f,M) -> Subset of () equals :: LPSPACC1:def 14
{ g where g is PartFunc of X,COMPLEX : ( g in L1_CFunctions M & f in L1_CFunctions M & f a.e.cpfunc= g,M ) } ;
correctness
coherence
{ g where g is PartFunc of X,COMPLEX : ( g in L1_CFunctions M & f in L1_CFunctions M & f a.e.cpfunc= g,M ) } is Subset of ()
;
proof end;
end;

:: deftheorem defines a.e-Ceq-class LPSPACC1:def 14 :
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,COMPLEX holds a.e-Ceq-class (f,M) = { g where g is PartFunc of X,COMPLEX : ( g in L1_CFunctions M & f in L1_CFunctions M & f a.e.cpfunc= g,M ) } ;

theorem Th30: :: LPSPACC1:30
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,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M holds
( g a.e.cpfunc= f,M iff g in a.e-Ceq-class (f,M) )
proof end;

theorem Th31: :: LPSPACC1: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,COMPLEX st f in L1_CFunctions M holds
f in a.e-Ceq-class (f,M)
proof end;

theorem Th32: :: LPSPACC1:32
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,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M holds
( a.e-Ceq-class (f,M) = a.e-Ceq-class (g,M) iff f a.e.cpfunc= g,M )
proof end;

theorem :: LPSPACC1: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,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M holds
( a.e-Ceq-class (f,M) = a.e-Ceq-class (g,M) iff g in a.e-Ceq-class (f,M) )
proof end;

theorem Th34: :: LPSPACC1:34
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,COMPLEX st f in L1_CFunctions M & f1 in L1_CFunctions M & g in L1_CFunctions M & g1 in L1_CFunctions M & a.e-Ceq-class (f,M) = a.e-Ceq-class (f1,M) & a.e-Ceq-class (g,M) = a.e-Ceq-class (g1,M) holds
a.e-Ceq-class ((f + g),M) = a.e-Ceq-class ((f1 + g1),M)
proof end;

theorem Th35: :: LPSPACC1:35
for a being Complex
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,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M & a.e-Ceq-class (f,M) = a.e-Ceq-class (g,M) holds
a.e-Ceq-class ((a (#) f),M) = a.e-Ceq-class ((a (#) g),M)
proof end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func CCosetSet M -> non empty Subset-Family of () equals :: LPSPACC1:def 15
{ (a.e-Ceq-class (f,M)) where f is PartFunc of X,COMPLEX : f in L1_CFunctions M } ;
correctness
coherence
{ (a.e-Ceq-class (f,M)) where f is PartFunc of X,COMPLEX : f in L1_CFunctions M } is non empty Subset-Family of ()
;
proof end;
end;

:: deftheorem defines CCosetSet LPSPACC1:def 15 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds CCosetSet M = { (a.e-Ceq-class (f,M)) where f is PartFunc of X,COMPLEX : f in L1_CFunctions M } ;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func addCCoset M -> BinOp of () means :Def16: :: LPSPACC1:def 16
for A, B being Element of CCosetSet M
for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
it . (A,B) = a.e-Ceq-class ((a + b),M);
existence
ex b1 being BinOp of () st
for A, B being Element of CCosetSet M
for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
b1 . (A,B) = a.e-Ceq-class ((a + b),M)
proof end;
uniqueness
for b1, b2 being BinOp of () st ( for A, B being Element of CCosetSet M
for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
b1 . (A,B) = a.e-Ceq-class ((a + b),M) ) & ( for A, B being Element of CCosetSet M
for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
b2 . (A,B) = a.e-Ceq-class ((a + b),M) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines addCCoset LPSPACC1:def 16 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being BinOp of () holds
( b4 = addCCoset M iff for A, B being Element of CCosetSet M
for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
b4 . (A,B) = a.e-Ceq-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 zeroCCoset M -> Element of CCosetSet M equals :: LPSPACC1:def 17
a.e-Ceq-class ((),M);
correctness
coherence
a.e-Ceq-class ((),M) is Element of CCosetSet M
;
proof end;
end;

:: deftheorem defines zeroCCoset LPSPACC1:def 17 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds zeroCCoset M = a.e-Ceq-class ((),M);

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func lmultCCoset M -> Function of [:COMPLEX,():],() means :Def18: :: LPSPACC1:def 18
for z being Complex
for A being Element of CCosetSet M
for f being PartFunc of X,COMPLEX st f in A holds
it . (z,A) = a.e-Ceq-class ((z (#) f),M);
existence
ex b1 being Function of [:COMPLEX,():],() st
for z being Complex
for A being Element of CCosetSet M
for f being PartFunc of X,COMPLEX st f in A holds
b1 . (z,A) = a.e-Ceq-class ((z (#) f),M)
proof end;
uniqueness
for b1, b2 being Function of [:COMPLEX,():],() st ( for z being Complex
for A being Element of CCosetSet M
for f being PartFunc of X,COMPLEX st f in A holds
b1 . (z,A) = a.e-Ceq-class ((z (#) f),M) ) & ( for z being Complex
for A being Element of CCosetSet M
for f being PartFunc of X,COMPLEX st f in A holds
b2 . (z,A) = a.e-Ceq-class ((z (#) f),M) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines lmultCCoset LPSPACC1:def 18 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being Function of [:COMPLEX,():],() holds
( b4 = lmultCCoset M iff for z being Complex
for A being Element of CCosetSet M
for f being PartFunc of X,COMPLEX st f in A holds
b4 . (z,A) = a.e-Ceq-class ((z (#) f),M) );

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
existence
ex b1 being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct st
( the carrier of b1 = CCosetSet M & the addF of b1 = addCCoset M & 0. b1 = zeroCCoset M & the Mult of b1 = lmultCCoset M )
proof end;
uniqueness
for b1, b2 being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct st the carrier of b1 = CCosetSet M & the addF of b1 = addCCoset M & 0. b1 = zeroCCoset M & the Mult of b1 = lmultCCoset M & the carrier of b2 = CCosetSet M & the addF of b2 = addCCoset M & 0. b2 = zeroCCoset M & the Mult of b2 = lmultCCoset M holds
b1 = b2
;
end;

:: deftheorem Def19 defines Pre-L-CSpace LPSPACC1:def 19 :
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 Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct holds
( b4 = Pre-L-CSpace M iff ( the carrier of b4 = CCosetSet M & the addF of b4 = addCCoset M & 0. b4 = zeroCCoset M & the Mult of b4 = lmultCCoset M ) );

theorem Th36: :: LPSPACC1: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,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M & f a.e.cpfunc= g,M holds
Integral (M,f) = Integral (M,g)
proof end;

theorem Th37: :: LPSPACC1:37
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,COMPLEX st f is_integrable_on M holds
( Integral (M,f) in COMPLEX & Integral (M,|.f.|) in REAL & |.f.| is_integrable_on M )
proof end;

theorem Th38: :: LPSPACC1:38
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,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M & f a.e.cpfunc= g,M holds
( |.f.| a.e.= |.g.|,M & Integral (M,|.f.|) = Integral (M,|.g.|) )
proof end;

theorem Th39: :: LPSPACC1: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,COMPLEX st ex x being VECTOR of () st
( f in x & g in x ) holds
( f a.e.cpfunc= g,M & f in L1_CFunctions M & g in L1_CFunctions M )
proof end;

theorem Th40: :: LPSPACC1:40
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S ex NORM being Function of the carrier of (),REAL st
for x being Point of () ex f being PartFunc of X,COMPLEX st
( f in x & NORM . x = Integral (M,(abs f)) )
proof end;

theorem Th41: :: LPSPACC1:41
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,COMPLEX
for x being Point of () st f in x holds
( f is_integrable_on M & f in L1_CFunctions M & abs f is_integrable_on M )
proof end;

theorem Th42: :: LPSPACC1: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,COMPLEX
for x being Point of () st f in x & g in x holds
( f a.e.cpfunc= g,M & Integral (M,f) = Integral (M,g) & Integral (M,(abs f)) = Integral (M,(abs g)) )
proof end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func L-1-CNorm M -> Function of the carrier of (),REAL means :Def20: :: LPSPACC1:def 20
for x being Point of () ex f being PartFunc of X,COMPLEX st
( f in x & it . x = Integral (M,(abs f)) );
existence
ex b1 being Function of the carrier of (),REAL st
for x being Point of () ex f being PartFunc of X,COMPLEX st
( f in x & b1 . x = Integral (M,(abs f)) )
by Th40;
uniqueness
for b1, b2 being Function of the carrier of (),REAL st ( for x being Point of () ex f being PartFunc of X,COMPLEX st
( f in x & b1 . x = Integral (M,(abs f)) ) ) & ( for x being Point of () ex f being PartFunc of X,COMPLEX st
( f in x & b2 . x = Integral (M,(abs f)) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines L-1-CNorm LPSPACC1:def 20 :
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 (),REAL holds
( b4 = L-1-CNorm M iff for x being Point of () ex f being PartFunc of X,COMPLEX st
( f in x & 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-CSpace M -> non empty CNORMSTR equals :: LPSPACC1:def 21
CNORMSTR(# the carrier of (), the ZeroF of (), the addF of (), the Mult of (),() #);
coherence
CNORMSTR(# the carrier of (), the ZeroF of (), the addF of (), the Mult of (),() #) is non empty CNORMSTR
;
end;

:: deftheorem defines L-1-CSpace LPSPACC1:def 21 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds L-1-CSpace M = CNORMSTR(# the carrier of (), the ZeroF of (), the addF of (), the Mult of (),() #);

theorem Th43: :: LPSPACC1:43
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for x being Point of () holds
( ex f being PartFunc of X,COMPLEX st
( f in L1_CFunctions M & x = a.e-Ceq-class (f,M) & = Integral (M,(abs f)) ) & ( for f being PartFunc of X,COMPLEX st f in x holds
Integral (M,(abs f)) = ) )
proof end;

theorem :: LPSPACC1: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,COMPLEX
for x being Point of () st f in x holds
( x = a.e-Ceq-class (f,M) & = Integral (M,(abs f)) )
proof end;

theorem Th45: :: LPSPACC1:45
for a being Complex
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,COMPLEX
for x, y being Point of () 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 :: LPSPACC1:46
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,COMPLEX st f in L1_CFunctions M & Integral (M,(abs f)) = 0 holds
f a.e.cpfunc= X --> 0c,M
proof end;

theorem Th47: :: LPSPACC1: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,COMPLEX st f in L1_CFunctions M & g in L1_CFunctions M holds
Integral (M,|.(f + g).|) <= (Integral (M,|.f.|)) + (Integral (M,|.g.|))
proof end;

registration
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
coherence
proof end;
end;