:: by Yasushige Watase , Noboru Endou and Yasunari Shidama

::

:: Received August 27, 2012

:: Copyright (c) 2012-2019 Association of Mizar Users

registration

let D be non empty set ;

let E be complex-membered set ;

coherence

for b_{1} being Element of PFuncs (D,E) holds b_{1} is complex-valued
;

end;
let E be complex-membered set ;

coherence

for b

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)

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

coherence

F1 - F2 is Element of PFuncs (D,COMPLEX)

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

coherence

F1 (#) F2 is Element of PFuncs (D,COMPLEX)

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

coherence

F1 /" F2 is Element of PFuncs (D,COMPLEX)

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

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)

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

definition

let V be non empty CLSStruct ;

let V1 be Subset of V;

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

for a being Complex

for v being VECTOR of V st v in V1 holds

a * v in V1;

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

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

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 ;

existence

ex b_{1} being non empty Subset of V st

( b_{1} is add-closed & b_{1} is multi-closed )

end;
existence

ex b

( b

proof end;

definition

let X be non empty CLSStruct ;

let X1 be non empty multi-closed Subset of X;

coherence

the Mult of X | [:COMPLEX,X1:] is Function of [:COMPLEX,X1:],X1;

end;
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 the Mult of X | [:COMPLEX,X1:];

coherence

the Mult of X | [:COMPLEX,X1:] is Function of [:COMPLEX,X1:],X1;

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

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 )

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 )

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 ;

ex b_{1} being BinOp of (PFuncs (A,COMPLEX)) st

for f, g being Element of PFuncs (A,COMPLEX) holds b_{1} . (f,g) = f (#) g

for b_{1}, b_{2} being BinOp of (PFuncs (A,COMPLEX)) st ( for f, g being Element of PFuncs (A,COMPLEX) holds b_{1} . (f,g) = f (#) g ) & ( for f, g being Element of PFuncs (A,COMPLEX) holds b_{2} . (f,g) = f (#) g ) holds

b_{1} = b_{2}

end;
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 for f, g being Element of PFuncs (A,COMPLEX) holds it . (f,g) = f (#) g;

ex b

for f, g being Element of PFuncs (A,COMPLEX) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines multcpfunc LPSPACC1:def 3 :

for A being non empty set

for b_{2} being BinOp of (PFuncs (A,COMPLEX)) holds

( b_{2} = multcpfunc A iff for f, g being Element of PFuncs (A,COMPLEX) holds b_{2} . (f,g) = f (#) g );

for A being non empty set

for b

( b

definition

let A be non empty set ;

ex b_{1} being Function of [:COMPLEX,(PFuncs (A,COMPLEX)):],(PFuncs (A,COMPLEX)) st

for a being Complex

for f being Element of PFuncs (A,COMPLEX) holds b_{1} . (a,f) = a (#) f

for b_{1}, b_{2} being Function of [:COMPLEX,(PFuncs (A,COMPLEX)):],(PFuncs (A,COMPLEX)) st ( for a being Complex

for f being Element of PFuncs (A,COMPLEX) holds b_{1} . (a,f) = a (#) f ) & ( for a being Complex

for f being Element of PFuncs (A,COMPLEX) holds b_{2} . (a,f) = a (#) f ) holds

b_{1} = b_{2}

end;
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 for a being Complex

for f being Element of PFuncs (A,COMPLEX) holds it . (a,f) = a (#) f;

ex b

for a being Complex

for f being Element of PFuncs (A,COMPLEX) holds b

proof end;

uniqueness for b

for f being Element of PFuncs (A,COMPLEX) holds b

for f being Element of PFuncs (A,COMPLEX) holds b

b

proof end;

:: deftheorem Def4 defines multcomplexcpfunc LPSPACC1:def 4 :

for A being non empty set

for b_{2} being Function of [:COMPLEX,(PFuncs (A,COMPLEX)):],(PFuncs (A,COMPLEX)) holds

( b_{2} = multcomplexcpfunc A iff for a being Complex

for f being Element of PFuncs (A,COMPLEX) holds b_{2} . (a,f) = a (#) f );

for A being non empty set

for b

( b

for f being Element of PFuncs (A,COMPLEX) holds b

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

definition

let D be non empty set ;

ex b_{1} being BinOp of (PFuncs (D,COMPLEX)) st

for F1, F2 being Element of PFuncs (D,COMPLEX) holds b_{1} . (F1,F2) = F1 + F2

for b_{1}, b_{2} being BinOp of (PFuncs (D,COMPLEX)) st ( for F1, F2 being Element of PFuncs (D,COMPLEX) holds b_{1} . (F1,F2) = F1 + F2 ) & ( for F1, F2 being Element of PFuncs (D,COMPLEX) holds b_{2} . (F1,F2) = F1 + F2 ) holds

b_{1} = b_{2}

end;
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 for F1, F2 being Element of PFuncs (D,COMPLEX) holds it . (F1,F2) = F1 + F2;

ex b

for F1, F2 being Element of PFuncs (D,COMPLEX) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines addcpfunc LPSPACC1:def 5 :

for D being non empty set

for b_{2} being BinOp of (PFuncs (D,COMPLEX)) holds

( b_{2} = addcpfunc D iff for F1, F2 being Element of PFuncs (D,COMPLEX) holds b_{2} . (F1,F2) = F1 + F2 );

for D being non empty set

for b

( b

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

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

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

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 ;

coherence

( addcpfunc A is commutative & addcpfunc A is associative )

end;
coherence

( addcpfunc A is commutative & addcpfunc A is associative )

proof end;

registration

let A be non empty set ;

coherence

( multcpfunc A is commutative & multcpfunc A is associative )

end;
coherence

( multcpfunc A is commutative & multcpfunc A is associative )

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)

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

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)

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)

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

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

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 ;

CLSStruct(# (PFuncs (A,COMPLEX)),(CPFuncZero A),(addcpfunc A),(multcomplexcpfunc A) #) is non empty CLSStruct ;

end;
func CLSp_PFunct A -> non empty CLSStruct equals :: LPSPACC1:def 8

CLSStruct(# (PFuncs (A,COMPLEX)),(CPFuncZero A),(addcpfunc A),(multcomplexcpfunc A) #);

coherence CLSStruct(# (PFuncs (A,COMPLEX)),(CPFuncZero A),(addcpfunc A),(multcomplexcpfunc A) #);

CLSStruct(# (PFuncs (A,COMPLEX)),(CPFuncZero A),(addcpfunc A),(multcomplexcpfunc A) #) is non empty CLSStruct ;

:: deftheorem defines CLSp_PFunct LPSPACC1:def 8 :

for A being non empty set holds CLSp_PFunct A = CLSStruct(# (PFuncs (A,COMPLEX)),(CPFuncZero A),(addcpfunc A),(multcomplexcpfunc A) #);

for A being non empty set holds CLSp_PFunct A = CLSStruct(# (PFuncs (A,COMPLEX)),(CPFuncZero A),(addcpfunc A),(multcomplexcpfunc A) #);

registration

let A be non empty set ;

( CLSp_PFunct A is strict & CLSp_PFunct A is Abelian & CLSp_PFunct A is add-associative & CLSp_PFunct A is right_zeroed & CLSp_PFunct A is vector-distributive & CLSp_PFunct A is scalar-distributive & CLSp_PFunct A is scalar-associative & CLSp_PFunct A is scalar-unital )

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

coherence ( CLSp_PFunct A is strict & CLSp_PFunct A is Abelian & CLSp_PFunct A is add-associative & CLSp_PFunct A is right_zeroed & CLSp_PFunct A is vector-distributive & CLSp_PFunct A is scalar-distributive & CLSp_PFunct A is scalar-associative & CLSp_PFunct A is scalar-unital )

proof end;

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

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;

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

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

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

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

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

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

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

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

( L1_CFunctions M is multi-closed & L1_CFunctions M is add-closed ) by Lm5;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

coherence

( L1_CFunctions M is multi-closed & L1_CFunctions M is add-closed ) by Lm5;

definition

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

CLSStruct(# (L1_CFunctions M),(In ((0. (CLSp_PFunct X)),(L1_CFunctions M))),(add| ((L1_CFunctions M),(CLSp_PFunct X))),(Mult_ (L1_CFunctions M)) #) is non empty CLSStruct ;

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

coherence CLSStruct(# (L1_CFunctions M),(In ((0. (CLSp_PFunct X)),(L1_CFunctions M))),(add| ((L1_CFunctions M),(CLSp_PFunct X))),(Mult_ (L1_CFunctions M)) #);

CLSStruct(# (L1_CFunctions M),(In ((0. (CLSp_PFunct X)),(L1_CFunctions M))),(add| ((L1_CFunctions M),(CLSp_PFunct X))),(Mult_ (L1_CFunctions M)) #) is non empty CLSStruct ;

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

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S holds CLSp_L1Funct M = CLSStruct(# (L1_CFunctions M),(In ((0. (CLSp_PFunct X)),(L1_CFunctions M))),(add| ((L1_CFunctions M),(CLSp_PFunct X))),(Mult_ (L1_CFunctions M)) #);

registration

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

( CLSp_L1Funct M is strict & CLSp_L1Funct M is Abelian & CLSp_L1Funct M is add-associative & CLSp_L1Funct M is right_zeroed & CLSp_L1Funct M is vector-distributive & CLSp_L1Funct M is scalar-distributive & CLSp_L1Funct M is scalar-associative & CLSp_L1Funct M is scalar-unital )

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

coherence ( CLSp_L1Funct M is strict & CLSp_L1Funct M is Abelian & CLSp_L1Funct M is add-associative & CLSp_L1Funct M is right_zeroed & CLSp_L1Funct M is vector-distributive & CLSp_L1Funct M is scalar-distributive & CLSp_L1Funct M is scalar-associative & CLSp_L1Funct M is scalar-unital )

proof 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

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

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;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let f, g be PartFunc of X,COMPLEX;

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

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

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

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 ;

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

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

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

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;

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

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

coherence { f where f is PartFunc of X,COMPLEX : ( f in L1_CFunctions M & f a.e.cpfunc= X --> 0c,M ) } ;

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

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

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) + (X --> 0c) = X --> 0c & a (#) (X --> 0c) = X --> 0c )

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;

coherence

( AlmostZeroCFunctions M is add-closed & AlmostZeroCFunctions M is multi-closed ) by Lm6;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

coherence

( AlmostZeroCFunctions M is add-closed & AlmostZeroCFunctions M is multi-closed ) by Lm6;

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 )

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;

CLSStruct(# (AlmostZeroCFunctions M),(In ((0. (CLSp_L1Funct M)),(AlmostZeroCFunctions M))),(add| ((AlmostZeroCFunctions M),(CLSp_L1Funct M))),(Mult_ (AlmostZeroCFunctions M)) #) is non empty CLSStruct ;

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

coherence CLSStruct(# (AlmostZeroCFunctions M),(In ((0. (CLSp_L1Funct M)),(AlmostZeroCFunctions M))),(add| ((AlmostZeroCFunctions M),(CLSp_L1Funct M))),(Mult_ (AlmostZeroCFunctions M)) #);

CLSStruct(# (AlmostZeroCFunctions M),(In ((0. (CLSp_L1Funct M)),(AlmostZeroCFunctions M))),(add| ((AlmostZeroCFunctions M),(CLSp_L1Funct M))),(Mult_ (AlmostZeroCFunctions M)) #) is non empty CLSStruct ;

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

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S holds CLSp_AlmostZeroFunct M = CLSStruct(# (AlmostZeroCFunctions M),(In ((0. (CLSp_L1Funct M)),(AlmostZeroCFunctions M))),(add| ((AlmostZeroCFunctions M),(CLSp_L1Funct M))),(Mult_ (AlmostZeroCFunctions M)) #);

registration

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

( CLSp_L1Funct M is strict & CLSp_L1Funct M is Abelian & CLSp_L1Funct M is add-associative & CLSp_L1Funct M is right_zeroed & CLSp_L1Funct M is vector-distributive & CLSp_L1Funct M is scalar-distributive & CLSp_L1Funct M is scalar-associative & CLSp_L1Funct M is scalar-unital ) ;

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

coherence ( CLSp_L1Funct M is strict & CLSp_L1Funct M is Abelian & CLSp_L1Funct M is add-associative & CLSp_L1Funct M is right_zeroed & CLSp_L1Funct M is vector-distributive & CLSp_L1Funct M is scalar-distributive & CLSp_L1Funct M is scalar-associative & CLSp_L1Funct M is scalar-unital ) ;

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

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;

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

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

correctness { g where g is PartFunc of X,COMPLEX : ( g in L1_CFunctions M & f in L1_CFunctions M & f a.e.cpfunc= g,M ) } ;

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

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

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

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)

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 )

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

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)

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)

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;

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

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

correctness { (a.e-Ceq-class (f,M)) where f is PartFunc of X,COMPLEX : f in L1_CFunctions M } ;

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

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

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;

ex b_{1} being BinOp of (CCosetSet M) 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

b_{1} . (A,B) = a.e-Ceq-class ((a + b),M)

for b_{1}, b_{2} being BinOp of (CCosetSet M) 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

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

b_{2} . (A,B) = a.e-Ceq-class ((a + b),M) ) holds

b_{1} = b_{2}

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

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

ex b

for A, B being Element of CCosetSet M

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

b

proof end;

uniqueness for b

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

b

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

b

b

proof 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 b_{4} being BinOp of (CCosetSet M) holds

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

b_{4} . (A,B) = a.e-Ceq-class ((a + b),M) );

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for b

( b

for a, b being PartFunc of X,COMPLEX 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;

correctness

coherence

a.e-Ceq-class ((X --> 0c),M) is Element of CCosetSet M;

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

correctness

coherence

a.e-Ceq-class ((X --> 0c),M) is Element of CCosetSet M;

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

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

definition

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

ex b_{1} being Function of [:COMPLEX,(CCosetSet M):],(CCosetSet M) st

for z being Complex

for A being Element of CCosetSet M

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

b_{1} . (z,A) = a.e-Ceq-class ((z (#) f),M)

for b_{1}, b_{2} being Function of [:COMPLEX,(CCosetSet M):],(CCosetSet M) st ( for z being Complex

for A being Element of CCosetSet M

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

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

b_{2} . (z,A) = a.e-Ceq-class ((z (#) f),M) ) holds

b_{1} = b_{2}

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

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

ex b

for z being Complex

for A being Element of CCosetSet M

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

b

proof end;

uniqueness for b

for A being Element of CCosetSet M

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

b

for A being Element of CCosetSet M

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

b

b

proof 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 b_{4} being Function of [:COMPLEX,(CCosetSet M):],(CCosetSet M) holds

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

b_{4} . (z,A) = a.e-Ceq-class ((z (#) f),M) );

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for b

( b

for A being Element of CCosetSet M

for f being PartFunc of X,COMPLEX 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;

ex b_{1} being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct st

( the carrier of b_{1} = CCosetSet M & the addF of b_{1} = addCCoset M & 0. b_{1} = zeroCCoset M & the Mult of b_{1} = lmultCCoset M )

for b_{1}, b_{2} being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct st the carrier of b_{1} = CCosetSet M & the addF of b_{1} = addCCoset M & 0. b_{1} = zeroCCoset M & the Mult of b_{1} = lmultCCoset M & the carrier of b_{2} = CCosetSet M & the addF of b_{2} = addCCoset M & 0. b_{2} = zeroCCoset M & the Mult of b_{2} = lmultCCoset M holds

b_{1} = b_{2}
;

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

existence ( the carrier of it = CCosetSet M & the addF of it = addCCoset M & 0. it = zeroCCoset M & the Mult of it = lmultCCoset M );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: 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 b_{4} being non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct holds

( b_{4} = Pre-L-CSpace M iff ( the carrier of b_{4} = CCosetSet M & the addF of b_{4} = addCCoset M & 0. b_{4} = zeroCCoset M & the Mult of b_{4} = lmultCCoset M ) );

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for b

( b

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)

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 )

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

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

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

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 )

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

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;

ex b_{1} 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 & b_{1} . x = Integral (M,(abs f)) )
by Th40;

uniqueness

for b_{1}, b_{2} 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 & b_{1} . x = Integral (M,(abs f)) ) ) & ( for x being Point of (Pre-L-CSpace M) ex f being PartFunc of X,COMPLEX st

( f in x & b_{2} . x = Integral (M,(abs f)) ) ) holds

b_{1} = b_{2}

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

ex b

for x being Point of (Pre-L-CSpace M) ex f being PartFunc of X,COMPLEX st

( f in x & b

uniqueness

for b

( f in x & b

( f in x & b

b

proof 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 b_{4} being Function of the carrier of (Pre-L-CSpace M),REAL holds

( b_{4} = L-1-CNorm M iff for x being Point of (Pre-L-CSpace M) ex f being PartFunc of X,COMPLEX st

( f in x & b_{4} . x = Integral (M,(abs f)) ) );

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for b

( b

( f in x & b

definition

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

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) #) is non empty CNORMSTR ;

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

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

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) #) is non empty CNORMSTR ;

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

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

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

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

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

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

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

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;

( L-1-CSpace M is ComplexNormSpace-like & L-1-CSpace M is vector-distributive & L-1-CSpace M is scalar-distributive & L-1-CSpace M is scalar-associative & L-1-CSpace M is scalar-unital & L-1-CSpace M is Abelian & L-1-CSpace M is add-associative & L-1-CSpace M is right_zeroed & L-1-CSpace M is right_complementable )

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

coherence ( L-1-CSpace M is ComplexNormSpace-like & L-1-CSpace M is vector-distributive & L-1-CSpace M is scalar-distributive & L-1-CSpace M is scalar-associative & L-1-CSpace M is scalar-unital & L-1-CSpace M is Abelian & L-1-CSpace M is add-associative & L-1-CSpace M is right_zeroed & L-1-CSpace M is right_complementable )

proof end;