:: On $L^1$ Space Formed by Complex-valued Partial Functions
:: by Yasushige Watase , Noboru Endou and Yasunari Shidama
::
:: Received August 27, 2012
:: Copyright (c) 2012-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, RLVECT_1, SUBSET_1, RELAT_1, RLSUB_1, IDEAL_1,
ARYTM_3, STRUCT_0, RSSPACE, FUNCT_1, ZFMISC_1, TARSKI, BINOP_1, SUPINF_2,
ALGSTR_0, REALSET1, FUNCT_7, PARTFUN1, VALUED_0, VALUED_1, FUNCOP_1,
CARD_1, ARYTM_1, PROB_1, MEASURE1, MEMBERED, INTEGRA5, MESFUNC5, REAL_1,
XXREAL_0, MESFUNC1, MEASURE6, SETFAM_1, COMPLEX1, PRE_TOPC, NORMSP_1,
LPSPACE1, CLVECT_1, LPSPACC1, XCMPLX_0, SQUARE_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, SETFAM_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, REALSET1,
NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_3, XREAL_0, SQUARE_1, MEMBERED,
VALUED_0, COMPLEX1, COMSEQ_3, VALUED_1, CFUNCT_1, SUPINF_2, PROB_1,
MEASURE1, RFUNCT_3, MEASURE6, EXTREAL1, MESFUNC1, MESFUNC5, MESFUNC6,
MESFUN6C, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, NORMSP_0, IDEAL_1,
CLVECT_1, LPSPACE1;
constructors COMPLEX1, EXTREAL1, CLVECT_1, CFUNCT_1, IDEAL_1, SQUARE_1,
MEASURE6, MESFUNC2, MESFUNC5, MESFUNC6, SUPINF_1, REALSET1, MESFUNC1,
RELSET_1, BINOP_2, MESFUN6C, LPSPACE2, COMSEQ_3;
registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, MEMBERED, PARTFUN1,
SQUARE_1, VALUED_0, SUBSET_1, XCMPLX_0, STRUCT_0, MEASURE1, XXREAL_3,
CLVECT_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, BINOP_1, ALGSTR_0, RLVECT_1, CLVECT_1;
equalities REALSET1, BINOP_1, STRUCT_0, ALGSTR_0, IDEAL_1, MESFUNC5, MESFUNC6,
SUBSET_1, SQUARE_1, CLVECT_1, LPSPACE1, NORMSP_0;
expansions TARSKI, BINOP_1, RLVECT_1, IDEAL_1, MESFUNC5, MESFUNC6, CLVECT_1;
theorems FUNCT_1, FUNCT_2, PARTFUN1, COMPLEX1, XBOOLE_0, TARSKI, RELAT_1,
VALUED_1, ZFMISC_1, RLVECT_1, FUNCOP_1, XBOOLE_1, BINOP_1, VALUED_0,
MEASURE1, MESFUNC6, RFUNCT_1, CLVECT_1, XCMPLX_0, MESFUN6C, MESFUN7C,
LPSPACE1, CFUNCT_1, SQUARE_1, XREAL_1, CSSPACE3, SUBSET_1, COMSEQ_3;
schemes BINOP_1, FUNCT_2;
begin :: Preliminaries of Complex Linear Space
registration
let D be non empty set, E be complex-membered set;
cluster -> complex-valued for Element of PFuncs(D,E);
coherence;
end;
definition
let D be non empty set, E be complex-membered set,
F1,F2 be Element of PFuncs(D,E);
redefine func F1+F2 -> Element of PFuncs(D,COMPLEX); :: redefines + (VALUED_1, definition)
coherence
proof
reconsider F1,F2 as PartFunc of D,E;
F1+F2 is PartFunc of D,COMPLEX;
hence thesis by PARTFUN1:45;
end;
redefine func F1-F2 -> Element of PFuncs(D,COMPLEX); :: redefines - (VALUED_1, definition)
coherence
proof
reconsider F1,F2 as PartFunc of D,E;
F1-F2 is PartFunc of D,COMPLEX;
hence thesis by PARTFUN1:45;
end;
redefine func F1(#)F2 -> Element of PFuncs(D,COMPLEX); :: redefines (#) (VALUED_1, definition)
coherence
proof
reconsider F1,F2 as PartFunc of D,E;
F1(#)F2 is PartFunc of D,COMPLEX;
hence thesis by PARTFUN1:45;
end;
redefine func F1 /" F2 -> Element of PFuncs(D,COMPLEX); :: redefines /" (VALUED_1, definition)
coherence
proof
reconsider F1,F2 as PartFunc of D,E;
F1 /" F2 is PartFunc of D,COMPLEX;
hence thesis by PARTFUN1:45;
end;
end;
definition
let D be non empty set, E be complex-membered set,
F be Element of PFuncs(D,E), a be Complex;
redefine func a(#)F -> Element of PFuncs(D,COMPLEX); :: redefines (#) (VALUED_1, definition)
coherence
proof
reconsider F as PartFunc of D,E;
a(#)F is PartFunc of D,COMPLEX;
hence thesis by PARTFUN1:45;
end;
end;
definition
let V be non empty CLSStruct, V1 be Subset of V;
attr V1 is multi-closed means :Def1:
for a be Complex, v be VECTOR of V st v in V1 holds a*v in V1;
end;
theorem
for V be ComplexLinearSpace, V1 be Subset of V holds
V1 is linearly-closed iff V1 is add-closed multi-closed;
registration
let V be non empty CLSStruct;
cluster add-closed multi-closed for non empty Subset of V;
existence
proof
set M = the carrier of V;
for u being object holds u in M implies u in the carrier of V;
then reconsider M as Subset of V by TARSKI:def 3;
reconsider M as non empty Subset of V;
take M;
thus thesis;
end;
end;
definition
let X be non empty CLSStruct;
let X1 be multi-closed non empty Subset of X;
func Mult_X1 -> Function of [:COMPLEX,X1:], X1 equals
(the Mult of X) | [:COMPLEX, X1:];
correctness
proof
A1: [:COMPLEX,X1:] c= [:COMPLEX,the carrier of X:] & dom the Mult of X =
[:COMPLEX, the carrier of X:] by FUNCT_2:def 1,ZFMISC_1:95;
A2: now
let z be object;
assume
A3: z in [:COMPLEX,X1:];
then consider r,x be object such that
A4: r in COMPLEX and
A5: x in X1 and
A6: z=[r,x] by ZFMISC_1:def 2;
reconsider r as Complex by A4;
reconsider y=x as VECTOR of X by A5;
[r,x] in dom((the Mult of X)|[:COMPLEX,X1:]) by A1,A3,A6,RELAT_1:62;
then ((the Mult of X)|[:COMPLEX,X1:]).z = r*y by A6,FUNCT_1:47;
hence ((the Mult of X)|[:COMPLEX,X1:]).z in X1 by A5,Def1;
end;
dom((the Mult of X)|[:COMPLEX,X1:])=[:COMPLEX,X1:] by A1,RELAT_1:62;
hence thesis by A2,FUNCT_2:3;
end;
end;
reserve a,b,r for Complex;
reserve V for ComplexLinearSpace;
theorem Th2:
for V be Abelian add-associative right_zeroed
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty CLSStruct, V1 be non empty Subset of V, d1 be
Element of V1, A be BinOp of V1, M be 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 add-associative right_zeroed
vector-distributive scalar-distributive scalar-associative scalar-unital
proof
let V be Abelian add-associative right_zeroed vector-distributive
scalar-distributive scalar-associative scalar-unital non
empty CLSStruct, V1 be non empty Subset of V, d1 be Element of V1, A be BinOp
of V1, M be Function of [:COMPLEX,V1:],V1;
set D = V1;
assume that
A1: d1 = 0.V and
A2: A = (the addF of V)||V1 and
A3: M = (the Mult of V)|[:COMPLEX,V1:];
set W = CLSStruct(# D,d1,A,M #);
A4: now let a;
let x be VECTOR of W;
reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;
thus a * x = (the Mult of V).[a1,x] by A3,FUNCT_1:49
.= (the Mult of V).(a,x);
end;
A5: now
let x,y be VECTOR of W;
thus x + y = (the addF of V).[x,y] by A2,FUNCT_1:49
.= (the addF of V).(x,y);
end;
W is Abelian add-associative right_zeroed vector-distributive
scalar-distributive scalar-associative scalar-unital
proof
set Mv = the Mult of V;
set Av = the addF of V;
hereby
let x,y be VECTOR of W;
reconsider x1 = x, y1 = y as VECTOR of V by TARSKI:def 3;
thus x + y = x1 + y1 by A5
.= y1 + x1
.= y + x by A5;
end;
now
let x,y,z be VECTOR of W;
reconsider x1 = x, y1 = y, z1 = z as VECTOR of V by TARSKI:def 3;
thus (x + y) + z = Av.(x + y,z1) by A5
.= (x1 + y1) + z1 by A5
.= x1 + (y1 + z1) by RLVECT_1:def 3
.= Av.(x1,y + z) by A5
.= x + (y + z) by A5;
end;
hence W is add-associative;
now
let x be VECTOR of W;
reconsider y = x as VECTOR of V by TARSKI:def 3;
thus x + 0.W = y + 0.V by A1,A5
.= x by RLVECT_1:def 4;
end;
hence W is right_zeroed;
hereby
let a1 be Complex;
let x,y be VECTOR of W;
reconsider a=a1 as Element of COMPLEX by XCMPLX_0:def 2;
reconsider x1 = x, y1 = y as VECTOR of V by TARSKI:def 3;
a * (x + y) = Mv.(a,x + y) by A4
.= a * (x1 + y1) by A5
.= a * x1 + a * y1 by CLVECT_1:def 2
.= Av.(Mv.(a,x),Mv.(a,y))
.= Av.(Mv.(a,x),a*y) by A4
.= Av.(a * x, a * y) by A4
.= a * x + a * y by A5;
hence a1 * (x + y)= a1 * x + a1 * y;
end;
hereby
let a1,b1 be Complex;
let x be VECTOR of W;
reconsider a=a1,b=b1 as Element of COMPLEX by XCMPLX_0:def 2;
reconsider y = x as VECTOR of V by TARSKI:def 3;
(a + b) * x = Mv.(a+b,x) by A4
.= (a + b) * y
.= a * y + b * y by CLVECT_1:def 3
.= Av.(Mv.(a,y),Mv.(b,y))
.= Av.(Mv.(a,x),b * x) by A4
.= Av.(a * x,b * x) by A4
.= a * x + b * x by A5;
hence (a1 + b1) * x= a1 * x + b1 * x;
end;
hereby
let a1,b1 be Complex;
let x be VECTOR of W;
reconsider a=a1,b=b1 as Element of COMPLEX by XCMPLX_0:def 2;
reconsider y = x as VECTOR of V by TARSKI:def 3;
(a * b) * x = Mv.(a*b, x) by A4
.= (a * b) * y
.= a * (b * y) by CLVECT_1:def 4
.= Mv.(a,Mv.(b,y))
.= Mv.(a,b * x) by A4
.= a * (b * x) by A4;
hence (a1 * b1) * x= a1 * (b1 * x);
end;
let x be VECTOR of W;
reconsider y = x as VECTOR of V by TARSKI:def 3;
thus 1r * x = Mv.(1r,x) by A4.= 1r * y
.= x by CLVECT_1:def 5;
end;
hence thesis;
end;
theorem Th3:
for V be Abelian add-associative right_zeroed
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty CLSStruct, V1 be add-closed multi-closed non
empty Subset of V st 0.V in V1 holds CLSStruct (# V1,In (0.V, V1), add|(V1,V),
Mult_ V1 #) is Abelian add-associative right_zeroed vector-distributive
scalar-distributive scalar-associative scalar-unital
proof
let V be Abelian add-associative right_zeroed vector-distributive
scalar-distributive scalar-associative scalar-unital non
empty CLSStruct, V1 be add-closed multi-closed non empty Subset of V;
assume 0.V in V1;
then In(0.V,V1) = 0.V by SUBSET_1:def 8;
hence thesis by Th2;
end;
begin :: Quasi-Complex Linear Space of Partial Functions
reserve A,B for non empty set;
reserve f,g,h for Element of PFuncs(A,COMPLEX);
definition
let A;
func multcpfunc A -> BinOp of PFuncs(A,COMPLEX) means
:Def3:
for f,g being Element of PFuncs(A,COMPLEX) holds it.(f,g) = f(#)g;
existence
proof
deffunc F(Element of PFuncs(A,COMPLEX),Element of PFuncs(A,COMPLEX))
= $1(#)$2;
ex F being BinOp of PFuncs(A,COMPLEX) st for f,g holds F.(f,g) = F(f,g)
from BINOP_1:sch 4;
hence thesis;
end;
uniqueness
proof
let it1,it2 be BinOp of PFuncs(A,COMPLEX) such that
A1: for f,g holds it1.(f,g) = f(#)g and
A2: for f,g holds it2.(f,g) = f(#)g;
now
let f,g;
thus it1.(f,g) = f(#)g by A1
.=it2.(f,g) by A2;
end;
hence thesis;
end;
end;
definition
let A;
func multcomplexcpfunc A -> Function of
[:COMPLEX,PFuncs(A,COMPLEX):],PFuncs(A,COMPLEX) means :Def4:
for a being Complex, f being Element of PFuncs(A,COMPLEX)
holds it.(a,f) = a(#)f;
existence
proof
deffunc FG(Complex,Element of PFuncs(A,COMPLEX)) = $1(#)$2;
consider F being Function of [:COMPLEX,PFuncs(A,COMPLEX):],
PFuncs(A,COMPLEX) such that
A1: for a be Element of COMPLEX,f holds F.(a,f) = FG(a,f) from BINOP_1:sch 4;
take F;
let a;
a in COMPLEX by XCMPLX_0:def 2;
hence thesis by A1;
end;
uniqueness
proof
let it1,it2 be Function of [:COMPLEX,PFuncs(A,COMPLEX):],PFuncs(A,COMPLEX)
such that
A2: for a being Complex,f being Element of PFuncs(A,COMPLEX) holds
it1.(a,f) = a(#)f and
A3: for a being Complex, f being Element of PFuncs(A,COMPLEX)
holds it2.(a,f) = a(#)f;
now
let a be Element of COMPLEX, f be Element of PFuncs(A,COMPLEX);
thus it1.(a,f) = a(#)f by A2
.= it2.(a,f) by A3;
end;
hence thesis;
end;
end;
:: 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:
for F1,F2 be Element of PFuncs(D,COMPLEX) holds it.(F1,F2) = F1 + F2;
existence
proof
deffunc O(Element of PFuncs(D,COMPLEX),
Element of PFuncs(D,COMPLEX))= $1 + $2;
ex o being BinOp of PFuncs(D,COMPLEX) st
for a,b being Element of PFuncs(D,COMPLEX) holds o.(a,b) = O(a,b)
from BINOP_1:sch 4;
hence thesis;
end;
uniqueness
proof
let o1,o2 be BinOp of PFuncs(D,COMPLEX);
assume that
A1: for f1,f2 be Element of PFuncs(D,COMPLEX) holds o1.(f1,f2) = f1 + f2 and
A2: for f1,f2 be Element of PFuncs(D,COMPLEX) holds o2.(f1,f2) = f1 + f2;
now
let f1,f2 be Element of PFuncs(D,COMPLEX);
o1.(f1,f2) = f1 + f2 by A1;
hence o1.(f1,f2)=o2.(f1,f2) by A2;
end;
hence thesis;
end;
end;
definition
let A be set;
func CPFuncZero A -> Element of PFuncs(A,COMPLEX) equals
A --> 0c;
coherence by PARTFUN1:45;
end;
definition
let A be set;
func CPFuncUnit A -> Element of PFuncs(A,COMPLEX) equals
A --> 1r;
coherence by PARTFUN1:45;
end;
theorem Th4:
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
hereby
assume
A1: h = (addcpfunc A).(f,g);
then dom h = dom(f+g) by Def5;
hence dom h = dom f /\ dom g by VALUED_1:def 1;
let x be Element of A;
assume x in dom h; then
A2: x in dom (f+g) by A1,Def5;
h.x = (f+g).x by A1,Def5;
hence h.x = f.x + g.x by A2,VALUED_1:def 1;
end;
assume that
A3: dom h = dom f /\ dom g and
A4: for x being Element of A st x in dom h holds h.x=f.x + g.x;
set k=(addcpfunc A).(f,g);
A5: now
let x be Element of A;
A6: k.x = (f+g).x by Def5;
assume
A7: x in dom h;
then x in dom(f+g) by A3,VALUED_1:def 1;
hence k.x = f.x + g.x by A6,VALUED_1:def 1
.= h.x by A4,A7;
end;
dom k = dom (f+g) by Def5
.= dom h by A3,VALUED_1:def 1;
hence thesis by A5,PARTFUN1:5;
end;
theorem Th5:
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
set k=(multcpfunc A).(f,g);
hereby
assume
A1: h = (multcpfunc A).(f,g);
hence dom h = dom (f(#)g) by Def3
.= dom f /\ dom g by VALUED_1:def 4;
let x be Element of A;
assume x in dom h;
then
A2: x in dom (f(#)g) by A1,Def3;
h.x = (f(#)g).x by A1,Def3;
hence h.x = f.x * g.x by A2,VALUED_1:def 4;
end;
assume that
A3: dom h = dom f /\ dom g and
A4: for x being Element of A st x in dom h holds h.x=f.x * g.x;
A5: now
let x be Element of A;
A6: k.x = (f(#)g).x by Def3;
assume
A7: x in dom h;
then x in dom (f(#)g) by A3,VALUED_1:def 4;
hence k.x = f.x * g.x by A6,VALUED_1:def 4
.= h.x by A4,A7;
end;
dom k = dom(f(#)g) by Def3
.= dom h by A3,VALUED_1:def 4;
hence thesis by A5,PARTFUN1:5;
end;
theorem
CPFuncZero A <> CPFuncUnit A
proof
(CPFuncUnit A).the Element of A = 1 by COMPLEX1:def 4,FUNCOP_1:7;
hence thesis by FUNCOP_1:7;
end;
theorem Th7:
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
hereby
assume
A1: h = (multcomplexcpfunc A).(a,f);
then dom h = dom(a(#)f) by Def4;
hence dom h = dom f by VALUED_1:def 5;
let x be Element of A;
assume x in dom f;
then x in dom(a(#)f) by VALUED_1:def 5;
then (a(#)f).x = a*(f.x) by VALUED_1:def 5;
hence h.x = a*(f.x) by A1,Def4;
end;
hereby
reconsider a1=a as Element of COMPLEX by XCMPLX_0:def 2;
reconsider k= (multcomplexcpfunc A).(a1,f) as Element of PFuncs(A,COMPLEX);
assume that
A2: dom f = dom h and
A3: for x being Element of A st x in dom f holds h.x = a*f.x;
A4: now
let x be Element of A;
assume
A5: x in dom f;
then x in dom(a(#)f) by VALUED_1:def 5;
then (a(#)f).x = a * f.x by VALUED_1:def 5;
then (a(#)f).x = h.x by A3,A5;
hence k.x = h.x by Def4;
end;
k = a(#)f by Def4;
then dom k = dom f by VALUED_1:def 5;
hence h = (multcomplexcpfunc A).(a,f) by A2,A4,PARTFUN1:5;
end;
end;
registration
let A;
cluster addcpfunc(A) -> commutative associative;
coherence
proof
set o=addcpfunc(A);
hereby
let F1,F2 be Element of PFuncs(A,COMPLEX);
thus o.(F1,F2) = F2+F1 by Def5
.= o.(F2,F1) by Def5;
end;
let F1,F2,F3 be Element of PFuncs(A,COMPLEX);
thus o.(F1,o.(F2,F3))
= F1 + o.(F2,F3) by Def5
.= F1+ (F2+F3) by Def5
.= F1+F2+F3 by RFUNCT_1:8
.= o.(F1,F2) + F3 by Def5
.= o.(o.(F1,F2),F3) by Def5;
end;
end;
registration
let A;
cluster multcpfunc(A) -> commutative associative;
coherence
proof
thus multcpfunc A is commutative
proof
let f,g be Element of PFuncs(A,COMPLEX);
A1: dom((multcpfunc A).(g,f)) = dom g/\ dom f by Th5;
A2: dom((multcpfunc A).(f,g)) = dom f/\ dom g by Th5;
now
let x be Element of A;
assume
A3: x in dom f /\ dom g;
hence ((multcpfunc A).(f,g)).x = g.x * f.x by A2,Th5
.= ((multcpfunc A).(g,f)).x by A1,A3,Th5;
end;
hence thesis by A2,A1,PARTFUN1:5;
end;
let f,g,h be Element of PFuncs(A,COMPLEX);
set j = (multcpfunc A).(g,h);
set k = (multcpfunc A).(f,g);
set j1 = (multcpfunc A).(f,j);
set k1 = (multcpfunc A).(k,h);
A4: dom k1 = dom k /\ dom h by Th5;
then
A5: dom k1 c= dom k by XBOOLE_1:17;
A6: dom k1 = (dom f /\ dom g)/\dom h by A4,Th5;
A7: dom j1 = dom f /\ dom j by Th5;
then
A8: dom j1 = dom f/\(dom g /\dom h) by Th5;
A9: dom j1 c= dom j by A7,XBOOLE_1:17;
now
let x be Element of A;
assume
A10: x in dom j1;
then
A11: x in dom k1 by A8,A6,XBOOLE_1:16;
thus j1.x =f.x * j.x by A10,Th5
.= f.x * (g.x * h.x) by A9,A10,Th5
.= (f.x * g.x) * h.x
.= k.x * h.x by A5,A11,Th5
.= k1.x by A11,Th5;
end;
hence thesis by A8,A6,PARTFUN1:5,XBOOLE_1:16;
end;
end;
theorem
CPFuncUnit A is_a_unity_wrt multcpfunc A
proof
thus CPFuncUnit A is_a_left_unity_wrt multcpfunc A
proof
let f;
set h = (multcpfunc A).(CPFuncUnit A,f);
dom h = dom(CPFuncUnit A) /\ dom f by Th5;
then dom h = A /\ dom f by FUNCOP_1:13;
then
A1: dom h = dom f by XBOOLE_1:28;
now
let x be Element of A;
assume x in dom f;
then h.x = (CPFuncUnit A).x * f.x by A1,Th5;
then h.x = 1r * f.x by FUNCOP_1:7
.= f.x by COMPLEX1:def 4;
hence h.x = f.x;
end;
hence thesis by A1,PARTFUN1:5;
end;
let f;
set h = (multcpfunc A).(f,CPFuncUnit A);
dom h = dom(CPFuncUnit A) /\ dom f by Th5;
then dom h = A /\ dom f by FUNCOP_1:13;
then
A2: dom h = dom f by XBOOLE_1:28;
now
let x be Element of A;
assume x in dom f;
then h.x = (CPFuncUnit A).x * f.x by A2,Th5;
then h.x = 1r * f.x by FUNCOP_1:7
.= f.x by COMPLEX1:def 4;
hence h.x = f.x;
end;
hence thesis by A2,PARTFUN1:5;
end;
theorem Th9:
CPFuncZero A is_a_unity_wrt addcpfunc A
proof
thus CPFuncZero A is_a_left_unity_wrt addcpfunc A
proof
let f;
set h = (addcpfunc A).(CPFuncZero A,f);
dom h = dom(CPFuncZero A) /\ dom f by Th4;
then dom h = A /\ dom f by FUNCOP_1:13;
then
A1: dom h = dom f by XBOOLE_1:28;
now
let x be Element of A;
A2: (CPFuncZero A).x = 0c by FUNCOP_1:7;
assume x in dom f;
hence h.x=0c+ f.x by A1,A2,Th4
.= f.x;
end;
hence thesis by A1,PARTFUN1:5;
end;
let f;
set h = (addcpfunc A).(f,CPFuncZero A);
dom h = dom(CPFuncZero A) /\ dom f by Th4;
then dom h = A /\ dom f by FUNCOP_1:13;
then
A3: dom h = dom f by XBOOLE_1:28;
now
let x be Element of A;
A4: (CPFuncZero A).x = 0c by FUNCOP_1:7;
assume x in dom f;
hence h.x=0c+ f.x by A3,A4,Th4
.= f.x;
end;
hence thesis by A3,PARTFUN1:5;
end;
reconsider R = -1r as Element of COMPLEX by XCMPLX_0:def 2;
theorem Th10:
(addcpfunc A).(f,(multcomplexcpfunc A).(-1r,f)) = (CPFuncZero A)|(dom f)
proof
reconsider g = (multcomplexcpfunc A).(R,f) as Element of PFuncs(A,COMPLEX);
set h = (addcpfunc A).(f,g);
dom (CPFuncZero A) = A by FUNCOP_1:13;
then dom ((CPFuncZero A)|(dom f)) = A /\ dom f by RELAT_1:61;
then
A1: dom ((CPFuncZero A)|(dom f)) = dom f by XBOOLE_1:28;
A2: dom h = dom g /\ dom f by Th4
.= dom f /\ dom f by Th7;
now
let x be Element of A;
assume
A3: x in dom f;
then
A4: x in dom((-1r)(#)f) by VALUED_1:def 5;
thus h.x = f.x + g.x by A2,A3,Th4
.= f.x + ((-1r)(#)f).x by Def4
.= f.x + (-1r) * f.x by A4,VALUED_1:def 5
.= (CPFuncZero A).x by FUNCOP_1:7,COMPLEX1:def 4
.= ((CPFuncZero A)|(dom f)).x by A3,FUNCT_1:49;
end;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem Th11:
(multcomplexcpfunc A).(1r,f) = f
proof
reconsider g = (multcomplexcpfunc A).(1r,f)
as Element of PFuncs(A,COMPLEX);
A1: now
let x be Element of A;
assume x in dom f;
hence g.x = 1r*(f.x) by Th7
.= f.x by COMPLEX1:def 4;
end;
dom g=dom f by Th7;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th12:
(multcomplexcpfunc A).(a,(multcomplexcpfunc A).(b,f))
= (multcomplexcpfunc A).(a*b,f)
proof
reconsider a,b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider c = a*b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider g = (multcomplexcpfunc A).(b,f) as Element of PFuncs(A,COMPLEX);
reconsider h = (multcomplexcpfunc A).(a,g) as Element of PFuncs(A,COMPLEX);
reconsider k = (multcomplexcpfunc A).(c,f) as Element of PFuncs(A,COMPLEX);
A1: dom h = dom g by Th7;
A2: dom g = dom f by Th7;
A3: now
let x be Element of A;
assume
A4: x in dom h;
hence h.x =a*(g.x) by A1,Th7
.=a*(b*(f.x)) by A2,A1,A4,Th7
.=(a*b)*(f.x)
.= k.x by A2,A1,A4,Th7;
end;
dom k = dom f by Th7;
hence thesis by A2,A1,A3,PARTFUN1:5;
end;
theorem Th13:
(addcpfunc A).((multcomplexcpfunc A).(a,f),(multcomplexcpfunc A).(b,f)) =
(multcomplexcpfunc A).(a+b,f)
proof
reconsider a,b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider c = a+b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider g = (multcomplexcpfunc A).(a,f) as Element of PFuncs(A,COMPLEX);
reconsider h = (multcomplexcpfunc A).(b,f) as Element of PFuncs(A,COMPLEX);
reconsider k = (multcomplexcpfunc A).(c,f) as Element of PFuncs(A,COMPLEX);
set j = (addcpfunc A).(g,h);
dom g = dom f by Th7;
then dom h /\ dom g = dom f /\ dom f by Th7;
then
A1: dom j = dom f by Th4;
A2: now
let x be Element of A;
assume
A3: x in dom j;
then x in dom(b(#)f) by A1,VALUED_1:def 5;
then (b(#)f).x = b*f.x by VALUED_1:def 5;
then
A4: h.x = b*f.x by Def4;
x in dom(a(#)f) by A1,A3,VALUED_1:def 5;
then (a(#)f).x = a*f.x by VALUED_1:def 5;
then g.x = a*f.x by Def4;
then g.x + h.x = (a+b)*(f.x) by A4;
hence j.x = (a+b)*(f.x) by A3,Th4
.= k.x by A1,A3,Th7;
end;
dom k = dom f by Th7;
hence thesis by A1,A2,PARTFUN1:5;
end;
Lm1: (addcpfunc A).((multcomplexcpfunc A).(a,f),(multcomplexcpfunc A).(a,g))
= (multcomplexcpfunc A).(a,(addcpfunc A).(f,g))
proof
reconsider a as Element of COMPLEX by XCMPLX_0:def 2;
reconsider h = (multcomplexcpfunc A).(a,f) as Element of PFuncs(A,COMPLEX);
reconsider i = (multcomplexcpfunc A).(a,g) as Element of PFuncs(A,COMPLEX);
set j = (addcpfunc A).(f,g);
reconsider k = (multcomplexcpfunc A).(a,j) as Element of PFuncs(A,COMPLEX);
set l = (addcpfunc A).(h,i);
A1: dom h = dom f & dom i = dom g by Th7;
A2: dom l = dom h /\ dom i by Th4;
A3: dom j = dom f /\ dom g by Th4;
A4: now
let x be Element of A;
A5: h.x = (a(#)f).x by Def4;
assume
A6: x in dom l;
then
A7: x in dom(f+g) by A1,A2,VALUED_1:def 1;
A8: i.x = (a(#)g).x by Def4;
x in dom i by A2,A6,XBOOLE_0:def 4;
then x in dom g by Th7;
then x in dom (a(#)g) by VALUED_1:def 5;
then
A9: i.x = a * g.x by A8,VALUED_1:def 5;
x in dom h by A2,A6,XBOOLE_0:def 4;
then x in dom f by Th7;
then x in dom (a(#)f) by VALUED_1:def 5;
then
A10: h.x = a * f.x by A5,VALUED_1:def 5;
thus l.x = h.x + i.x by A6,Th4
.= a*(f.x+g.x) by A10,A9
.= a*(f+g).x by A7,VALUED_1:def 1
.= a*j.x by Def5
.= k.x by A1,A3,A2,A6,Th7;
end;
dom k = dom j by Th7;
hence thesis by A1,A3,A2,A4,PARTFUN1:5;
end;
theorem
(multcpfunc A).(f,(addcpfunc A).(g,h)) =
(addcpfunc A).((multcpfunc A).(f,g),(multcpfunc A).(f,h))
proof
set i = (multcpfunc A).(f,h);
set j = (multcpfunc A).(f,g);
set k = (addcpfunc A).(j,i);
set l = (addcpfunc A).(g,h);
set m = (multcpfunc A).(f,l);
A1: dom f /\ dom g /\ dom h = dom f /\ (dom g /\ dom h) by XBOOLE_1:16;
dom i = dom f /\ dom h & dom j = dom f /\ dom g by Th5;
then dom k = (dom h /\ dom f) /\ (dom f /\ dom g) by Th4;
then dom k = dom h /\ (dom f /\ (dom f /\ dom g)) by XBOOLE_1:16;
then
A2: dom k = dom h /\ (dom f /\ dom f /\ dom g) by XBOOLE_1:16;
A3: dom f /\ dom g /\ dom h = dom g /\ (dom f /\ dom h) by XBOOLE_1:16;
A4: now
let x be Element of A;
assume
A5: x in dom k;
then x in dom f /\ dom g by A2,XBOOLE_0:def 4;
then
A6: x in dom(f(#)g) by VALUED_1:def 4;
x in dom g /\ dom h by A2,A1,A5,XBOOLE_0:def 4;
then
A7: x in dom(g+h) by VALUED_1:def 1;
j.x = (f(#)g).x by Def3;
then
A8: j.x = f.x * g.x by A6,VALUED_1:def 4;
x in dom f /\ dom h by A2,A3,A5,XBOOLE_0:def 4;
then
A9: x in dom(f(#)h) by VALUED_1:def 4;
i.x = (f(#)h).x by Def3;
then
A10: i.x = f.x * h.x by A9,VALUED_1:def 4;
k.x = j.x + i.x by A5,Th4;
then l.x = (g+h).x & k.x = f.x * (g.x + h.x) by A8,A10, Def5;
then
A11: k.x = f.x * l.x by A7,VALUED_1:def 1;
x in dom f /\ dom l by A2,A1,A5,Th4;
then
A12: x in dom(f(#)l) by VALUED_1:def 4;
m.x = (f(#)l).x by Def3;
hence k.x = m.x by A12,A11,VALUED_1:def 4;
end;
dom m = dom f /\ dom l & dom l = dom g /\ dom h by Th4,Th5;
hence thesis by A2,A4,PARTFUN1:5,XBOOLE_1:16;
end;
theorem
(multcpfunc A).((multcomplexcpfunc A).(a,f),g)
= (multcomplexcpfunc A).(a,(multcpfunc A).(f,g))
proof
reconsider a as Element of COMPLEX by XCMPLX_0:def 2;
reconsider i = (multcomplexcpfunc A).(a,f) as Element of PFuncs(A,COMPLEX);
set j = (multcpfunc A).(f,g);
set k = (multcpfunc A).(i,g);
reconsider l = (multcomplexcpfunc A).(a,j) as Element of PFuncs(A,COMPLEX);
A1: dom i = dom f & dom k = dom i /\ dom g by Th5,Th7;
A2: dom j = dom f /\ dom g by Th5;
A3: now
let x be Element of A;
A4: j.x = (f(#)g).x by Def3;
assume
A5: x in dom k;
then x in dom(f(#)g) by A1,VALUED_1:def 4;
then
A6: j.x = f.x * g.x by A4,VALUED_1:def 4;
A7: i.x = (a(#)f).x & dom (a(#)f) = dom f by Def4,VALUED_1:def 5;
x in dom f by A1,A5,XBOOLE_0:def 4;
then
A8: i.x = a * f.x by A7,VALUED_1:def 5;
A9: l.x = (a(#)j).x by Def4;
x in dom(a(#)j) by A1,A2,A5,VALUED_1:def 5;
then
A10: l.x = a*(f.x * g.x) by A6,A9,VALUED_1:def 5;
k.x =i.x * g.x by A5,Th5;
hence k.x = l.x by A8,A10;
end;
dom l = dom j by Th7;
hence thesis by A1,A2,A3,PARTFUN1:5;
end;
definition
let A;
func CLSp_PFunctA -> non empty CLSStruct equals
CLSStruct(#PFuncs(A,COMPLEX),
CPFuncZero A, addcpfunc A, multcomplexcpfunc A#);
coherence;
end;
reserve u,v,w for VECTOR of CLSp_PFunctA;
registration
let A;
cluster CLSp_PFunctA -> strict Abelian add-associative right_zeroed
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence
proof
set IT = CLSp_PFunctA;
thus IT is strict;
thus u+v = v+u by BINOP_1:def 2;
thus u+v+w = u+(v+w) by BINOP_1:def 3;
thus u+0.IT = u
proof
reconsider u9=u as Element of PFuncs(A,COMPLEX);
A1: CPFuncZero A is_a_unity_wrt addcpfunc A by Th9;
thus u+0.IT = u by A1,BINOP_1:3;
end;
thus for a,u,v holds a*(u+v) = a*u + a *v
proof
let a;
reconsider a1= a as Element of COMPLEX by XCMPLX_0:def 2;
for u,v be VECTOR of CLSp_PFunctA holds a*(u+v) = a*u + a*v
proof
let u,v be VECTOR of CLSp_PFunctA;
reconsider u9=u as Element of PFuncs(A,COMPLEX);
reconsider v9=v as Element of PFuncs(A,COMPLEX);
a1*(u+v) = (multcomplexcpfunc A).(a1,(addcpfunc A).(u9,v9))
.= (addcpfunc A).
((multcomplexcpfunc A).(a1,u9),(multcomplexcpfunc A).(a1,v9)) by Lm1
.= a1*u + a1*v;
hence thesis;
end;
hence thesis;
end;
thus for a,b being Complex,v holds (a+b)*v = a*v + b*v
proof
let a,b be Complex, v be VECTOR of CLSp_PFunctA;
reconsider a1=a,b1=b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider v9=v as Element of PFuncs(A,COMPLEX);
(a1+b1)*v = (multcomplexcpfunc A).(a1+b1,v9).=
(addcpfunc A).((multcomplexcpfunc A).(a1,v9),
(multcomplexcpfunc A).(b1,v9))
by Th13 .= a1*v + b1*v;
hence thesis;
end;
thus for a,b being Complex,v holds (a*b)*v = a*(b*v)
proof
let a,b be Complex, v be VECTOR of CLSp_PFunctA;
reconsider a1=a,b1=b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider v9=v as Element of PFuncs(A,COMPLEX);
(a1*b1)*v = (multcomplexcpfunc A).(a1*b1,v9) .=
(multcomplexcpfunc A).(a1,(multcomplexcpfunc A).(b1,v9)) by Th12
.= a1*(b1*v);
hence thesis;
end;
let v;
reconsider v9=v as Element of PFuncs(A,COMPLEX);
1r * v = (multcomplexcpfunc A).(1r,v9) .= v by Th11;
hence 1r * v = v;
end;
end;
begin :: Quasi-Complex Linear Space of Integrable Functions
reserve X for non empty set,
x for Element of X,
S for SigmaField of X,
M for sigma_Measure of S,
E,E1,E2,A,B for Element of S,
f,g,h,f1,g1 for PartFunc of X,COMPLEX;
registration
let X; let f be PartFunc of X,COMPLEX;
cluster abs f -> nonnegative;
coherence
proof
now let x be object;
assume x in dom abs f; then
(abs f).x = |.f.x.| by VALUED_1:def 11;
hence 0 <= (abs f).x by COMPLEX1:46;
end;
hence thesis by MESFUNC6:52;
end;
end;
theorem Th16:
for f be PartFunc of X,COMPLEX st dom f in S
& for x st x in dom f holds 0= f.x holds
f is_integrable_on M & Integral(M,f) = 0
proof
let f be PartFunc of X,COMPLEX;
assume dom f in S; then
reconsider E = dom f as Element of S;
assume
A1: for x st x in dom f holds 0 = f.x;
A2: for x st x in dom f holds (Re f).x = 0 & (Im f).x = 0
proof
let x such that
A3: x in dom f;
A4: x in dom (Re f) & x in dom(Im f) by A3,COMSEQ_3:def 3,def 4;
A5: (Re f).x = Re (f.x) by COMSEQ_3:def 3,A4
.= 0 by A3,A1,COMPLEX1:4;
(Im f).x = Im (f.x) by COMSEQ_3:def 4,A4
.= 0 by A3,A1,COMPLEX1:4;
hence thesis by A5;
end;
A6: dom Re f = E by COMSEQ_3:def 3;
A7: dom Im f = E by COMSEQ_3:def 4;
set f1 = Re f;
A8: E=dom f1 & for x st x in dom f1 holds 0 = f1.x by A2,A6;
A9: R_EAL f1 is_integrable_on M & Integral(M,R_EAL f1) = 0 by LPSPACE1:22,A8;
A10: Re f is_integrable_on M & Integral(M,Re f) = 0 by A9;
set f2 = Im f;
A11: E=dom f2 & for x st x in dom f2 holds 0 = f2.x by A2,A7;
A12: R_EAL f2 is_integrable_on M & Integral(M,R_EAL f2) = 0 by LPSPACE1:22,A11;
A13: Im f is_integrable_on M & Integral(M,Im f) = 0 by A12;
f is_integrable_on M by A10,A13,MESFUN6C:def 2; then
ex RF, IF be Real st
RF = Integral(M,Re f) & IF= Integral(M,Im f) &
Integral(M,f) = RF+IF*<i> by MESFUN6C:def 3;
hence thesis by A10,A13,MESFUN6C:def 2;
end;
Lm2: (X = dom f & for x st x in dom f holds 0 = f.x) implies f
is_integrable_on M & Integral(M,f) =0
proof
A1: X is Element of S by MEASURE1:7;
assume X=dom f & for x st x in dom f holds 0 = f.x;
hence thesis by A1,Th16;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func L1_CFunctions M -> non empty Subset of CLSp_PFunctX equals
{ f where f
is PartFunc of X,COMPLEX : ex ND be Element of S st M.ND=0 & dom f = ND` & f
is_integrable_on M };
correctness
proof
reconsider ND = {} as Element of S by MEASURE1:7;
set g = X --> 0c;
set I = { f where f is PartFunc of X,COMPLEX :
ex ND be Element of S st M.ND= 0 & dom f = ND` & f is_integrable_on M };
A1: I c= PFuncs(X,COMPLEX)
proof
let x be object;
assume x in I; then
ex f be PartFunc of X,COMPLEX st x = f & ex ND be Element of S st M.ND=
0 & dom f = ND` & f is_integrable_on M;
hence thesis by PARTFUN1:45;
end;
A2: dom g = ND` by FUNCOP_1:13;
for x be Element of X st x in dom g holds g.x = 0 by FUNCOP_1:7;
then M.ND =0 & g is_integrable_on M by A2,Lm2,VALUED_0:def 19;
then g in I by A2;
hence thesis by A1;
end;
end;
Lm3: X --> 0 in L1_CFunctions M
proof
set g = X --> 0c;
reconsider ND = {} as Element of S by MEASURE1:7;
A1: dom g = ND` by FUNCT_2:def 1;
for x be Element of X st x in dom g holds g.x = 0 by FUNCOP_1:7;
then M.ND =0 & g is_integrable_on M by A1,Lm2,VALUED_0:def 19;
hence thesis by A1;
end;
Lm4: M.E1=0 & M.E2=0 implies M.(E1\/E2) =0
proof
assume M.E1=0 & M.E2=0; then
E1 is measure_zero of M & E2 is measure_zero of M by MEASURE1:def 7;
hence thesis by MEASURE1:37,MEASURE1:def 7;
end;
theorem Th17:
f in L1_CFunctions M & g in L1_CFunctions M implies f + g in L1_CFunctions M
proof
set W = L1_CFunctions M;
assume that
A1: f in W and
A2: g in W;
ex f1 be PartFunc of X,COMPLEX st f1=f &ex ND be Element of S st M.ND=0 &
dom f1 = ND` & f1 is_integrable_on M by A1;
then consider NDv be Element of S such that
A3: M.NDv=0 and
A4: dom f = NDv` and
A5: f is_integrable_on M;
ex g1 be PartFunc of X,COMPLEX st g1=g &ex ND be Element of S st M.ND=0 &
dom g1 = ND` & g1 is_integrable_on M by A2;
then consider NDu be Element of S such that
A6: M.NDu=0 and
A7: dom g = NDu` and
A8: g is_integrable_on M;
A9: dom (f+g)= NDv` /\ NDu` by A4,A7,VALUED_1:def 1
.= (NDv \/ NDu)` by XBOOLE_1:53;
M.(NDv \/ NDu) =0 & f+g is_integrable_on M by A3,A5,A6,A8,Lm4,
MESFUN6C:33;
hence thesis by A9;
end;
theorem Th18:
f in L1_CFunctions M implies a(#)f in L1_CFunctions M
proof
set W = L1_CFunctions M;
assume f in W; then
ex f1 be PartFunc of X,COMPLEX st f1=f & ex ND be Element of S st M.ND=0 &
dom f1 = ND` & f1 is_integrable_on M;
then consider ND be Element of S such that
A1: M.ND=0 and
A2: dom f = ND` & f is_integrable_on M;
dom (a(#)f) = ND` & a(#)f is_integrable_on M by A2,MESFUN6C:40,
VALUED_1:def 5;
hence thesis by A1;
end;
Lm5: L1_CFunctions M is add-closed & L1_CFunctions M is multi-closed
proof
set W = L1_CFunctions M;
now
let v,u be Element of CLSp_PFunctX such that
A1: v in W and
A2: u in W;
reconsider h = v+u as Element of PFuncs(X,COMPLEX);
consider v1 be PartFunc of X, COMPLEX such that
A3: v1=v and
ex ND be Element of S st M.ND=0 & dom v1 = ND` & v1 is_integrable_on M
by A1;
consider u1 be PartFunc of X, COMPLEX such that
A4: u1=u and
ex ND be Element of S st M.ND=0 & dom u1 = ND` & u1 is_integrable_on M
by A2;
dom h = dom v1 /\ dom u1 & for x be object st x in dom h holds h.x = v1.x
+ u1. x by A3,A4,Th4;
then v+u=v1+u1 by VALUED_1:def 1;
hence v+u in L1_CFunctions M by A1,A2,A3,A4,Th17;
end;
hence L1_CFunctions M is add-closed;
now let a be Complex, u be VECTOR of CLSp_PFunctX such that
A5: u in W;
reconsider a1= a as Element of COMPLEX by XCMPLX_0:def 2;
consider u1 be PartFunc of X, COMPLEX such that
A6: u1=u and
ex ND be Element of S st M.ND=0 & dom u1 = ND` & u1 is_integrable_on M
by A5;
reconsider h = a1*u as Element of PFuncs(X,COMPLEX);
A7:a1*u = (multcomplexcpfunc X).(a,u); then
A8: dom h = dom u1 by A6,Th7;
then for x be object st x in dom h holds h.x = a*(u1.x) by A6,A7,Th7;
then a1*u=a(#)u1 by A8,VALUED_1:def 5;
hence a*u in L1_CFunctions M by A5,A6,Th18;
end;
hence thesis;
end;
registration
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
cluster L1_CFunctions M -> multi-closed add-closed;
coherence by Lm5;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func CLSp_L1Funct M -> non empty CLSStruct equals
CLSStruct (# L1_CFunctions M, In (0.(CLSp_PFunctX), L1_CFunctions M),
add|(L1_CFunctions M,CLSp_PFunctX), Mult_(L1_CFunctions M) #);
coherence;
end;
registration
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
cluster CLSp_L1Funct M -> strict Abelian add-associative right_zeroed
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence
proof
0.(CLSp_PFunctX) in L1_CFunctions M by Lm3;
hence thesis by Th3;
end;
end;
begin :: Quotient Space of Quasi-Complex Linear Space of Integrable Functions
reserve v,u for VECTOR of CLSp_L1Funct M;
theorem Th19:
f=v & g=u implies f+g=v+u
proof
reconsider v2=v,u2=u as VECTOR of CLSp_PFunct(X) by TARSKI:def 3;
reconsider h = v2+u2 as Element of PFuncs(X,COMPLEX);
reconsider v3= v2,u3=u2 as Element of PFuncs(X,COMPLEX);
A1: dom h= dom v3 /\ dom u3 by Th4;
assume
A2: f=v & g=u;
then for x be object st x in dom h holds h.x = f.x + g.x by Th4;
then h= f+g by A2,A1,VALUED_1:def 1;
hence thesis by ZFMISC_1:87,FUNCT_1:49;
end;
theorem Th20:
f=u implies a(#)f=a*u
proof
reconsider u2=u as VECTOR of CLSp_PFunctX by TARSKI:def 3;
reconsider h = a*u2 as Element of PFuncs(X,COMPLEX);
assume
A1: f=u;
A2: a*u2 = (multcomplexcpfunc X).(a,u2);
A3: dom h = dom f by A1,A2,Th7;
A4:for x be object st x in dom h holds h.x = a*(f.x) by A1,A2,A3,Th7;
A5: h= a(#)f by A3,A4,VALUED_1:def 5;
reconsider a as Element of COMPLEX by XCMPLX_0:def 2;
[a,u] in [:COMPLEX,(L1_CFunctions M):];
hence thesis by A5,FUNCT_1:49;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g
be PartFunc of X,COMPLEX;
pred f a.e.cpfunc= g,M means
:Def11:
ex E be Element of S st M.E = 0 & f|E` = g|E`;
end;
theorem Th21:
f=u implies u+(-1r)*u = (X --> 0c)|dom f &
ex v,g be 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
reconsider u2=u as VECTOR of CLSp_PFunctX by TARSKI:def 3;
reconsider h = u2+(-1r)*u2 as Element of PFuncs(X,COMPLEX);
set g = X-->0c;
u+(-1r)*u in L1_CFunctions M;
then consider v be PartFunc of X,COMPLEX such that
A1: v=u+(-1r)*u and
ex ND be Element of S st M.ND=0 & dom v = ND` & v is_integrable_on M;
assume
A2: f=u;
reconsider u9=u2 as Element of PFuncs(X,COMPLEX);
A3: h = (addcpfunc X).(u2,(multcomplexcpfunc X).(-1r,u2))
.= (CPFuncZero X)|(dom f) by A2,Th10;
u in L1_CFunctions M; then
ex uu1 be PartFunc of X,COMPLEX st uu1=u & ex ND be Element of S st M.ND=0
& dom uu1 = ND` & uu1 is_integrable_on M;
then consider ND be Element of S such that
A4: M.ND=0 and
A5: dom f = ND` and
f is_integrable_on M by A2;
[R,u] in [:COMPLEX,L1_CFunctions M:]; then
A6: (-1r)*u2=(-1r)*u by FUNCT_1:49;
hence u+(-1r)*u = (X --> 0)|dom f by A3,ZFMISC_1:87,FUNCT_1:49;
v|ND` = g|ND`|ND` by A3,A6,A1,A5,ZFMISC_1:87,FUNCT_1:49;
then
A7: v|ND` = g|ND` by FUNCT_1:51;
g in L1_CFunctions M by Lm3;
hence thesis by A1,A4,A7,Def11;
end;
theorem Th22:
f a.e.cpfunc= f,M
proof
{} is Element of S by MEASURE1:7;
then consider E being Element of S such that
A1: E = {};
A2: f|E` = f|E`;
M.E = 0 by A1,VALUED_0:def 19;
hence thesis by A2;
end;
theorem
f a.e.cpfunc= g,M implies g a.e.cpfunc= f,M;
theorem Th24:
f a.e.cpfunc= g,M & g a.e.cpfunc= h,M implies f a.e.cpfunc= h,M
proof
assume that
A1: f a.e.cpfunc= g,M and
A2: g a.e.cpfunc= h,M;
consider EQ1 being Element of S such that
A3: M.EQ1=0 and
A4: f|EQ1` = g|EQ1` by A1;
consider EQ2 being Element of S such that
A5: M.EQ2=0 and
A6: g|EQ2` = h|EQ2` by A2;
A7: M.(EQ1 \/ EQ2) = 0 by A3,A5,Lm4;
A8: (EQ1\/EQ2)` c= EQ2` by XBOOLE_1:7,34;
A9: (EQ1\/EQ2)` c= EQ1` by XBOOLE_1:7,34;
then f|(EQ1\/EQ2)` =g|EQ1`|(EQ1\/EQ2)` by A4,FUNCT_1:51
.=g|(EQ1\/EQ2)` by A9,FUNCT_1:51
.=h|EQ2`|(EQ1\/EQ2)` by A6,A8,FUNCT_1:51
.=h|(EQ1\/EQ2)` by A8,FUNCT_1:51;
hence thesis by A7;
end;
theorem Th25:
f a.e.cpfunc= f1,M & g a.e.cpfunc= g1,M implies (f+g) a.e.cpfunc= (f1+g1),M
proof
assume that
A1: f a.e.cpfunc= f1,M and
A2: g a.e.cpfunc= g1,M;
consider EQ1 being Element of S such that
A3: M.(EQ1)=0 and
A4: f|EQ1` =f1|EQ1` by A1;
consider EQ2 being Element of S such that
A5: M.(EQ2)=0 and
A6: g|EQ2` =g1|EQ2` by A2;
A7: (EQ1\/EQ2)` c= EQ1` by XBOOLE_1:7,34; then
f|(EQ1\/EQ2)` = f1|EQ1`|(EQ1\/EQ2)` by A4,FUNCT_1:51; then
A8: f|(EQ1\/EQ2)` = f1|(EQ1\/EQ2)` by A7,FUNCT_1:51;
A9: (EQ1\/EQ2)` c= EQ2` by XBOOLE_1:7,34; then
g|(EQ1\/EQ2)` = g1|EQ2`|(EQ1\/EQ2)` by A6,FUNCT_1:51
.=g1|(EQ1\/EQ2)` by A9,FUNCT_1:51; then
A10:(f+g)|(EQ1\/EQ2)` = f1|(EQ1\/EQ2)` + g1|(EQ1\/EQ2)` by A8,RFUNCT_1:44
.= (f1+g1)|(EQ1\/EQ2)` by RFUNCT_1:44;
M.(EQ1 \/ EQ2) = 0 by A3,A5,Lm4;
hence thesis by A10;
end;
theorem Th26:
f a.e.cpfunc= g,M implies a(#)f a.e.cpfunc= a(#)g,M
proof
assume f a.e.cpfunc= g,M;
then consider E being Element of S such that
A1: M.E = 0 and
A2: f|E`=g|E`;
(a(#)f)|E` = a(#)(g|E`) by A2,RFUNCT_1:49
.= (a(#)g)|E` by RFUNCT_1:49;
hence thesis by A1;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func AlmostZeroCFunctions M -> non empty Subset of CLSp_L1Funct M equals
{ f where f is PartFunc of X,COMPLEX :
f in L1_CFunctions M & f a.e.cpfunc= X-->0c,M };
coherence
proof
A1: now
let x be object;
assume
x in { f where f is PartFunc of X,COMPLEX: f in L1_CFunctions M & f
a.e.cpfunc= X-->0c,M }; then
ex f be PartFunc of X,COMPLEX st x=f & f in L1_CFunctions M &
f a.e.cpfunc= X-->0c,M;
hence x in the carrier of CLSp_L1Funct M;
end;
X-->0c a.e.cpfunc= X-->0c,M & X-->0 in L1_CFunctions M by Lm3,Th22;
then X-->0 in { f where f is PartFunc of X,COMPLEX : f in L1_CFunctions M
& f a.e.cpfunc= X-->0c,M };
hence thesis by A1,TARSKI:def 3;
end;
end;
theorem Th27:
(X-->0c) + (X-->0c) = X-->0c & a(#)(X-->0c) = X-->0c
proof
set g1 = X-->0c;
set g2 = X-->0c;
A1: now
let x be Element of X;
assume x in dom(a(#)g1);
then (a(#)g1).x = a * g1.x by VALUED_1:def 5;
then (a(#)g1).x = a * 0 by FUNCOP_1:7;
hence (a(#)g1).x = (X --> 0c).x by FUNCOP_1:7;
end;
A2: dom(g1+g2) = dom g1 /\ dom g2 by VALUED_1:def 1;
now
let x be Element of X;
assume x in dom(X --> 0c);
then (g1+g2).x = g1.x + g2.x by A2,VALUED_1:def 1;
then (g1+g2).x = 0 + g2.x by FUNCOP_1:7;
hence (g1+g2).x = (X --> 0c).x;
end;
hence g1+g2 = X-->0c by A2,PARTFUN1:5;
dom(a(#)g1) = dom(X-->0c) by VALUED_1:def 5;
hence thesis by A1,PARTFUN1:5;
end;
Lm6: AlmostZeroCFunctions M is add-closed & AlmostZeroCFunctions M is
multi-closed
proof
set Z = AlmostZeroCFunctions M;
set V = CLSp_L1Funct M;
now
let v,u be VECTOR of V such that
A1: v in Z and
A2: u in Z;
consider v1 be PartFunc of X, COMPLEX such that
A3: v1=v and
v1 in L1_CFunctions M and
A4: v1 a.e.cpfunc= X-->0c,M by A1;
consider u1 be PartFunc of X, COMPLEX such that
A5: u1=u and
u1 in L1_CFunctions M and
A6: u1 a.e.cpfunc= X-->0c,M by A2;
A7: v+u=v1+u1 by A3,A5,Th19;
(X-->0c)+(X-->0c)=X-->0c by Th27;
then v1+u1 a.e.cpfunc=X-->0c,M by A4,A6,Th25;
hence v+u in Z by A7;
end;
hence Z is add-closed;
now
let a be Complex, u be VECTOR of V;
reconsider a1= a as Element of COMPLEX by XCMPLX_0:def 2;
assume u in Z;
then consider u1 be PartFunc of X, COMPLEX such that
A8: u1=u and
u1 in L1_CFunctions M and
A9: u1 a.e.cpfunc= X-->0c,M;
A10: a1*u=a(#)u1 by A8,Th20;
a1(#)(X-->0)=X-->0 by Th27;
then a1(#)u1 a.e.cpfunc=X-->0c,M by A9,Th26;
hence a*u in Z by A10;
end;
hence thesis;
end;
registration
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
cluster AlmostZeroCFunctions M -> add-closed multi-closed;
coherence by Lm6;
end;
theorem
0.(CLSp_L1Funct M) = X-->0c & 0.(CLSp_L1Funct M) in
AlmostZeroCFunctions M
proof
thus 0.(CLSp_L1Funct M) = X --> 0c by Lm3,SUBSET_1:def 8;
X-->0c a.e.cpfunc= X-->0c,M & 0.(CLSp_L1Funct M) = 0.(CLSp_PFunctX)
by Lm3,Th22,SUBSET_1:def 8;
hence thesis;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func CLSp_AlmostZeroFunct M -> non empty CLSStruct equals
CLSStruct (#
AlmostZeroCFunctions M, In(0.(CLSp_L1Funct M),AlmostZeroCFunctions M),
add|(AlmostZeroCFunctions M,CLSp_L1Funct M),
Mult_(AlmostZeroCFunctions M) #);
coherence;
end;
registration
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
cluster CLSp_L1Funct M -> strict Abelian add-associative right_zeroed
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence;
end;
reserve v,u for VECTOR of CLSp_AlmostZeroFunct M;
theorem
f=v & g=u implies f+g=v+u
proof
assume
A1: f=v & g=u;
reconsider v2=v, u2=u as VECTOR of CLSp_L1Funct M by TARSKI:def 3;
thus v+u=v2+u2 by ZFMISC_1:87,FUNCT_1:49
.=f+g by A1,Th19;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be
PartFunc of X,COMPLEX;
func a.e-Ceq-class(f,M) -> Subset of L1_CFunctions M equals
{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
proof
now
let x be object;
assume
x in {g where g is PartFunc of X,COMPLEX : g in L1_CFunctions M & f
in L1_CFunctions M & f a.e.cpfunc= g,M };
then ex g be PartFunc of X,COMPLEX st x=g & g in L1_CFunctions M & f in
L1_CFunctions M & f a.e.cpfunc= g,M;
hence x in L1_CFunctions M;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem Th30:
f in L1_CFunctions M & g in L1_CFunctions M implies (g a.e.cpfunc= f,M
iff g in a.e-Ceq-class(f,M))
proof
assume
A1: f in L1_CFunctions M & g in L1_CFunctions M;
hereby
assume g a.e.cpfunc= f,M;
then f a.e.cpfunc= g,M;
hence g in a.e-Ceq-class(f,M) by A1;
end;
assume g in a.e-Ceq-class(f,M);
then ex r be PartFunc of X,COMPLEX st g=r & r in L1_CFunctions M & f in
L1_CFunctions M & f a.e.cpfunc= r,M;
hence g a.e.cpfunc= f,M;
end;
theorem Th31:
f in L1_CFunctions M implies f in a.e-Ceq-class(f,M)
proof
assume
A1: f in L1_CFunctions M;
f a.e.cpfunc= f,M by Th22;
hence f in a.e-Ceq-class(f,M) by A1;
end;
theorem Th32:
f in L1_CFunctions M & g in L1_CFunctions M implies (a.e-Ceq-class(
f,M) = a.e-Ceq-class(g,M) iff f a.e.cpfunc= g,M)
proof
assume that
A1: f in L1_CFunctions M and
A2: g in L1_CFunctions M;
hereby
assume a.e-Ceq-class(f,M) = a.e-Ceq-class(g,M);
then f in {r where r is PartFunc of X,COMPLEX : r in L1_CFunctions M &
g in L1_CFunctions M & g a.e.cpfunc= r,M } by A1,Th31;
then ex r be PartFunc of X,COMPLEX st f=r & r in L1_CFunctions M
& g in L1_CFunctions M & g a.e.cpfunc= r,M;
hence f a.e.cpfunc= g,M;
end;
assume
A3: f a.e.cpfunc= g,M;
now
let x be object;
assume x in a.e-Ceq-class(f,M);
then consider r be PartFunc of X,COMPLEX such that
A4: x=r & r in L1_CFunctions M and
f in L1_CFunctions M and
A5: f a.e.cpfunc= r,M;
g a.e.cpfunc= f,M by A3;
then g a.e.cpfunc= r,M by A5,Th24;
hence x in a.e-Ceq-class(g,M) by A2,A4;
end;
then
A6: a.e-Ceq-class(f,M) c= a.e-Ceq-class(g,M);
now
let x be object;
assume x in a.e-Ceq-class(g,M);
then consider r be PartFunc of X,COMPLEX such that
A7: x=r & r in L1_CFunctions M and
g in L1_CFunctions M and
A8: g a.e.cpfunc= r,M;
f a.e.cpfunc= r,M by A3,A8,Th24;
hence x in a.e-Ceq-class(f,M) by A1,A7;
end;
then a.e-Ceq-class(g,M) c= a.e-Ceq-class(f,M);
hence thesis by A6,XBOOLE_0:def 10;
end;
theorem
f in L1_CFunctions M & g in L1_CFunctions M implies (a.e-Ceq-class(f,M) =
a.e-Ceq-class(g,M) iff g in a.e-Ceq-class(f,M))
proof
assume
A1: f in L1_CFunctions M & g in L1_CFunctions M;
then g a.e.cpfunc= f,M iff g in a.e-Ceq-class(f,M) by Th30;
hence thesis by A1,Th32;
end;
theorem Th34:
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) implies a.e-Ceq-class(f+g,M) = a.e-Ceq-class(f1+g1,M)
proof
assume that
A1: f in L1_CFunctions M & f1 in L1_CFunctions M & g in L1_CFunctions M &
g1 in L1_CFunctions M and
A2: a.e-Ceq-class(f,M) = a.e-Ceq-class(f1,M) & a.e-Ceq-class(g,M) =
a.e-Ceq-class(g1,M);
f a.e.cpfunc= f1,M & g a.e.cpfunc= g1,M by A1,A2,Th32;
then
A3: f + g a.e.cpfunc= f1+g1,M by Th25;
f + g in L1_CFunctions M & f1+g1 in L1_CFunctions M by A1,Th17;
hence thesis by A3,Th32;
end;
theorem Th35:
f in L1_CFunctions M & g in L1_CFunctions M & a.e-Ceq-class(f,M) =
a.e-Ceq-class(g,M) implies a.e-Ceq-class(a(#)f,M) = a.e-Ceq-class(a(#)g,M)
proof
assume that
A1: f in L1_CFunctions M & g in L1_CFunctions M and
A2: a.e-Ceq-class(f,M) = a.e-Ceq-class(g,M);
f a.e.cpfunc= g,M by A1,A2,Th32;
then
A3: a(#)f a.e.cpfunc= a(#)g,M by Th26;
a(#)f in L1_CFunctions M & a(#)g in L1_CFunctions M by A1,Th18;
hence thesis by A3,Th32;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func CCosetSet M -> non empty Subset-Family of L1_CFunctions M equals
{
a.e-Ceq-class(f,M) where f is PartFunc of X,COMPLEX : f in L1_CFunctions M};
correctness
proof
set C = {a.e-Ceq-class(f,M) where f is PartFunc of X,COMPLEX : f in
L1_CFunctions M};
A1: C c= bool L1_CFunctions M
proof
let x be object;
assume x in C;
then ex f be PartFunc of X,COMPLEX st a.e-Ceq-class(f,M) = x & f in
L1_CFunctions M;
hence thesis;
end;
X-->0 in L1_CFunctions M by Lm3;
then a.e-Ceq-class(X-->0c,M) in C;
hence thesis by A1;
end;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func addCCoset M -> BinOp of CCosetSet M means
:Def16:
for A,B be Element of
CCosetSet M, a,b be PartFunc of X,COMPLEX st a in A & b in B holds it.(A,B) =
a.e-Ceq-class(a+b,M);
existence
proof
defpred P[set,set,set] means for a,b be PartFunc of X,COMPLEX st a in $1
& b in $2 holds $3 = a.e-Ceq-class(a+b,M);
set C = CCosetSet M;
A1: now
let A,B be Element of C;
A in C;
then consider a be PartFunc of X,COMPLEX such that
A2: A=a.e-Ceq-class(a,M) and
A3: a in L1_CFunctions M;
B in C;
then consider b be PartFunc of X,COMPLEX such that
A4: B=a.e-Ceq-class(b,M) and
A5: b in L1_CFunctions M;
set z = a.e-Ceq-class(a+b,M);
A6: a+b in L1_CFunctions M by A3,A5,Th17;
then z in C;
then reconsider z as Element of C;
take z;
now
let a1,b1 be PartFunc of X,COMPLEX;
assume
A7: a1 in A & b1 in B;
then a1 a.e.cpfunc= a,M & b1 a.e.cpfunc= b,M by A2,A3,A4,A5,Th30;
then
A8: a1+b1 a.e.cpfunc= a+b,M by Th25;
a1+b1 in L1_CFunctions M by A7,Th17;
hence z = a.e-Ceq-class(a1+b1,M) by A6,A8,Th32;
end;
hence P[A,B,z];
end;
consider f be Function of [:C,C:],C such that
A9: for A,B be Element of C holds P[A,B, f.(A,B)] from BINOP_1:sch 3(A1);
reconsider f as BinOp of C;
take f;
let A,B be Element of C;
let a,b be PartFunc of X,COMPLEX;
assume a in A & b in B;
hence thesis by A9;
end;
uniqueness
proof
set C = CCosetSet M;
let f1,f2 be BinOp of CCosetSet M such that
A10: for A,B be Element of CCosetSet M, a,b be PartFunc of X,COMPLEX st a
in A & b in B holds f1.(A,B) = a.e-Ceq-class(a+b,M) and
A11: for A,B be Element of CCosetSet M, a,b be PartFunc of X,COMPLEX st a
in A & b in B holds f2.(A,B) = a.e-Ceq-class(a+b,M);
now
let A,B be Element of CCosetSet M;
A in C;
then consider a1 be PartFunc of X,COMPLEX such that
A12: A=a.e-Ceq-class(a1,M) & a1 in L1_CFunctions M;
B in C;
then consider b1 be PartFunc of X,COMPLEX such that
A13: B=a.e-Ceq-class(b1,M) & b1 in L1_CFunctions M;
A14: b1 in B by A13,Th31;
A15: a1 in A by A12,Th31;
then f1.(A,B) = a.e-Ceq-class(a1+b1,M) by A10,A14;
hence f1.(A,B) = f2.(A,B) by A11,A15,A14;
end;
hence thesis;
end;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func zeroCCoset M -> Element of CCosetSet M equals
a.e-Ceq-class(X --> 0c,M);
correctness
proof
X-->0c in L1_CFunctions M by Lm3;
then a.e-Ceq-class(X-->0c,M) in CCosetSet M;
hence thesis;
end;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func lmultCCoset M -> Function of [:COMPLEX, CCosetSet M:],CCosetSet M means
:Def18:
for z be Complex, A be Element of CCosetSet M, f be PartFunc of X,COMPLEX st
f in A holds it.(z,A) = a.e-Ceq-class(z(#)f,M);
existence
proof
defpred P[Element of COMPLEX,set,set] means for f be PartFunc of X,COMPLEX
st f in $2 holds $3 = a.e-Ceq-class($1(#)f,M);
set C = CCosetSet M;
A1: now
let z be Element of COMPLEX, A be Element of C;
A in C;
then consider a be PartFunc of X,COMPLEX such that
A2: A = a.e-Ceq-class(a,M) and
A3: a in L1_CFunctions M;
set c = a.e-Ceq-class(z(#)a,M);
A4: z(#)a in L1_CFunctions M by A3,Th18;
then c in C;
then reconsider c as Element of C;
take c;
now
let a1 be PartFunc of X,COMPLEX;
assume
A5: a1 in A;
then a1 a.e.cpfunc= a,M by A2,A3,Th30;
then
A6: z(#)a1 a.e.cpfunc= z(#)a,M by Th26;
z(#)a1 in L1_CFunctions M by A5,Th18;
hence c = a.e-Ceq-class(z(#)a1,M) by A4,A6,Th32;
end;
hence P[z,A,c];
end;
consider f be Function of [:COMPLEX,C:],C such that
A7: for z be Element of COMPLEX, A be Element of C holds P[z,A, f.(z,A)]
from BINOP_1:sch 3(A1);
take f;
let z be Complex, A be Element of C, a be PartFunc of X,COMPLEX;
z in COMPLEX by XCMPLX_0:def 2;
hence thesis by A7;
end;
uniqueness
proof
set C = CCosetSet M;
let f1,f2 be Function of [:COMPLEX,C:],C such that
A8: for z be Complex, A be Element of CCosetSet M, a be
PartFunc of X,COMPLEX st a in A holds f1.(z,A) = a.e-Ceq-class(z(#)a,M) and
A9: for z be Complex, A be Element of CCosetSet M, a be
PartFunc of X,COMPLEX st a in A holds f2.(z,A) = a.e-Ceq-class(z(#)a,M);
now
let z be Element of COMPLEX, A be Element of CCosetSet M;
A in C;
then consider a1 be PartFunc of X,COMPLEX such that
A10: A=a.e-Ceq-class(a1,M) & a1 in L1_CFunctions M;
thus f1.(z,A) = a.e-Ceq-class(z(#)a1,M) by A8,A10,Th31
.= f2.(z,A) by A9,A10,Th31;
end;
hence thesis;
end;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func Pre-L-CSpace M -> strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty CLSStruct means
:Def19:
the carrier of it = CCosetSet M & the addF of it = addCCoset M
& 0.it = zeroCCoset M & the Mult of it = lmultCCoset M;
existence
proof
set C = CCosetSet M, aC = addCCoset M, zC = zeroCCoset M,
lC = lmultCCoset M, A = CLSStruct (# C,zC,aC,lC #);
A1: A is Abelian
proof
let A1,A2 be Element of A;
A1 in C;
then consider a be PartFunc of X,COMPLEX such that
A2: A1 = a.e-Ceq-class(a,M) & a in L1_CFunctions M;
A2 in C;
then consider b be PartFunc of X,COMPLEX such that
A3: A2 = a.e-Ceq-class(b,M) & b in L1_CFunctions M;
A4: b in A2 by A3,Th31;
A5: a in A1 by A2,Th31;
then A1+A2 = a.e-Ceq-class(a+b,M) by A4,Def16;
hence thesis by A5,A4,Def16;
end;
A6: A is right_zeroed
proof
set z = X --> 0c;
A7: z in L1_CFunctions M by Lm3;
A8: z in 0.A by A7,Th31;
let A1 be Element of A;
A1 in C;
then consider a be PartFunc of X,COMPLEX such that
A9: A1=a.e-Ceq-class(a,M) and
A10: a in L1_CFunctions M;
reconsider a1=a as VECTOR of CLSp_L1Funct M by A10;
reconsider a1=a,z1=z as VECTOR of CLSp_L1Funct M by A10,A7;
A11: a+z =a1+z1 by Th19
.=a1+0.CLSp_L1Funct M
.=a by RLVECT_1:def 4;
a in A1 by A9,A10,Th31;
hence thesis by A9,A8,A11,Def16;
end;
A12: now
let x,y be Complex, A1,A2 be Element of A;
reconsider x1=x, y1=y as Element of COMPLEX by XCMPLX_0:def 2;
A1 in C;
then consider a be PartFunc of X,COMPLEX such that
A13: A1=a.e-Ceq-class(a,M) and
A14: a in L1_CFunctions M;
A15: a in A1 by A13,A14,Th31;
lC.(x1,A1) =a.e-Ceq-class(x(#)a,M) by A13,A14,Th31,Def18;
then
A16: x(#)a in x*A1 by A14,Th18,Th31;
A2 in C;
then consider b be PartFunc of X,COMPLEX such that
A17: A2=a.e-Ceq-class(b,M) and
A18: b in L1_CFunctions M;
reconsider a1=a,b1=b as VECTOR of CLSp_L1Funct M by A14,A18;
A19: x(#)a = x1*a1 by Th20;
A20: b in A2 by A17,A18,Th31;
lC.(x1,A2) =a.e-Ceq-class(x(#)b,M) by A17,A18,Th31,Def18;
then
A21: x(#)b in x1*A2 by A18,Th18,Th31;
a+b = a1+b1 by Th19;
then x(#)(a+b) = x1*(a1+b1) by Th20;
then
A22: x(#)(a+b) = x*a1+x*b1 by CLVECT_1:def 2;
A23: x(#)b = x1*b1 by Th20;
aC.(A1,A2) =a.e-Ceq-class(a+b,M) by A15,A20,Def16;
then
A24: a+b in (A1+A2) by A14,A18,Th17,Th31;
x1*(A1+A2) = lC.(x1,A1+A2) .=
a.e-Ceq-class(x(#)(a+b),M) by A24,Def18
.= a.e-Ceq-class(x(#)a+x(#)b,M) by A19,A22,A23,Th19;
hence x*(A1+A2) = x*A1+x*A2 by A16,A21,Def16;
A25: y(#)a = y1*a1 by Th20;
lC.(y1,A1) =a.e-Ceq-class(y(#)a,M) by A13,A14,Th31,Def18;
then
A26: y(#)a in y1*A1 by A14,Th18,Th31;
A27: (x+y)(#)a = (x1+y1)*a1 by Th20
.= x*a1+y*a1 by CLVECT_1:def 3
.= x(#)a + y(#)a by A25,A19,Th19;
(x1+y1)*A1 = lC.(x1+y1,A1)
.= a.e-Ceq-class(x(#)a+y(#)a,M) by A27,A13,A14,Th31,Def18;
hence (x+y)*A1 = x*A1+y*A1 by A16,A26,Def16;
A28: x1(#)(y1(#)a) =x1*(y1*a1) by A25,Th20
.= (x1*y1)*a1 by CLVECT_1:def 4
.= (x1*y1)(#)a by Th20;
(x1*y1)*A1 = lC.(x1*y1,A1)
.=a.e-Ceq-class(x1(#)(y1(#)a),M) by A28,A13,A14,Th31,Def18
.= lC.(x1,y1*A1) by A26,Def18
.=x*(y*A1);
hence (x*y)*A1=x*(y*A1);
A29: 1r(#)a =1r*a1 by Th20
.= a by CLVECT_1:def 5;
thus 1r*A1 = lC.(1r,A1)
.= A1 by A13,A29,A14,Th31,Def18;
end;
A30: A is right_complementable
proof
let A1 be Element of A;
A1 in C;
then consider a be PartFunc of X,COMPLEX such that
A31: A1=a.e-Ceq-class(a,M) and
A32: a in L1_CFunctions M;
set A2 = a.e-Ceq-class((-1r)(#)a,M);
A33: (-1r)(#)a in L1_CFunctions M by A32,Th18;
then A2 in C;
then reconsider A2 as Element of A;
A34: a in A1 & (-1r)(#)a in A2 by A31,A32,Th18,Th31;
reconsider a1=a as VECTOR of CLSp_L1Funct M by A32;
take A2;
consider v,g be PartFunc of X,COMPLEX such that
v in L1_CFunctions M and
g in L1_CFunctions M and
A35: v = a1+(-1r)*a1 and
A36: g = X --> 0c and
A37: v a.e.cpfunc= g,M by Th21;
A38: X --> 0c in L1_CFunctions M by Lm3;
A39: a+(-1r)(#)a in L1_CFunctions M by A32,A33,Th17;
(-1r)(#)a = (-1r)*a1 by Th20;
then a+(-1r)(#)a a.e.cpfunc= g,M by A35,A37,Th19;
then 0.A = a.e-Ceq-class(a+ (-1r)(#)a,M) by A36,A39,A38,Th32;
hence thesis by A34,Def16;
end;
A is add-associative
proof
let A1,A2,A3 be Element of A;
A1 in C;
then consider a be PartFunc of X,COMPLEX such that
A40: A1=a.e-Ceq-class(a,M) and
A41: a in L1_CFunctions M;
A2 in C;
then consider b be PartFunc of X,COMPLEX such that
A42: A2=a.e-Ceq-class(b,M) and
A43: b in L1_CFunctions M;
A3 in C;
then consider c be PartFunc of X,COMPLEX such that
A44: A3=a.e-Ceq-class(c,M) and
A45: c in L1_CFunctions M;
A46: c in A3 by A44,A45,Th31;
A47: b in A2 by A42,A43,Th31;
then aC.(A2,A3) =a.e-Ceq-class(b+c,M) by A46,Def16;
then
A48: b+c in A2+A3 by A43,A45,Th17,Th31;
reconsider a1=a,b1=b,c1=c as VECTOR of CLSp_L1Funct M by A41,A43,A45;
b+c = b1+c1 by Th19;
then a+(b+c) =a1+(b1+c1) by Th19;
then
A49: a+(b+c) =(a1+b1)+c1 by RLVECT_1:def 3;
a+b = a1+b1 by Th19;
then
A50: a+(b+c) = a+b+c by A49,Th19;
A51: a in A1 by A40,A41,Th31;
then aC.(A1,A2) =a.e-Ceq-class(a+b,M) by A47,Def16;
then a+b in A1+A2 by A41,A43,Th17,Th31;
then A1+A2+A3 = a.e-Ceq-class(a+(b+c),M) by A46,A50,Def16;
hence thesis by A51,A48,Def16;
end;
then reconsider A as strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty CLSStruct by A1,A6,
A30,A12,CLVECT_1:def 2,def 3,def 4,def 5;
take A;
thus thesis;
end;
uniqueness;
end;
begin :: Complex Normed Space of Integrable Functions
theorem Th36:
f in L1_CFunctions M & g in L1_CFunctions M & f a.e.cpfunc= g,M implies
Integral(M,f) = Integral(M,g)
proof
assume that
A1: f in L1_CFunctions M and
A2: g in L1_CFunctions M and
A3: f a.e.cpfunc= g,M;
consider EQ being Element of S such that
A4: M.EQ = 0 and
A5: f|EQ` = g|EQ` by A3;
A6: ex f1 be PartFunc of X,COMPLEX st f=f1 & ex ND be Element of S st M.ND=0 &
dom f1 = ND` & f1 is_integrable_on M by A1;
then consider NDf be Element of S such that
A7: M.NDf=0 and
A8: dom f = NDf` and
f is_integrable_on M;
A9: M.(EQ \/ NDf) = 0 by A7,A4,Lm4;
consider E1 being Element of S such that
A10: E1 = dom f and f is E1-measurable by A6,MESFUN7C:35;
A11: ex g1 be PartFunc of X,COMPLEX st g=g1 & ex ND be Element of S st M.ND=0
& dom g1 = ND` & g1 is_integrable_on M by A2;
then consider NDg be Element of S such that
A12: M.NDg=0 and
A13: dom g = NDg` and
g is_integrable_on M;
A14: M.(EQ \/ NDg) = 0 by A12,A4,Lm4;
consider E2 being Element of S such that
A15: E2 = dom g and g is E2-measurable by A11,MESFUN7C:35;
A16: EQ` \ (NDf \/NDg) = (EQ \/ (NDf \/NDg))` by XBOOLE_1:41
.=(NDg \/ (EQ \/NDf))` by XBOOLE_1:4
.=NDg` \ (EQ \/NDf) by XBOOLE_1:41;
A17: EQ` \ (NDf \/NDg) = (EQ \/ (NDf \/NDg))` by XBOOLE_1:41
.= (NDf \/ (EQ \/NDg))` by XBOOLE_1:4
.= NDf` \ (EQ \/NDg) by XBOOLE_1:41;
A18: EQ` \ (NDf \/NDg) c= EQ` by XBOOLE_1:36;
then f|(EQ` \ (NDf \/NDg)) = g|EQ`|(EQ`\(NDf \/NDg)) by A5,FUNCT_1:51
.= g|(EQ`\(NDf \/ NDg)) by A18,FUNCT_1:51;
hence Integral(M,f) = Integral(M,g|(NDg` \(EQ\/NDf)))
by A6,A8,A10,A17,A16,A14,MESFUN6C:22
.= Integral(M,g) by A11,A13,A15,A9,MESFUN6C:22;
end;
theorem Th37:
f is_integrable_on M implies Integral(M,f) in COMPLEX &
Integral(M,|.f.|) in REAL & |.f.| is_integrable_on M
proof
assume
A1: f is_integrable_on M;
reconsider AF = |.f.| as PartFunc of X,REAL;
AF is_integrable_on M by A1,MESFUN7C:35;
hence thesis by LPSPACE1:44,XCMPLX_0:def 2;
end;
theorem Th38:
f in L1_CFunctions M & g in L1_CFunctions M & f a.e.cpfunc= g,M implies
|.f.| a.e.= |.g.|,M & Integral(M,|.f.|) = Integral(M,|.g.|)
proof
assume that
A1: f in L1_CFunctions M and
A2: g in L1_CFunctions M and
A3: f a.e.cpfunc= g,M;
reconsider AF = |. f .|, AG = |. g .| as PartFunc of X,REAL;
A4: ex f1 be PartFunc of X,COMPLEX st f=f1 & ex ND be Element of S st M.ND=0 &
dom f1 = ND` & f1 is_integrable_on M by A1;
then consider NDf be Element of S such that
A5: M.NDf=0 and
A6: dom f = NDf` and
f is_integrable_on M;
A7: AF is_integrable_on M by A4,Th37;
consider EQ being Element of S such that
A8: M.EQ = 0 and
A9: f|EQ` = g|EQ` by A3;
A10: AF|EQ` = abs(g|EQ`) by A9,CFUNCT_1:54
.= AG|EQ` by CFUNCT_1:54;
A11: ex g1 be PartFunc of X,COMPLEX st g=g1 & ex ND be Element of S st M.ND=0 &
dom g1 = ND` & g1 is_integrable_on M by A2;
then consider NDg be Element of S such that
A12: M.NDg=0 and
A13: dom g = NDg` and
g is_integrable_on M;
A14: AG is_integrable_on M by A11,Th37;
dom AG = NDg` by A13,VALUED_1:def 11;
then
A15: AG in L1_Functions M by A12,A14;
dom AF = NDf` by A6,VALUED_1:def 11;
then AF in L1_Functions M by A5,A7;
hence thesis by A15,A8,A10,LPSPACE1:def 10,LPSPACE1:43;
end;
theorem Th39:
(ex x be VECTOR of Pre-L-CSpace M st f in x & g in x) implies f
a.e.cpfunc= g,M & f in L1_CFunctions M & g in L1_CFunctions M
proof
given x be VECTOR of Pre-L-CSpace M such that
A1: f in x and
A2: g in x;
x in the carrier of Pre-L-CSpace M;
then x in CCosetSet M by Def19;
then consider h be PartFunc of X,COMPLEX such that
A3: x=a.e-Ceq-class(h,M) and
h in L1_CFunctions M;
ex k be PartFunc of X,COMPLEX st f=k & k in L1_CFunctions M & h in
L1_CFunctions M & h a.e.cpfunc= k,M by A1,A3;
then
A4: f a.e.cpfunc= h,M;
ex j be PartFunc of X,COMPLEX st g=j & j in L1_CFunctions M & h in
L1_CFunctions M & h a.e.cpfunc= j,M by A2,A3;
hence thesis by A1,A3,A4,Th24;
end;
theorem Th40:
ex NORM be Function of the carrier of Pre-L-CSpace M,REAL st for
x be Point of Pre-L-CSpace M ex f be PartFunc of X,COMPLEX
st f in x & NORM.x = Integral(M,abs f)
proof
defpred P[set,set] means ex f be PartFunc of X,COMPLEX st f in $1 & $2 =
Integral(M,abs f);
A1: for x be Point of Pre-L-CSpace M ex y being Element of REAL st P[x,y]
proof
let x be Point of Pre-L-CSpace M;
x in the carrier of Pre-L-CSpace M;
then x in CCosetSet M by Def19;
then consider f be PartFunc of X,COMPLEX such that
A2: x=a.e-Ceq-class(f,M) and
A3: f in L1_CFunctions M;
ex f0 be PartFunc of X,COMPLEX st f=f0 & ex ND be Element of S st M.ND=0
& dom f0 = ND` & f0 is_integrable_on M by A3;
then Integral(M,abs f) in REAL by Th37;
hence thesis by A2,A3,Th31;
end;
consider f being Function of Pre-L-CSpace M,REAL such that
A4: for x being Point of Pre-L-CSpace M holds P[x,f.x] from FUNCT_2:sch 3
(A1 );
take f;
thus thesis by A4;
end;
reserve x for Point of Pre-L-CSpace M;
theorem Th41:
f in x implies f is_integrable_on M & f in L1_CFunctions M & abs
f is_integrable_on M
proof
x in the carrier of Pre-L-CSpace M;
then x in CCosetSet M by Def19;
then consider h be PartFunc of X,COMPLEX such that
A1: x=a.e-Ceq-class(h,M) and
h in L1_CFunctions M;
assume f in x;
then ex g be PartFunc of X,COMPLEX st f=g & g in L1_CFunctions M & h in
L1_CFunctions M & h a.e.cpfunc= g,M by A1;
then
ex f0 be PartFunc of X,COMPLEX st f=f0 & ex ND be Element of S st M.ND=0 &
dom f0 = ND` & f0 is_integrable_on M;
hence thesis by Th37;
end;
theorem Th42:
f in x & g in x implies f a.e.cpfunc= g,M & Integral(M,f) = Integral(M,g)
& Integral(M,abs f) = Integral(M,abs g)
proof
assume that
A1: f in x and
A2: g in x;
A3: g in L1_CFunctions M by A2,Th39;
f a.e.cpfunc= g,M & f in L1_CFunctions M by A1,A2,Th39;
hence thesis by A3,Th36,Th38;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func L-1-CNorm M -> Function of the carrier of Pre-L-CSpace M,REAL means
:
Def20: for x be Point of Pre-L-CSpace M ex f be PartFunc of X,COMPLEX
st f in x & it.x = Integral(M,abs f);
existence by Th40;
uniqueness
proof
let N1,N2 be Function of the carrier of Pre-L-CSpace M,REAL;
assume
A1: ( for x be Point of Pre-L-CSpace M ex f be PartFunc of X,COMPLEX st f
in x & N1.x = Integral(M,abs f))& for x be Point of Pre-L-CSpace M ex g be
PartFunc of X,COMPLEX st g in x & N2.x = Integral(M,abs g);
now
let x be Point of Pre-L-CSpace M;
( ex f be PartFunc of X,COMPLEX st f in x & N1.x = Integral(M,abs f))&
ex g be PartFunc of X,COMPLEX st g in x & N2.x = Integral(M,abs g) by A1;
hence N1.x=N2.x by Th42;
end;
hence N1=N2 by FUNCT_2:def 8;
end;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func L-1-CSpace M -> non empty CNORMSTR equals
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;
end;
reserve x,y for Point of L-1-CSpace M;
theorem Th43:
( ex f be PartFunc of X,COMPLEX st f in L1_CFunctions M & x=
a.e-Ceq-class(f,M) & ||.x.|| = Integral(M,abs f) ) &
for f be PartFunc of X,COMPLEX
st f in x holds Integral(M,abs f) = ||.x.||
proof
reconsider y=x as Point of Pre-L-CSpace M;
consider f be PartFunc of X,COMPLEX such that
A1: f in y and
A2: (L-1-CNorm M).y = Integral(M,abs f) by Def20;
y in the carrier of Pre-L-CSpace M;
then y in CCosetSet M by Def19;
then consider g be PartFunc of X,COMPLEX such that
A3: y=a.e-Ceq-class(g,M) & g in L1_CFunctions M;
g in y by A3,Th31;
then f a.e.cpfunc= g,M by A1,Th39;
then x = a.e-Ceq-class(f,M) by A1,A3,Th32;
hence thesis by A1,A2,Th42;
end;
theorem
f in x implies x= a.e-Ceq-class(f,M) & ||.x.|| = Integral(M,abs f)
proof
assume
A1: f in x;
reconsider y=x as Point of Pre-L-CSpace M;
y in the carrier of Pre-L-CSpace M;
then y in CCosetSet M by Def19;
then consider g be PartFunc of X,COMPLEX such that
A2: y=a.e-Ceq-class(g,M) & g in L1_CFunctions M;
g in y by A2,Th31;
then f a.e.cpfunc= g,M by A1,Th39;
hence thesis by A1,A2,Th32,Th43;
end;
theorem Th45:
(f in x & g in y implies f+g in x+y) & (f in x implies a(#)f in a*x)
proof
set C = CCosetSet M;
hereby
reconsider x1=x,y1=y as Point of Pre-L-CSpace M;
assume that
A1: f in x and
A2: g in y;
y1 in the carrier of Pre-L-CSpace M;
then
A3: y1 in C by Def19;
then consider b be PartFunc of X,COMPLEX such that
A4: y1=a.e-Ceq-class(b,M) and
A5: b in L1_CFunctions M;
A6: b in y1 by A4,A5,Th31;
ex r be PartFunc of X,COMPLEX st g=r & r in L1_CFunctions M & b in
L1_CFunctions M & b a.e.cpfunc= r,M by A2,A4;
then
A7: a.e-Ceq-class(b,M) = a.e-Ceq-class(g,M) by Th32;
x1 in the carrier of Pre-L-CSpace M;
then
A8: x1 in C by Def19;
then consider a be PartFunc of X,COMPLEX such that
A9: x1=a.e-Ceq-class(a,M) and
A10: a in L1_CFunctions M;
a in x1 by A9,A10,Th31;
then (addCCoset M).(x1,y1) = a.e-Ceq-class(a+b,M) by A8,A3,A6,Def16;
then
A11: x1+y1 = a.e-Ceq-class(a+b,M) by Def19;
ex r be PartFunc of X,COMPLEX st f=r & r in L1_CFunctions M & a in
L1_CFunctions M & a a.e.cpfunc= r,M by A1,A9;
then a.e-Ceq-class(a,M) = a.e-Ceq-class(f,M) by Th32;
then
a.e-Ceq-class(a+b,M) = a.e-Ceq-class(f+g,M) by A1,A2,A9,A10,A4,A5,A7,Th34;
hence f+g in x+y by A1,A2,A9,A4,A11,Th17,Th31;
end;
hereby
reconsider x1=x as Point of Pre-L-CSpace M;
x1 in the carrier of Pre-L-CSpace M;
then
A12: x1 in C by Def19;
then consider f1 be PartFunc of X,COMPLEX such that
A13: x1=a.e-Ceq-class(f1,M) and
A14: f1 in L1_CFunctions M;
(lmultCCoset M).(a,x1) = a.e-Ceq-class(a(#)f1,M) by A13,A14,Th31,A12,Def18;
then
A15: a*x1 = a.e-Ceq-class(a(#)f1,M) by Def19;
assume
A16: f in x;
then ex r be PartFunc of X,COMPLEX st f=r & r in L1_CFunctions M & f1 in
L1_CFunctions M & f1 a.e.cpfunc= r,M by A13;
then a.e-Ceq-class(f1,M) = a.e-Ceq-class(f,M) by Th32;
then a.e-Ceq-class(a(#)f1,M) = a.e-Ceq-class(a(#)f,M) by A16,A13,A14,
Th35;
hence a(#)f in a*x by A16,A13,A15,Th18,Th31;
end;
end;
theorem
f in L1_CFunctions M & Integral(M,abs f) = 0 implies
f a.e.cpfunc= X-->0c,M
proof
assume that
A1: f in L1_CFunctions M and
A2: Integral(M,abs f) = 0;
A3: ex f1 be PartFunc of X,COMPLEX st f=f1 & ex ND be Element of S st M.ND=0 &
dom f1 = ND` & f1 is_integrable_on M by A1;
then consider NDf be Element of S such that
A4: M.NDf=0 and
A5: dom f = NDf` and f is_integrable_on M;
dom abs f = NDf` & abs f is_integrable_on M
by A3,A5,Th37,VALUED_1:def 11;
then
A6: abs f in L1_Functions M by A4;
A7: Integral(M,abs(abs f)) = 0 by A2;
consider Ef being Element of S such that
A8: M.Ef=0 and
A9: (abs f)|Ef` = (X-->0)|Ef` by A6,A7,LPSPACE1:53,LPSPACE1:def 10;
A10:dom (X-->0) = X by FUNCOP_1:13;
A11: dom ((abs f)|Ef`) = dom(abs f) /\Ef` by RELAT_1:61;
A12: dom( f|Ef`) = dom f /\ Ef` by RELAT_1:61
.= dom(abs f) /\Ef` by VALUED_1:def 11
.= dom ((abs f)|Ef`) by RELAT_1:61;
for x be object st x in dom (f|Ef`) holds f|Ef`.x = (X-->0)|Ef`.x
proof
let x be object;
assume
A13: x in dom ( f|Ef`);
A14: x in dom(abs f) & x in Ef` by A13,A12,A11,XBOOLE_0:def 4;
A15: x in dom ((X-->0)|Ef`) by A10,RELAT_1:62, A14;
A16: (abs f).x = (X-->0)|Ef`.x by A9,A13,A12, FUNCT_1:47
.= (X-->0).x by A15, FUNCT_1:47
.= 0 by A13,FUNCOP_1:7;
A17:(Re (f.x))^2 >= 0 & (Im (f.x))^2 >= 0 by XREAL_1:63;
sqrt((Re (f.x))^2 + (Im (f.x))^2)
= |.f.x.| by COMPLEX1:def 12
.=0 by A16,A14,VALUED_1:def 11; then
(Re (f.x))^2 = 0 & (Im (f.x))^2 = 0 by A17,SQUARE_1:31;
then
A18: (Re (f.x))^2 + (Im (f.x))^2 = 0;
f|Ef`.x = f.x by A13,FUNCT_1:47 .= 0 by A18,COMPLEX1:5
.= (X-->0).x by A13,FUNCOP_1:7
.=(X-->0)|Ef`.x by A15, FUNCT_1:47;
hence thesis;
end;
hence thesis by A8,A9,A12,FUNCT_1:def 11;
end;
theorem Th47:
f in L1_CFunctions M & g in L1_CFunctions M implies
Integral(M,|.f+g.|) <= Integral(M,|.f.|) + Integral(M,|.g.|)
proof
assume that
A1: f in L1_CFunctions M and
A2: g in L1_CFunctions M;
ex f1 be PartFunc of X,COMPLEX st f=f1
& ex NDf be Element of S st M.NDf=0 &
dom f1 = NDf` & f1 is_integrable_on M by A1;
then consider NDf1 be Element of S such that
A3: M.NDf1=0 and
A4: dom f = NDf1` & f is_integrable_on M;
R_EAL |.f.| is_integrable_on M by A4,Th37,MESFUNC6:def 4;
then consider Ef being Element of S such that
A5: Ef = dom R_EAL |.f.| and
A6: R_EAL |.f.| is Ef-measurable;
ex g1 be PartFunc of X,COMPLEX st g=g1
& ex NDg be Element of S st M.NDg=0 &
dom g1 = NDg` & g1 is_integrable_on M by A2;
then consider NDg1 be Element of S such that
A7: M.NDg1=0 and
A8: dom g = NDg1` & g is_integrable_on M;
R_EAL |.g.| is_integrable_on M by A8,Th37,MESFUNC6:def 4;
then consider Eg being Element of S such that
A9: Eg = dom R_EAL |.g.| and
A10: R_EAL |.g.| is Eg-measurable;
consider E be Element of S such that
A11: E = dom(f+g) &
Integral(M,(|.f+g.|)|E) <= Integral(M,(|.f.|)|E)
+ Integral(M,(|.g.|)|E) by A4,A8,MESFUN7C:42;
A12: dom(|.f+g.|) = E by A11,VALUED_1:def 11;
set NF = NDf1` /\ NDg1;
set NG = NDg1` /\ NDf1;
NDf1` is Element of S & NDg1` is Element of S by MEASURE1:def 1; then
A13: NF is Element of S & NG is Element of S &
Ef is Element of S & Eg is Element of S by MEASURE1:11;
A14: Ef = NDf1` by A4,A5,VALUED_1:def 11;
A15: Eg = NDg1` by A8,A9,VALUED_1:def 11;
then
A16: E = Ef /\ Eg by A11,A14,A4,A8,VALUED_1:def 1;
A17: Ef \Eg = (X \ NDf1) \ X \/ (X \ NDf1) /\ NDg1 by A14,A15,XBOOLE_1:52
.= X \(NDf1 \/ X) \/ (X \ NDf1) /\ NDg1 by XBOOLE_1:41
.= X \ X \/(X \ NDf1)/\ NDg1 by XBOOLE_1:12
.= {} \/ (X \ NDf1) /\ NDg1 by XBOOLE_1:37
.= NF;
A18: E = Ef \ (Ef \Eg) by A16,XBOOLE_1:48;
A19: Eg \Ef = (X \ NDg1) \ X \/ (X \ NDg1) /\ NDf1 by A14,A15,XBOOLE_1:52
.= X \(NDg1 \/ X) \/ (X \ NDg1) /\ NDf1 by XBOOLE_1:41
.= X \ X \/(X \ NDg1)/\ NDf1 by XBOOLE_1:12
.= {} \/ (X \ NDg1) /\ NDf1 by XBOOLE_1:37
.= NG;
A20: E = Eg \ (Eg \Ef) by A16,XBOOLE_1:48;
NDf1 is measure_zero of M & NDg1 is measure_zero of M
by A3,A7,MEASURE1:def 7; then
NF is measure_zero of M & NG is measure_zero of M
by A13,MEASURE1:36,XBOOLE_1:17; then
A21: M.NF = 0 & M.NG = 0 by MEASURE1:def 7;
A22: Integral(M,(|.f.|)|E) = Integral(M,(|.f.|))
by A18,A17,A6,MESFUNC6:def 1,A5,A21,MESFUNC6:89;
Integral(M,(|.g.|)|E) = Integral(M,(|.g.|))
by A10,MESFUNC6:def 1,A9,A21,A20,A19,MESFUNC6:89;
hence thesis by A11,A12,RELAT_1:69,A22;
end;
registration
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
cluster L-1-CSpace M -> ComplexNormSpace-like vector-distributive
scalar-distributive scalar-associative scalar-unital Abelian
add-associative right_zeroed right_complementable;
coherence
proof
set l = L-1-CSpace M;
l is ComplexNormSpace-like
proof
let x, y be Point of l, a be Complex;
consider f be PartFunc of X,COMPLEX such that
A1: f in x and
A2: ||.x.|| = Integral(M,abs f) by Def20;
set aa = |.a.|;
abs f is_integrable_on M by A1,Th41;
then Integral(M,|.a.|(#)abs f) = aa * Integral(M,abs f) by MESFUNC6:102;
then Integral(M,abs(a(#)f)) = aa * Integral(M,abs f) by RFUNCT_1:25;
then
A3: Integral(M,abs(a(#)f)) = |.a.| * ||.x.|| by A2;
reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;
A4: f is_integrable_on M & f in L1_CFunctions M by A1,Th41;
consider g be PartFunc of X,COMPLEX such that
A5: g in y and
A6: ||.y.|| = Integral(M,abs g) by Def20;
A7: g is_integrable_on M & g in L1_CFunctions M by A5,Th41;
A8: ||.x+y.|| = Integral(M,abs(f+g)) by A1,A5,Th45,Th43;
a1(#)f in a1*x by A1,Th45;
then A9: ||.a*x.|| = |.a.| * ||.x.|| by A3,Th43;
Integral(M,abs f) + Integral(M,abs g) = ||.x.|| + ||.y.|| by A2,A6;
then ||.x+y.|| <= ||.x.|| + ||.y.|| by A4,A8,A7,Th47;
hence thesis by A9;
end;
hence thesis by CSSPACE3:2;
end;
end;