LPSPACC1: On $L^1$ Space Formed by Complex-valued Partial Functions

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

proof end;

:: original: -
redefine func F1 - F2 -> Element of PFuncs (D,COMPLEX);
coherence

proof end;

:: original: (#)
redefine func F1 (#) F2 -> Element of PFuncs (D,COMPLEX);
coherence

proof end;

:: original: /"
redefine func F1 /" F2 -> Element of PFuncs (D,COMPLEX);
coherence

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

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 :

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 Element of bool the carrier of V;

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:];

proof end;

end;

:: deftheorem defines Mult_ LPSPACC1:def 2 :

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;

proof end;

proof end;

end;

:: deftheorem Def3 defines multcpfunc LPSPACC1:def 3 :

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;

proof end;

proof end;

end;

:: deftheorem Def4 defines multcomplexcpfunc LPSPACC1:def 4 :

:: Newly Define addcpfunc instead of addpfunc(D) of RFUNCT_3:def 4

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;

proof end;

proof end;

end;

:: deftheorem Def5 defines addcpfunc LPSPACC1:def 5 :

definition

let A be set ;

func CPFuncZero A -> Element of PFuncs (A,COMPLEX) equals :: LPSPACC1:def 6
A --> 0c;

coherence by PARTFUN1:45;

end;

:: deftheorem defines CPFuncZero LPSPACC1:def 6 :

definition

let A be set ;

func CPFuncUnit A -> Element of PFuncs (A,COMPLEX) equals :: LPSPACC1:def 7
A --> 1r;

coherence by PARTFUN1:45;

end;

:: deftheorem defines CPFuncUnit LPSPACC1:def 7 :

theorem Th4: :: LPSPACC1:4

for A being non empty set
for f, g, h being Element of PFuncs (A,COMPLEX) holds
( h = (addcpfunc 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) ) ) )

proof end;

theorem Th5: :: LPSPACC1:5

for A being non empty set
for f, g, h being Element of PFuncs (A,COMPLEX) holds
( h = (multcpfunc 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) ) ) )

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 = (multcomplexcpfunc A) . (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 ;

cluster addcpfunc A -> commutative associative ;

proof end;

end;

registration

let A be non empty set ;

cluster multcpfunc A -> commutative associative ;

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 (addcpfunc A) . (f,((multcomplexcpfunc A) . ((- 1r),f))) = (CPFuncZero A) | (dom f)

proof end;

theorem Th11: :: LPSPACC1:11

for A being non empty set
for f being Element of PFuncs (A,COMPLEX) holds (multcomplexcpfunc A) . (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 (multcomplexcpfunc A) . (a,((multcomplexcpfunc A) . (b,f))) = (multcomplexcpfunc A) . ((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 (addcpfunc A) . (((multcomplexcpfunc A) . (a,f)),((multcomplexcpfunc A) . (b,f))) = (multcomplexcpfunc A) . ((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 (addcpfunc A) . (((multcomplexcpfunc A) . (a,f)),((multcomplexcpfunc A) . (a,g))) = (multcomplexcpfunc A) . (a,((addcpfunc 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 (multcpfunc A) . (f,((addcpfunc A) . (g,h))) = (addcpfunc A) . (((multcpfunc A) . (f,g)),((multcpfunc A) . (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 (multcpfunc A) . (((multcomplexcpfunc A) . (a,f)),g) = (multcomplexcpfunc A) . (a,((multcpfunc 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)),(CPFuncZero A),(addcpfunc A),(multcomplexcpfunc A) #);

end;

:: deftheorem defines CLSp_PFunct LPSPACC1:def 8 :

registration

let A be non empty set ;

cluster CLSp_PFunct A -> non empty Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

proof end;

end;

registration

let X be non empty set ;
let f be PartFunc of X,COMPLEX;

cluster |.f.| -> nonnegative ;

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 (CLSp_PFunct X) 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 ) } ;

proof end;

end;

:: deftheorem defines L1_CFunctions LPSPACC1:def 9 :

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;

cluster L1_CFunctions M -> non empty add-closed multi-closed ;

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(# (L1_CFunctions M),(In ((0. (CLSp_PFunct X)),(L1_CFunctions M))),(add| ((L1_CFunctions M),(CLSp_PFunct X))),(Mult_ (L1_CFunctions M)) #);

end;

:: deftheorem defines CLSp_L1Funct LPSPACC1:def 10 :

registration

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

cluster CLSp_L1Funct M -> non empty Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

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 (CLSp_L1Funct M) 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 (CLSp_L1Funct M) 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 :

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 (CLSp_L1Funct M) st f = u holds
( u + ((- 1r) * u) = (X --> 0c) | (dom f) & ex v, g being PartFunc of X,COMPLEX st
( v in L1_CFunctions M & g in L1_CFunctions M & v = u + ((- 1r) * 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 (CLSp_L1Funct M) equals :: LPSPACC1:def 12
{ f where f is PartFunc of X,COMPLEX : ( f in L1_CFunctions M & f a.e.cpfunc= X --> 0c,M ) } ;

proof end;

end;

:: deftheorem defines AlmostZeroCFunctions LPSPACC1:def 12 :

theorem Th27: :: LPSPACC1:27

for a being Complex
for X being non empty set holds
( (X --> 0c) + (X --> 0c) = X --> 0c & a (#) (X --> 0c) = 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;

cluster AlmostZeroCFunctions M -> non empty add-closed multi-closed ;

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. (CLSp_L1Funct M) = X --> 0c & 0. (CLSp_L1Funct M) 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(# (AlmostZeroCFunctions M),(In ((0. (CLSp_L1Funct M)),(AlmostZeroCFunctions M))),(add| ((AlmostZeroCFunctions M),(CLSp_L1Funct M))),(Mult_ (AlmostZeroCFunctions M)) #);

end;

:: deftheorem defines CLSp_AlmostZeroFunct LPSPACC1:def 13 :

registration

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

cluster CLSp_L1Funct M -> non empty Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

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 (CLSp_AlmostZeroFunct M) 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 (L1_CFunctions M) 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 ) } ;

proof end;

end;

:: deftheorem defines a.e-Ceq-class LPSPACC1:def 14 :

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

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 (L1_CFunctions M) equals :: LPSPACC1:def 15
{ (a.e-Ceq-class (f,M)) where f is PartFunc of X,COMPLEX : f in L1_CFunctions M } ;

proof end;

end;

:: deftheorem defines CCosetSet LPSPACC1:def 15 :

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

proof end;

proof end;

end;

:: deftheorem Def16 defines addCCoset LPSPACC1:def 16 :

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 ((X --> 0c),M);

proof end;

end;

:: deftheorem defines zeroCCoset LPSPACC1:def 17 :

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,(CCosetSet M):],(CCosetSet M) 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);

proof end;

proof end;

end;

:: deftheorem Def18 defines lmultCCoset LPSPACC1:def 18 :

definition

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

func Pre-L-CSpace M -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct means :Def19: :: LPSPACC1:def 19
( the carrier of it = CCosetSet M & the addF of it = addCCoset M & 0. it = zeroCCoset M & the Mult of it = lmultCCoset M );

proof end;

uniqueness ;

end;

:: deftheorem Def19 defines Pre-L-CSpace LPSPACC1:def 19 :

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

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 (Pre-L-CSpace M) 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 (Pre-L-CSpace M),REAL st
for x being Point of (Pre-L-CSpace M) 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 (Pre-L-CSpace M) 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 (Pre-L-CSpace M) 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 (Pre-L-CSpace M),REAL means :Def20: :: LPSPACC1:def 20
for x being Point of (Pre-L-CSpace M) ex f being PartFunc of X,COMPLEX st
( f in x & it . x = Integral (M,(abs f)) );

existence by Th40;
uniqueness

proof end;

end;

:: deftheorem Def20 defines L-1-CNorm LPSPACC1:def 20 :

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 (Pre-L-CSpace M), the ZeroF of (Pre-L-CSpace M), the addF of (Pre-L-CSpace M), the Mult of (Pre-L-CSpace M),(L-1-CNorm M) #);

end;

:: deftheorem defines L-1-CSpace LPSPACC1:def 21 :

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 (L-1-CSpace M) holds
( ex f being PartFunc of X,COMPLEX st
( f in L1_CFunctions M & x = a.e-Ceq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,COMPLEX st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )

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 (L-1-CSpace M) st f in x holds
( x = a.e-Ceq-class (f,M) & ||.x.|| = 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 (L-1-CSpace M) 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;

cluster L-1-CSpace M -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;