:: On $L^1$ Space Formed by Real-valued Partial Functions
:: by Yasushige Watase , Noboru Endou and Yasunari Shidama
::
:: Received August 26, 2008
:: Copyright (c) 2008-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, REAL_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_1, FUNCOP_1,
CARD_1, RFUNCT_3, ARYTM_1, PROB_1, MEASURE1, NAT_1, INTEGRA5, MESFUNC5,
MESFUNC2, XXREAL_0, MESFUNC1, SUPINF_1, MEASURE6, VECTSP10, SETFAM_1,
COMPLEX1, PRE_TOPC, NORMSP_1, LPSPACE1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XXREAL_3, XCMPLX_0,
NUMBERS, COMPLEX1, XXREAL_0, XREAL_0, SUPINF_1, SUPINF_2, EXTREAL1,
REALSET1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
BINOP_1, NAT_1, REAL_1, STRUCT_0, ALGSTR_0, RLVECT_1, RLSUB_1,
IDEAL_1, SETFAM_1, DOMAIN_1, PRE_TOPC, NORMSP_0, NORMSP_1, PROB_1,
MEASURE1, MEASURE2, MEASURE3, MEASURE6, MESFUNC1,
VALUED_1, RFUNCT_3, FUNCOP_1, MESFUNC2, MESFUNC5,
MESFUNC6, FUNCT_7;
constructors COMPLEX1, EXTREAL1, BINOP_1, REAL_1, RLSUB_1, IDEAL_1, NORMSP_1,
MEASURE3, MEASURE6, MESFUNC2, MESFUNC5, MESFUNC6, SUPINF_1, FUNCT_7,
REALSET1, MESFUNC1, RELSET_1, BINOP_2, NUMBERS;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED,
VALUED_0, NAT_1, SUBSET_1, PARTFUN1, XXREAL_0, RLVECT_1, STRUCT_0,
NORMSP_1, MEASURE1, MESFUNC7, XXREAL_3;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, SUPINF_2, ALGSTR_0, RLVECT_1;
equalities REALSET1, BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1, IDEAL_1, MESFUNC5,
MESFUNC6, SUBSET_1, XXREAL_3, NORMSP_0;
expansions TARSKI, BINOP_1, RLVECT_1, IDEAL_1, MESFUNC5, MESFUNC6;
theorems FUNCT_1, FUNCT_2, PARTFUN1, COMPLEX1, XBOOLE_0, TARSKI, RELAT_1,
VALUED_1, RLSUB_1, ZFMISC_1, RLVECT_1, FUNCOP_1, XBOOLE_1, BINOP_1,
SUPINF_2, RFUNCT_3, MESFUNC5, MESFUNC2, EXTREAL1, MEASURE1, MESFUNC6,
PROB_1, RFUNCT_1, XXREAL_0, NUMBERS, ABSVALUE, MESFUNC1, MEASURE2,
MESFUNC7, RSSPACE3, NORMSP_1, VALUED_0, RELSET_1, XXREAL_3, XREAL_0,
SUBSET_1;
schemes BINOP_1, FUNCT_2;
begin :: Preliminaries of Real Linear Space
definition
let V be non empty RLSStruct, V1 be Subset of V;
attr V1 is multi-closed means
:Def1:
for a be Real, v be VECTOR of V st v in V1 holds a*v in V1;
end;
theorem
for V be RealLinearSpace, V1 be Subset of V holds V1 is
linearly-closed iff V1 is add-closed multi-closed
by RLSUB_1:def 1;
registration
let V be non empty RLSStruct;
cluster add-closed multi-closed non empty for 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 RLSStruct;
let X1 be multi-closed non empty Subset of X;
func Mult_X1 -> Function of [:REAL,X1:], X1 equals
(the Mult of X) | [:REAL,
X1:];
correctness
proof
A1: [:REAL,X1:] c= [:REAL,the carrier of X:] & dom the Mult of X = [:REAL,
the carrier of X:] by FUNCT_2:def 1,ZFMISC_1:95;
A2: now
let z be object;
assume
A3: z in [:REAL,X1:];
then consider r,x be object such that
A4: r in REAL and
A5: x in X1 and
A6: z=[r,x] by ZFMISC_1:def 2;
reconsider r as Real by A4;
reconsider y=x as VECTOR of X by A5;
[r,x] in dom((the Mult of X)|[:REAL,X1:]) by A1,A3,A6,RELAT_1:62;
then ((the Mult of X)|[:REAL,X1:]).z = r*y by A6,FUNCT_1:47;
hence ((the Mult of X)|[:REAL,X1:]).z in X1 by A5,Def1;
end;
dom((the Mult of X)|[:REAL,X1:])=[:REAL,X1:] by A1,RELAT_1:62;
hence thesis by A2,FUNCT_2:3;
end;
end;
reserve a,b,r for Real;
theorem Th2:
for V be Abelian add-associative right_zeroed
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty RLSStruct, V1 be non empty Subset of V, d1 be
Element of V1, A be BinOp of V1, M be Function of [:REAL,V1:],V1 st d1 = 0.V &
A = (the addF of V)|| V1 & M = (the Mult of V)|[:REAL,V1:] holds RLSStruct(# V1
,d1,A,M #) is Abelian 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 RLSStruct, V1 be non empty Subset of V, d1 be Element of V1, A be BinOp
of V1, M be Function of [:REAL,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)|[:REAL,V1:];
set W = RLSStruct(# D,d1,A,M #);
A4: now
let a;
reconsider aa=a as Element of REAL by XREAL_0:def 1;
let x be VECTOR of W;
thus a * x = (the Mult of V).[aa,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 Real;
let x,y be VECTOR of W;
reconsider a=a1 as Real;
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 RLVECT_1:def 5
.= Av.(Mv.(a,x1),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 Real;
let x be VECTOR of W;
reconsider a=a1,b=b1 as Real;
reconsider y = x as VECTOR of V by TARSKI:def 3;
(a + b) * x = (a + b) * y by A4
.= a * y + b * y by RLVECT_1:def 6
.= Av.(Mv.(a,y),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 Real;
let x be VECTOR of W;
reconsider a=a1,b=b1 as Real;
reconsider y = x as VECTOR of V by TARSKI:def 3;
(a * b) * x = (a * b) * y by A4
.= a * (b * y) by RLVECT_1:def 7
.= 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 1 * x = 1 * y by A4
.= x by RLVECT_1:def 8;
end;
hence thesis;
end;
theorem Th3:
for V be Abelian add-associative right_zeroed
vector-distributive scalar-distributive scalar-associative scalar-unital
non empty RLSStruct, V1 be add-closed multi-closed non
empty Subset of V st 0.V in V1 holds RLSStruct (# 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 RLSStruct, 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;
theorem Th4:
for V be non empty RLSStruct, V1 be add-closed multi-closed non
empty Subset of V, v,u be VECTOR of V, w1,w2 be VECTOR of RLSStruct (# V1,In(0.
V,V1), add|(V1,V), Mult_ V1 #) st w1 = v & w2 = u holds w1 + w2 = v + u
by ZFMISC_1:87,FUNCT_1:49;
theorem Th5:
for V be non empty RLSStruct, V1 be add-closed multi-closed non
empty Subset of V,
a be Real, v be VECTOR of V, w be VECTOR of RLSStruct (# V1,
In (0.V, V1), add|(V1,V), Mult_ V1 #) st w = v holds a*w = a*v
proof
let V be non empty RLSStruct, V1 be add-closed multi-closed non empty Subset
of V, a be Real,
v be VECTOR of V, w be VECTOR of RLSStruct (# V1,In (0.V, V1),
add|(V1,V),Mult_ V1 #);
reconsider a as Element of REAL by XREAL_0:def 1;
assume
A1: w = v;
then [a,v] in [:REAL,V1:] by ZFMISC_1:87;
hence thesis by A1,FUNCT_1:49;
end;
begin :: Quasi-Real Linear Space of Partial Functions
reserve A,B for non empty set;
reserve f,g,h for Element of PFuncs(A,REAL);
definition
let A,B;
let F be BinOp of PFuncs(A,B), f,g be Element of PFuncs(A,B);
redefine func F.(f,g) -> Element of PFuncs(A,B); :: redefines . (BINOP_1, definition)
coherence
proof
reconsider f,g as Element of PFuncs(A,B);
F.(f,g) is Element of PFuncs(A,B);
hence thesis;
end;
end;
definition
let A;
func multpfunc A -> BinOp of PFuncs(A,REAL) means
:Def3:
for f,g being Element of PFuncs(A,REAL) holds it.(f,g) = f(#)g;
existence
proof
deffunc F(Element of PFuncs(A,REAL),Element of PFuncs(A,REAL)) = $1(#)$2;
ex F being BinOp of PFuncs(A,REAL) 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,REAL) 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 multrealpfunc A -> Function of [:REAL,PFuncs(A,REAL):],PFuncs(A,REAL)
means
:Def4:
for a being Real,
f being Element of PFuncs(A,REAL) holds it.(a,f) = a(#)f;
existence
proof
deffunc F(Element of REAL,Element of PFuncs(A,REAL)) = $1(#)$2;
consider F being Function of [:REAL,PFuncs(A,REAL):],PFuncs(A,REAL)
such that
A1: for a being Element of REAL,f holds F.(a,f) = F(a,f) from BINOP_1:sch 4;
take F;
let a be Real, f be Element of PFuncs(A,REAL);
reconsider a as Element of REAL by XREAL_0:def 1;
F.(a,f) = F(a,f) by A1;
hence thesis;
end;
uniqueness
proof
let it1,it2 be Function of [:REAL,PFuncs(A,REAL):],PFuncs(A,REAL) such
that
A2: for a being Real,
f being Element of PFuncs(A,REAL) holds it1.(a,f) = a(#)f and
A3: for a being Real,
f being Element of PFuncs(A,REAL) holds it2.(a,f) = a(#)f;
now
let a be Element of REAL, f be Element of PFuncs(A,REAL);
thus it1.(a,f) = a(#)f by A2
.= it2.(a,f) by A3;
end;
hence thesis;
end;
end;
definition
let A;
func RealPFuncZero A -> Element of PFuncs(A,REAL) equals
A --> 0;
coherence
proof
A -->In(0,REAL) is Function of A,REAL;
hence thesis by PARTFUN1:45;
end;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
definition
let A;
func RealPFuncUnit A -> Element of PFuncs(A,REAL) equals
A --> 1;
coherence
proof
A -->jj is Function of A,REAL;
hence thesis by PARTFUN1:45;
end;
end;
theorem Th6:
h = (addpfunc A).(f,g) iff (dom h= dom f /\ dom g & for x being
Element of A st x in dom h holds h.x = f.x + g.x)
proof
hereby
assume
A1: h = (addpfunc A).(f,g);
then dom h = dom(f+g) by RFUNCT_3:def 4;
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,RFUNCT_3:def 4;
h.x = (f+g).x by A1,RFUNCT_3:def 4;
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=(addpfunc A).(f,g);
A5: now
let x be Element of A;
A6: k.x = (f+g).x by RFUNCT_3:def 4;
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 RFUNCT_3:def 4
.= dom h by A3,VALUED_1:def 1;
hence thesis by A5,PARTFUN1:5;
end;
theorem Th7:
h = (multpfunc A).(f,g) iff dom h = dom f /\ dom g & for x being
Element of A st x in dom h holds h.x = f.x * g.x
proof
set k=(multpfunc A).(f,g);
hereby
assume
A1: h = (multpfunc 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
RealPFuncZero A <> RealPFuncUnit A
proof
set a = the Element of A;
(RealPFuncZero A).a=0 by FUNCOP_1:7;
hence thesis by FUNCOP_1:7;
end;
theorem Th9:
h = (multrealpfunc 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 = (multrealpfunc 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 aa=a as Element of REAL by XREAL_0:def 1;
reconsider k= (multrealpfunc A).(aa,f) as Element of PFuncs(A,REAL);
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 = (multrealpfunc A).(a,f) by A2,A4,PARTFUN1:5;
end;
end;
theorem Th10:
(addpfunc A).(f,g) = (addpfunc A).(g,f)
by RFUNCT_3:14,BINOP_1:def 2;
theorem Th11:
(addpfunc A).(f,(addpfunc A).(g,h)) = (addpfunc A).((addpfunc A) .(f,g),h)
by RFUNCT_3:15,BINOP_1:def 3;
theorem
(multpfunc A).(f,g) = (multpfunc A).(g,f)
proof
A1: dom((multpfunc A).(g,f)) = dom g/\ dom f by Th7;
A2: dom((multpfunc A).(f,g)) = dom f/\ dom g by Th7;
now
let x be Element of A;
assume
A3: x in dom f /\ dom g;
hence ((multpfunc A).(f,g)).x = g.x * f.x by A2,Th7
.= ((multpfunc A).(g,f)).x by A1,A3,Th7;
end;
hence thesis by A2,A1,PARTFUN1:5;
end;
theorem
(multpfunc A).(f,(multpfunc A).(g,h)) = (multpfunc A).((multpfunc A).(
f,g),h)
proof
set j = (multpfunc A).(g,h);
set k = (multpfunc A).(f,g);
set j1 = (multpfunc A).(f,j);
set k1 = (multpfunc A).(k,h);
A1: dom k1 = dom k /\ dom h by Th7;
then
A2: dom k1 c= dom k by XBOOLE_1:17;
A3: dom k1 = (dom f /\ dom g)/\dom h by A1,Th7;
A4: dom j1 = dom f /\ dom j by Th7;
then
A5: dom j1 = dom f/\(dom g /\dom h) by Th7;
A6: dom j1 c= dom j by A4,XBOOLE_1:17;
now
let x be Element of A;
assume
A7: x in dom j1;
then
A8: x in dom k1 by A5,A3,XBOOLE_1:16;
thus j1.x =f.x * j.x by A7,Th7
.= f.x * (g.x * h.x) by A6,A7,Th7
.= (f.x * g.x) * h.x
.= k.x * h.x by A2,A8,Th7
.= k1.x by A8,Th7;
end;
hence thesis by A5,A3,PARTFUN1:5,XBOOLE_1:16;
end;
theorem
(multpfunc A).(RealPFuncUnit A,f) = f
proof
set h = (multpfunc A).(RealPFuncUnit A,f);
dom h = dom(RealPFuncUnit A) /\ dom f by Th7;
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 = (RealPFuncUnit A).x * f.x by A1,Th7;
then h.x = 1 * f.x by FUNCOP_1:7;
hence h.x = f.x;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th15:
(addpfunc A).(RealPFuncZero A,f) = f
proof
set h = (addpfunc A).(RealPFuncZero A,f);
dom h = dom(RealPFuncZero A) /\ dom f by Th6;
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: (RealPFuncZero A).x = 0 by FUNCOP_1:7;
assume x in dom f;
hence h.x=0+ f.x by A1,A2,Th6
.= f.x;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th16:
(addpfunc A).(f,(multrealpfunc A).(-1,f)) = (RealPFuncZero A)|( dom f)
proof
reconsider g = (multrealpfunc A).(-jj,f) as Element of PFuncs(A,REAL);
set h = (addpfunc A).(f,g);
dom (RealPFuncZero A) = A by FUNCOP_1:13;
then dom ((RealPFuncZero A)|(dom f)) = A /\ dom f by RELAT_1:61;
then
A1: dom ((RealPFuncZero A)|(dom f)) = dom f by XBOOLE_1:28;
A2: dom h = dom g /\ dom f by Th6
.= dom f /\ dom f by Th9;
now
let x be Element of A;
assume
A3: x in dom f;
then
A4: x in dom((-1)(#)f) by VALUED_1:def 5;
thus h.x = f.x + g.x by A2,A3,Th6
.= f.x + ((-1)(#)f).x by Def4
.= f.x + (-1) * f.x by A4,VALUED_1:def 5
.= (RealPFuncZero A).x by FUNCOP_1:7
.= ((RealPFuncZero A)|(dom f)).x by A3,FUNCT_1:49;
end;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem Th17:
(multrealpfunc A).(1,f) = f
proof
reconsider g = (multrealpfunc A).(jj,f) as Element of PFuncs(A,REAL);
A1: now
let x be Element of A;
assume x in dom f;
hence g.x = 1*(f.x) by Th9
.= f.x;
end;
dom g=dom f by Th9;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th18:
(multrealpfunc A).(a,(multrealpfunc A).(b,f)) = (multrealpfunc A ).(a*b,f)
proof
reconsider aa=a, bb=b as Element of REAL by XREAL_0:def 1;
reconsider g = (multrealpfunc A).(bb,f) as Element of PFuncs(A,REAL);
reconsider h = (multrealpfunc A).(aa,g) as Element of PFuncs(A,REAL);
reconsider k = (multrealpfunc A).(aa*bb,f) as Element of PFuncs(A,REAL);
A1: dom h = dom g by Th9;
A2: dom g = dom f by Th9;
A3: now
let x be Element of A;
assume
A4: x in dom h;
hence h.x =a*(g.x) by A1,Th9
.=a*(b*(f.x)) by A2,A1,A4,Th9
.=(a*b)*(f.x)
.= k.x by A2,A1,A4,Th9;
end;
dom k = dom f by Th9;
hence thesis by A2,A1,A3,PARTFUN1:5;
end;
theorem Th19:
(addpfunc A).((multrealpfunc A).(a,f),(multrealpfunc A).(b,f)) =
(multrealpfunc A).(a+b,f)
proof
reconsider aa=a, bb=b as Element of REAL by XREAL_0:def 1;
reconsider g = (multrealpfunc A).(aa,f) as Element of PFuncs(A,REAL);
reconsider h = (multrealpfunc A).(bb,f) as Element of PFuncs(A,REAL);
reconsider k = (multrealpfunc A).(aa+bb,f) as Element of PFuncs(A,REAL);
set j = (addpfunc A).(g,h);
dom g = dom f by Th9;
then dom h /\ dom g = dom f /\ dom f by Th9;
then
A1: dom j = dom f by Th6;
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,Th6
.= k.x by A1,A3,Th9;
end;
dom k = dom f by Th9;
hence thesis by A1,A2,PARTFUN1:5;
end;
Lm1: (addpfunc A).((multrealpfunc A).(a,f),(multrealpfunc A).(a,g)) = (
multrealpfunc A).(a,(addpfunc A).(f,g))
proof
reconsider aa=a as Element of REAL by XREAL_0:def 1;
reconsider h = (multrealpfunc A).(aa,f) as Element of PFuncs(A,REAL);
reconsider i = (multrealpfunc A).(aa,g) as Element of PFuncs(A,REAL);
set j = (addpfunc A).(f,g);
reconsider k = (multrealpfunc A).(aa,j) as Element of PFuncs(A,REAL);
set l = (addpfunc A).(h,i);
A1: dom h = dom f & dom i = dom g by Th9;
A2: dom l = dom h /\ dom i by Th6;
A3: dom j = dom f /\ dom g by Th6;
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 Th9;
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 Th9;
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,Th6
.= a*(f.x+g.x) by A10,A9
.= a*(f+g).x by A7,VALUED_1:def 1
.= a*j.x by RFUNCT_3:def 4
.= k.x by A1,A3,A2,A6,Th9;
end;
dom k = dom j by Th9;
hence thesis by A1,A3,A2,A4,PARTFUN1:5;
end;
theorem
(multpfunc A).(f,(addpfunc A).(g,h)) = (addpfunc A).((multpfunc A).(f,
g),(multpfunc A).(f,h))
proof
set i = (multpfunc A).(f,h);
set j = (multpfunc A).(f,g);
set k = (addpfunc A).(j,i);
set l = (addpfunc A).(g,h);
set m = (multpfunc 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 Th7;
then dom k = (dom h /\ dom f) /\ (dom f /\ dom g) by Th6;
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,Th6;
then l.x = (g+h).x & k.x = f.x * (g.x + h.x) by A8,A10,RFUNCT_3:def 4;
then
A11: k.x = f.x * l.x by A7,VALUED_1:def 1;
x in dom f /\ dom l by A2,A1,A5,Th6;
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 Th6,Th7;
hence thesis by A2,A4,PARTFUN1:5,XBOOLE_1:16;
end;
theorem
(multpfunc A).((multrealpfunc A).(a,f),g) = (multrealpfunc A).(a,(
multpfunc A).(f,g))
proof
reconsider aa=a as Element of REAL by XREAL_0:def 1;
reconsider i = (multrealpfunc A).(aa,f) as Element of PFuncs(A,REAL);
set j = (multpfunc A).(f,g);
set k = (multpfunc A).(i,g);
reconsider l = (multrealpfunc A).(aa,j) as Element of PFuncs(A,REAL);
A1: dom i = dom f & dom k = dom i /\ dom g by Th7,Th9;
A2: dom j = dom f /\ dom g by Th7;
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,Th7;
hence k.x = l.x by A8,A10;
end;
dom l = dom j by Th9;
hence thesis by A1,A2,A3,PARTFUN1:5;
end;
definition
let A;
func RLSp_PFunctA -> non empty RLSStruct equals
RLSStruct(#PFuncs(A,REAL),
RealPFuncZero A, addpfunc A, multrealpfunc A#);
coherence;
end;
reserve u,v,w for VECTOR of RLSp_PFunctA;
registration
let A;
cluster RLSp_PFunctA -> strict Abelian add-associative right_zeroed
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence
proof
set IT = RLSp_PFunctA;
thus IT is strict;
thus u+v = v+u by Th10;
thus u+v+w = u+(v+w) by Th11;
thus u+0.IT = u
proof
reconsider u9=u as Element of PFuncs(A,REAL);
thus u+0.IT = (addpfunc(A)).(RealPFuncZero(A),u9) by Th10
.= u by Th15;
end;
thus for a being Real,u,v holds a*(u+v) = a*u + a *v
by Lm1;
thus for a,b being Real,v holds (a+b)*v = a*v + b*v
by Th19;
thus for a,b being Real,v holds (a*b)*v = a*(b*v)
by Th18;
let v;
thus 1 * v = v by Th17;
end;
end;
begin :: Quasi-Real 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 for Element of S,
f,g,h,f1,g1 for PartFunc of X ,REAL;
theorem Th22:
for X,S,M for f be PartFunc of X,ExtREAL st (ex E st E = dom f)
& for x st x in dom f holds 0= f.x holds f is_integrable_on M & Integral(M,f) =
0
proof
let X,S,M;
let f be PartFunc of X,ExtREAL;
given E such that
A1: E = dom f;
assume
A2: for x st x in dom f holds 0 = f.x;
then
A3: for x be object st x in dom f holds f.x = 0;
then
A4: f is_simple_func_in S by A1,MESFUNC6:2;
then
A5: integral+(M,f) = 0 by A1,A2,MESFUNC2:34,MESFUNC5:87;
A6: dom max+f = dom f by MESFUNC2:def 2;
A7: now
let x be Element of X;
assume
A8: x in dom f;
hence f.x = max(0,0) by A2
.=max(f.x,0) by A2,A8
.= (max+f).x by A6,A8,MESFUNC2:def 2;
end;
A9: f is E-measurable by A1,A3,MESFUNC2:34,MESFUNC6:2;
A10: f is nonnegative
proof
let y be ExtReal;
assume y in rng f;
then ex x1 being object st x1 in dom f & y = f.x1 by FUNCT_1:def 3;
hence y >= 0 by A2;
end;
then 0. = Integral(M,f) by A1,A4,A5,MESFUNC2:34,MESFUNC5:88
.= integral+(M,f)-integral+(M,max-f) by A6,A7,PARTFUN1:5
.= 0.+(-integral+(M,max-f)) by A1,A2,A4,MESFUNC2:34,MESFUNC5:87
.= -integral+(M,max-f) by XXREAL_3:4;
then
A11: --integral+(M,max-f) = -0;
integral+(M,max+f) < +infty by A6,A7,A5,PARTFUN1:5;
hence f is_integrable_on M by A1,A9,A11;
thus thesis by A1,A9,A5,A10,MESFUNC5:88;
end;
definition
let X be non empty set, r be Real;
redefine func X --> r -> PartFunc of X,REAL; :: redefines --> (FUNCOP_1, definition)
coherence
proof
reconsider r as Element of REAL by XREAL_0:def 1;
X --> r is PartFunc of X,REAL;
hence thesis;
end;
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
A2: X=dom f & for x st x in dom f holds 0 = f.x;
then R_EAL f is_integrable_on M by A1,Th22;
hence thesis by A2,Th22;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func L1_Functions M -> non empty Subset of RLSp_PFunctX equals
{ f where f
is PartFunc of X,REAL : 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:34;
set g = X --> 0;
set I = { f where f is PartFunc of X,REAL : ex ND be Element of S st M.ND=
0 & dom f = ND` & f is_integrable_on M };
A1: I c= PFuncs(X,REAL)
proof
let x be object;
assume x in I;
then
ex f be PartFunc of X,REAL 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 is PartFunc of X,REAL & X --> 0 in L1_Functions M
proof
reconsider g = X --> In(0,REAL) as Function of X,REAL by FUNCOP_1:46;
reconsider ND = {} as Element of S by MEASURE1:34;
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;
then E1 \/ E2 is measure_zero of M by MEASURE1:37;
hence thesis by MEASURE1:def 7;
end;
theorem Th23:
f in L1_Functions M & g in L1_Functions M implies f + g in L1_Functions M
proof
set W = L1_Functions M;
assume that
A1: f in W and
A2: g in W;
ex f1 be PartFunc of X,REAL 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,REAL 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,MESFUNC6:100;
hence thesis by A9;
end;
theorem Th24:
f in L1_Functions M implies a(#)f in L1_Functions M
proof
set W = L1_Functions M;
assume f in W;
then
ex f1 be PartFunc of X,REAL 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,MESFUNC6:102
,VALUED_1:def 5;
hence thesis by A1;
end;
Lm5: L1_Functions M is add-closed & L1_Functions M is multi-closed
proof
set W = L1_Functions M;
now
let v,u be Element of RLSp_PFunctX such that
A1: v in W and
A2: u in W;
reconsider h = v+u as Element of PFuncs(X,REAL);
consider v1 be PartFunc of X, REAL 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, REAL 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,Th6;
then v+u=v1+u1 by VALUED_1:def 1;
hence v+u in L1_Functions M by A1,A2,A3,A4,Th23;
end;
hence L1_Functions M is add-closed;
now
let a be Real, u be VECTOR of RLSp_PFunctX such that
A5: u in W;
consider u1 be PartFunc of X, REAL 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 = a*u as Element of PFuncs(X,REAL);
A7: dom h = dom u1 by A6,Th9;
then for x be object st x in dom h holds h.x = a*(u1.x) by A6,Th9;
then a*u=a(#)u1 by A7,VALUED_1:def 5;
hence a*u in L1_Functions M by A5,A6,Th24;
end;
hence thesis;
end;
registration
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
cluster L1_Functions 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 RLSp_L1Funct M -> non empty RLSStruct equals
RLSStruct (# L1_Functions
M, In (0.(RLSp_PFunctX), L1_Functions M), add|(L1_Functions M,RLSp_PFunctX),
Mult_(L1_Functions M) #);
coherence;
end;
registration
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
cluster RLSp_L1Funct M -> strict Abelian add-associative right_zeroed
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence
proof
0.(RLSp_PFunctX) in L1_Functions M by Lm3;
hence thesis by Th3;
end;
end;
begin :: Quotient Space of Quasi-Real Linear Space of Integrable Functions
reserve v,u for VECTOR of RLSp_L1Funct M;
theorem Th25:
f=v & g=u implies f+g=v+u
proof
reconsider v2=v as VECTOR of RLSp_PFunct(X) by TARSKI:def 3;
reconsider u2=u as VECTOR of RLSp_PFunct(X) by TARSKI:def 3;
reconsider h = v2+u2 as Element of PFuncs(X,REAL);
reconsider v3= v2 as Element of PFuncs(X,REAL);
reconsider u3= u2 as Element of PFuncs(X,REAL);
A1: dom h= dom v3 /\ dom u3 by Th6;
assume
A2: f=v & g=u;
then for x be object st x in dom h holds h.x = f.x + g.x by Th6;
then h= f+g by A2,A1,VALUED_1:def 1;
hence thesis by Th4;
end;
theorem Th26:
f=u implies a(#)f=a*u
proof
reconsider u2=u as VECTOR of RLSp_PFunctX by TARSKI:def 3;
reconsider h = a*u2 as Element of PFuncs(X,REAL);
assume
A1: f=u;
then
A2: dom h = dom f by Th9;
then for x be object st x in dom h holds h.x = a*(f.x) by A1,Th9;
then h= a(#)f by A2,VALUED_1:def 5;
hence thesis by Th5;
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,REAL;
pred f a.e.= g,M means
ex E be Element of S st M.E = 0 & f|E` = g|E`;
end;
theorem Th27:
f=u implies u+(-1)*u = (X --> 0)|dom f & ex v,g be PartFunc of X
,REAL st v in L1_Functions M & g in L1_Functions M & v = u+(-1)*u & g = X --> 0
& v a.e.= g,M
proof
reconsider u2=u as VECTOR of RLSp_PFunctX by TARSKI:def 3;
reconsider h = u2+(-1)*u2 as Element of PFuncs(X,REAL);
set g = X-->0;
u+(-1)*u in L1_Functions M;
then consider v be PartFunc of X,REAL such that
A1: v=u+(-1)*u and
ex ND be Element of S st M.ND=0 & dom v = ND` & v is_integrable_on M;
assume
A2: f=u;
then
A3: h = (RealPFuncZero X)|dom f by Th16;
u in L1_Functions M;
then
ex uu1 be PartFunc of X,REAL 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;
A6: (-1)*u2=(-1)*u by Th5;
hence u+(-1)*u = (X --> 0)|dom f by A3,Th4;
v|ND` = g|ND`|ND` by A3,A6,A1,A5,Th4;
then v|ND` = g|ND` by FUNCT_1:51;
then
A7: v a.e.= g,M by A4;
g in L1_Functions M by Lm3;
hence thesis by A1,A7;
end;
theorem Th28:
f a.e.= f,M
proof
{} is Element of S by PROB_1:4;
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.= g,M implies g a.e.= f,M;
theorem Th30:
f a.e.= g,M & g a.e.= h,M implies f a.e.= h,M
proof
assume that
A1: f a.e.= g,M and
A2: g a.e.= 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 Th31:
f a.e.= f1,M & g a.e.= g1,M implies (f+g) a.e.= (f1+g1),M
proof
assume that
A1: f a.e.= f1,M and
A2: g a.e.= 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 Th32:
f a.e.= g,M implies a(#)f a.e.= a(#)g,M
proof
assume f a.e.= 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 AlmostZeroFunctions M -> non empty Subset of RLSp_L1Funct M equals
{ f
where f is PartFunc of X,REAL : f in L1_Functions M & f a.e.= X-->0,M };
coherence
proof
A1: now
let x be object;
assume x in { f where f is PartFunc of X,REAL: f in L1_Functions M & f
a.e.= X-->0,M };
then
ex f be PartFunc of X,REAL st x=f & f in L1_Functions M & f a.e.= X
-->0,M;
hence x in the carrier of RLSp_L1Funct M;
end;
X-->0 a.e.= X-->0,M & X-->0 in L1_Functions M by Lm3,Th28;
then X-->0 in { f where f is PartFunc of X,REAL : f in L1_Functions M & f
a.e.= X-->0,M };
hence thesis by A1,TARSKI:def 3;
end;
end;
theorem Th33:
(X-->0) + (X-->0) = X-->0 & a(#)(X-->0) = X-->0
proof
set g1 = X-->0;
set g2 = X-->0;
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 --> 0).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 --> 0);
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 --> 0).x;
end;
hence g1+g2 = X-->0 by A2,PARTFUN1:5;
dom(a(#)g1) = dom(X-->0) by VALUED_1:def 5;
hence thesis by A1,PARTFUN1:5;
end;
Lm6: AlmostZeroFunctions M is add-closed & AlmostZeroFunctions M is
multi-closed
proof
set Z = AlmostZeroFunctions M;
set V = RLSp_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, REAL such that
A3: v1=v and
v1 in L1_Functions M and
A4: v1 a.e.= X-->0,M by A1;
consider u1 be PartFunc of X, REAL such that
A5: u1=u and
u1 in L1_Functions M and
A6: u1 a.e.= X-->0,M by A2;
A7: v+u=v1+u1 by A3,A5,Th25;
(X-->0)+(X-->0)=X-->0 by Th33;
then v1+u1 a.e.=X-->0,M by A4,A6,Th31;
hence v+u in Z by A7;
end;
hence Z is add-closed;
now
let a be Real, u be VECTOR of V;
assume u in Z;
then consider u1 be PartFunc of X, REAL such that
A8: u1=u and
u1 in L1_Functions M and
A9: u1 a.e.= X-->0,M;
A10: a*u=a(#)u1 by A8,Th26;
a(#)(X-->0)=X-->0 by Th33;
then a(#)u1 a.e.=X-->0,M by A9,Th32;
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 AlmostZeroFunctions M -> add-closed multi-closed;
coherence by Lm6;
end;
theorem
0.(RLSp_L1Funct M) = X-->0 & 0.(RLSp_L1Funct M) in AlmostZeroFunctions M
proof
thus 0.(RLSp_L1Funct M) = X --> 0 by Lm3,SUBSET_1:def 8;
X-->0 a.e.= X-->0,M & 0.(RLSp_L1Funct M) = 0.(RLSp_PFunctX) by Lm3,Th28,
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 RLSp_AlmostZeroFunct M -> non empty RLSStruct equals
RLSStruct (#
AlmostZeroFunctions M, In(0.(RLSp_L1Funct M),AlmostZeroFunctions M), add|(
AlmostZeroFunctions M,RLSp_L1Funct M), Mult_(AlmostZeroFunctions M) #);
coherence;
end;
registration
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
cluster RLSp_L1Funct M -> strict strict Abelian add-associative right_zeroed
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence;
end;
reserve v,u for VECTOR of RLSp_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 RLSp_L1Funct M by TARSKI:def 3;
thus v+u=v2+u2 by Th4
.=f+g by A1,Th25;
end;
theorem
f=u implies a(#)f=a*u
proof
assume
A1: f=u;
reconsider u2=u as VECTOR of RLSp_L1Funct M by TARSKI:def 3;
thus a*u=a*u2 by Th5
.=a(#)f by A1,Th26;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be
PartFunc of X,REAL;
func a.e-eq-class(f,M) -> Subset of L1_Functions M equals
{g where g is
PartFunc of X,REAL : g in L1_Functions M & f in L1_Functions M & f a.e.= g,M };
correctness
proof
now
let x be object;
assume x in {g where g is PartFunc of X,REAL : g in L1_Functions M & f
in L1_Functions M & f a.e.= g,M };
then ex g be PartFunc of X,REAL st x=g & g in L1_Functions M & f in
L1_Functions M & f a.e.= g,M;
hence x in L1_Functions M;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem Th37:
f in L1_Functions M & g in L1_Functions M implies (g a.e.= f,M
iff g in a.e-eq-class(f,M))
proof
assume
A1: f in L1_Functions M & g in L1_Functions M;
hereby
assume g a.e.= f,M;
then f a.e.= g,M;
hence g in a.e-eq-class(f,M) by A1;
end;
hereby
assume g in a.e-eq-class(f,M);
then ex r be PartFunc of X,REAL st g=r & r in L1_Functions M & f in
L1_Functions M & f a.e.= r,M;
hence g a.e.= f,M;
end;
end;
theorem Th38:
f in L1_Functions M implies f in a.e-eq-class(f,M)
proof
hereby
assume
A1: f in L1_Functions M;
f a.e.= f,M by Th28;
hence f in a.e-eq-class(f,M) by A1;
end;
end;
theorem Th39:
f in L1_Functions M & g in L1_Functions M implies (a.e-eq-class(
f,M) = a.e-eq-class(g,M) iff f a.e.= g,M)
proof
assume that
A1: f in L1_Functions M and
A2: g in L1_Functions M;
hereby
assume a.e-eq-class(f,M) = a.e-eq-class(g,M);
then f in {r where r is PartFunc of X,REAL : r in L1_Functions M & g in
L1_Functions M & g a.e.= r,M } by A1,Th38;
then ex r be PartFunc of X,REAL st f=r & r in L1_Functions M & g in
L1_Functions M & g a.e.= r,M;
hence f a.e.= g,M;
end;
assume
A3: f a.e.= g,M;
now
let x be object;
assume x in a.e-eq-class(f,M);
then consider r be PartFunc of X,REAL such that
A4: x=r & r in L1_Functions M and
f in L1_Functions M and
A5: f a.e.= r,M;
g a.e.= f,M by A3;
then g a.e.= r,M by A5,Th30;
hence x in a.e-eq-class(g,M) by A2,A4;
end;
then
A6: a.e-eq-class(f,M) c= a.e-eq-class(g,M);
now
let x be object;
assume x in a.e-eq-class(g,M);
then consider r be PartFunc of X,REAL such that
A7: x=r & r in L1_Functions M and
g in L1_Functions M and
A8: g a.e.= r,M;
f a.e.= r,M by A3,A8,Th30;
hence x in a.e-eq-class(f,M) by A1,A7;
end;
then a.e-eq-class(g,M) c= a.e-eq-class(f,M);
hence thesis by A6,XBOOLE_0:def 10;
end;
theorem
f in L1_Functions M & g in L1_Functions M implies (a.e-eq-class(f,M) =
a.e-eq-class(g,M) iff g in a.e-eq-class(f,M))
proof
assume
A1: f in L1_Functions M & g in L1_Functions M;
then g a.e.= f,M iff g in a.e-eq-class(f,M) by Th37;
hence thesis by A1,Th39;
end;
theorem Th41:
f in L1_Functions M & f1 in L1_Functions M & g in L1_Functions M
& g1 in L1_Functions M & a.e-eq-class(f,M) = a.e-eq-class(f1,M) & a.e-eq-class(
g,M) = a.e-eq-class(g1,M) implies a.e-eq-class(f+g,M) = a.e-eq-class(f1+g1,M)
proof
assume that
A1: f in L1_Functions M & f1 in L1_Functions M & g in L1_Functions M &
g1 in L1_Functions M and
A2: a.e-eq-class(f,M) = a.e-eq-class(f1,M) & a.e-eq-class(g,M) =
a.e-eq-class(g1,M);
f a.e.= f1,M & g a.e.= g1,M by A1,A2,Th39;
then
A3: f + g a.e.= f1+g1,M by Th31;
f + g in L1_Functions M & f1+g1 in L1_Functions M by A1,Th23;
hence thesis by A3,Th39;
end;
theorem Th42:
f in L1_Functions M & g in L1_Functions M & a.e-eq-class(f,M) =
a.e-eq-class(g,M) implies a.e-eq-class(a(#)f,M) = a.e-eq-class(a(#)g,M)
proof
assume that
A1: f in L1_Functions M & g in L1_Functions M and
A2: a.e-eq-class(f,M) = a.e-eq-class(g,M);
f a.e.= g,M by A1,A2,Th39;
then
A3: a(#)f a.e.= a(#)g,M by Th32;
a(#)f in L1_Functions M & a(#)g in L1_Functions M by A1,Th24;
hence thesis by A3,Th39;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func CosetSet M -> non empty Subset-Family of L1_Functions M equals
{
a.e-eq-class(f,M) where f is PartFunc of X,REAL : f in L1_Functions M};
correctness
proof
set C = {a.e-eq-class(f,M) where f is PartFunc of X,REAL : f in
L1_Functions M};
A1: C c= bool L1_Functions M
proof
let x be object;
assume x in C;
then ex f be PartFunc of X,REAL st a.e-eq-class(f,M) = x & f in
L1_Functions M;
hence thesis;
end;
X-->0 in L1_Functions M by Lm3;
then a.e-eq-class(X-->0,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 addCoset M -> BinOp of CosetSet M means
:Def15:
for A,B be Element of
CosetSet M, a,b be PartFunc of X,REAL st a in A & b in B holds it.(A,B) =
a.e-eq-class(a+b,M);
existence
proof
defpred P[set,set,set] means for a,b be PartFunc of X,REAL st a in $1& b
in $2 holds $3 = a.e-eq-class(a+b,M);
set C = CosetSet M;
A1: now
let A,B be Element of C;
A in C;
then consider a be PartFunc of X,REAL such that
A2: A=a.e-eq-class(a,M) and
A3: a in L1_Functions M;
B in C;
then consider b be PartFunc of X,REAL such that
A4: B=a.e-eq-class(b,M) and
A5: b in L1_Functions M;
set z = a.e-eq-class(a+b,M);
A6: a+b in L1_Functions M by A3,A5,Th23;
then z in C;
then reconsider z as Element of C;
take z;
now
let a1,b1 be PartFunc of X,REAL;
assume
A7: a1 in A & b1 in B;
then a1 a.e.= a,M & b1 a.e.= b,M by A2,A3,A4,A5,Th37;
then
A8: a1+b1 a.e.= a+b,M by Th31;
a1+b1 in L1_Functions M by A7,Th23;
hence z = a.e-eq-class(a1+b1,M) by A6,A8,Th39;
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,REAL;
assume a in A & b in B;
hence thesis by A9;
end;
uniqueness
proof
set C = CosetSet M;
let f1,f2 be BinOp of CosetSet M such that
A10: for A,B be Element of CosetSet M, a,b be PartFunc of X,REAL st a
in A & b in B holds f1.(A,B) = a.e-eq-class(a+b,M) and
A11: for A,B be Element of CosetSet M, a,b be PartFunc of X,REAL st a
in A & b in B holds f2.(A,B) = a.e-eq-class(a+b,M);
now
let A,B be Element of CosetSet M;
A in C;
then consider a1 be PartFunc of X,REAL such that
A12: A=a.e-eq-class(a1,M) & a1 in L1_Functions M;
B in C;
then consider b1 be PartFunc of X,REAL such that
A13: B=a.e-eq-class(b1,M) & b1 in L1_Functions M;
A14: b1 in B by A13,Th38;
A15: a1 in A by A12,Th38;
then f1.(A,B) = a.e-eq-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 zeroCoset M -> Element of CosetSet M means
:Def16:
ex f be PartFunc of
X,REAL st f = X --> 0 & f in L1_Functions M & it = a.e-eq-class(f,M);
correctness
proof
X-->0 in L1_Functions M by Lm3;
then a.e-eq-class(X-->0,M) in CosetSet M;
hence thesis by Lm3;
end;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func lmultCoset M -> Function of [:REAL, CosetSet M:],CosetSet M means
:
Def17: for
z be Real, A be Element of CosetSet M, f be PartFunc of X
,REAL st f in A holds it.(z,A) = a.e-eq-class(z(#)f,M);
existence
proof
defpred P[Real,set,set] means for f be PartFunc of X,REAL st f
in $2 holds $3 = a.e-eq-class($1(#)f,M);
set C = CosetSet M;
A1: now
let z be Element of REAL, A be Element of C;
A in C;
then consider a be PartFunc of X,REAL such that
A2: A = a.e-eq-class(a,M) and
A3: a in L1_Functions M;
set c = a.e-eq-class(z(#)a,M);
A4: z(#)a in L1_Functions M by A3,Th24;
then c in C;
then reconsider c as Element of C;
take c;
now
let a1 be PartFunc of X,REAL;
assume
A5: a1 in A;
then a1 a.e.= a,M by A2,A3,Th37;
then
A6: z(#)a1 a.e.= z(#)a,M by Th32;
z(#)a1 in L1_Functions M by A5,Th24;
hence c = a.e-eq-class(z(#)a1,M) by A4,A6,Th39;
end;
hence P[z,A,c];
end;
consider f be Function of [:REAL,C:],C such that
A7: for z be Element of REAL, A be Element of C holds P[z,A, f.(z,A)]
from BINOP_1:sch 3(A1);
A8: for z be Real, A be Element of C holds P[z,A, f.(z,A)]
proof let z be Real, A be Element of C;
reconsider z as Element of REAL by XREAL_0:def 1;
P[z,A, f.(z,A)] by A7;
hence thesis;
end;
take f;
let z be Real, A be Element of C, a be PartFunc of X,REAL;
assume a in A;
hence thesis by A8;
end;
uniqueness
proof
set C = CosetSet M;
let f1,f2 be Function of [:REAL,C:],C such that
A9: for z be Real, A be Element of CosetSet M, a be
PartFunc of X,REAL st a in A holds f1.(z,A) = a.e-eq-class(z(#)a,M) and
A10: for z be Real, A be Element of CosetSet M, a be
PartFunc of X,REAL st a in A holds f2.(z,A) = a.e-eq-class(z(#)a,M);
now
let z be Element of REAL, A be Element of CosetSet M;
A in C;
then consider a1 be PartFunc of X,REAL such that
A11: A=a.e-eq-class(a1,M) & a1 in L1_Functions M;
thus f1.(z,A) = a.e-eq-class(z(#)a1,M) by A9,A11,Th38
.= f2.(z,A) by A10,A11,Th38;
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-Space M -> strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty RLSStruct means
:Def18:
the carrier of it = CosetSet M & the addF of it = addCoset M & 0.it = zeroCoset
M & the Mult of it = lmultCoset M;
existence
proof
set C = CosetSet M, aC = addCoset M, zC = zeroCoset M, lC = lmultCoset M,
A = RLSStruct (# 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,REAL such that
A2: A1 = a.e-eq-class(a,M) & a in L1_Functions M;
A2 in C;
then consider b be PartFunc of X,REAL such that
A3: A2 = a.e-eq-class(b,M) & b in L1_Functions M;
A4: b in A2 by A3,Th38;
A5: a in A1 by A2,Th38;
then A1+A2 = a.e-eq-class(a+b,M) by A4,Def15;
hence thesis by A5,A4,Def15;
end;
A6: A is right_zeroed
proof
consider z be PartFunc of X,REAL such that
A7: z = X --> 0 and
A8: z in L1_Functions M and
A9: zeroCoset M=a.e-eq-class(z,M) by Def16;
A10: z in 0.A by A8,A9,Th38;
let A1 be Element of A;
A1 in C;
then consider a be PartFunc of X,REAL such that
A11: A1=a.e-eq-class(a,M) and
A12: a in L1_Functions M;
reconsider a1=a,z1=z as VECTOR of RLSp_L1Funct M by A12,A8;
A13: a+z =a1+z1 by Th25
.=a1+0.RLSp_L1Funct M by A7
.=a by RLVECT_1:def 4;
a in A1 by A11,A12,Th38;
hence thesis by A11,A10,A13,Def15;
end;
A14: now
let x,y be Real, A1,A2 be Element of A;
reconsider x1=x, y1=y as Real;
A1 in C;
then consider a be PartFunc of X,REAL such that
A15: A1=a.e-eq-class(a,M) and
A16: a in L1_Functions M;
A17: a in A1 by A15,A16,Th38;
then lC.(x1,A1) =a.e-eq-class(x(#)a,M) by Def17;
then
A18: x(#)a in x*A1 by A16,Th24,Th38;
A2 in C;
then consider b be PartFunc of X,REAL such that
A19: A2=a.e-eq-class(b,M) and
A20: b in L1_Functions M;
reconsider a1=a,b1=b as VECTOR of RLSp_L1Funct M by A16,A20;
A21: x(#)a = x1*a1 by Th26;
A22: b in A2 by A19,A20,Th38;
then lC.(x1,A2) =a.e-eq-class(x(#)b,M) by Def17;
then
A23: x(#)b in x1*A2 by A20,Th24,Th38;
a+b = a1+b1 by Th25;
then x(#)(a+b) = x1*(a1+b1) by Th26;
then
A24: x(#)(a+b) = x*a1+x*b1 by RLVECT_1:def 5;
x(#)b = x1*b1 by Th26;
then
A25: x(#)(a+b) = x(#)a + x(#)b by A21,A24,Th25;
aC.(A1,A2) =a.e-eq-class(a+b,M) by A17,A22,Def15;
then a+b in (A1+A2) by A16,A20,Th23,Th38;
then x1*(A1+A2) = a.e-eq-class(x(#)a+x(#)b,M) by A25,Def17;
hence x*(A1+A2) = x*A1+x*A2 by A18,A23,Def15;
A26: y(#)a = y1*a1 by Th26;
lC.(y1,A1) =a.e-eq-class(y(#)a,M) by A17,Def17;
then
A27: y(#)a in y1*A1 by A16,Th24,Th38;
(x+y)(#)a = (x1+y1)*a1 by Th26
.= x*a1+y*a1 by RLVECT_1:def 6
.= x(#)a + y(#)a by A26,A21,Th25;
then (x1+y1)*A1 = a.e-eq-class(x(#)a+y(#)a,M) by A17,Def17;
hence (x+y)*A1 = x*A1+y*A1 by A18,A27,Def15;
x(#)(y(#)a) =x*(y*a1) by A26,Th26
.= (x1*y1)*a1 by RLVECT_1:def 7
.= (x*y)(#)a by Th26;
then (x1*y1)*A1 = a.e-eq-class(x1(#)(y1(#)a),M) by A17,Def17
.=x*(y*A1) by A27,Def17;
hence (x*y)*A1=x*(y*A1);
1(#)a =1*a1 by Th26
.= a by RLVECT_1:def 8;
hence 1*A1 = A1 by A15,A17,Def17;
end;
A28: A is right_complementable
proof
let A1 be Element of A;
A1 in C;
then consider a be PartFunc of X,REAL such that
A29: A1=a.e-eq-class(a,M) and
A30: a in L1_Functions M;
set A2 = a.e-eq-class((-1)(#)a,M);
A31: (-1)(#)a in L1_Functions M by A30,Th24;
then A2 in C;
then reconsider A2 as Element of A;
A32: a in A1 & (-1)(#)a in A2 by A29,A30,Th24,Th38;
reconsider a1=a as VECTOR of RLSp_L1Funct M by A30;
take A2;
consider v,g be PartFunc of X,REAL such that
v in L1_Functions M and
g in L1_Functions M and
A33: v = a1+(-1)*a1 and
A34: g = X --> 0 and
A35: v a.e.= g,M by Th27;
A36: ex z be PartFunc of X,REAL st z = X --> 0 & z in L1_Functions M &
zeroCoset M=a.e-eq-class(z,M) by Def16;
A37: a+(-1)(#)a in L1_Functions M by A30,A31,Th23;
(-1)(#)a = (-1)*a1 by Th26;
then a+(-1)(#)a a.e.= g,M by A33,A35,Th25;
then 0.A = a.e-eq-class(a+ (-1)(#)a,M) by A34,A37,A36,Th39;
hence thesis by A32,Def15;
end;
A is add-associative
proof
let A1,A2,A3 be Element of A;
A1 in C;
then consider a be PartFunc of X,REAL such that
A38: A1=a.e-eq-class(a,M) and
A39: a in L1_Functions M;
A2 in C;
then consider b be PartFunc of X,REAL such that
A40: A2=a.e-eq-class(b,M) and
A41: b in L1_Functions M;
A3 in C;
then consider c be PartFunc of X,REAL such that
A42: A3=a.e-eq-class(c,M) and
A43: c in L1_Functions M;
A44: c in A3 by A42,A43,Th38;
A45: b in A2 by A40,A41,Th38;
then aC.(A2,A3) =a.e-eq-class(b+c,M) by A44,Def15;
then
A46: b+c in A2+A3 by A41,A43,Th23,Th38;
reconsider a1=a,b1=b,c1=c as VECTOR of RLSp_L1Funct M by A39,A41,A43;
b+c = b1+c1 by Th25;
then a+(b+c) =a1+(b1+c1) by Th25;
then
A47: a+(b+c) =(a1+b1)+c1 by RLVECT_1:def 3;
a+b = a1+b1 by Th25;
then
A48: a+(b+c) = a+b+c by A47,Th25;
A49: a in A1 by A38,A39,Th38;
then aC.(A1,A2) =a.e-eq-class(a+b,M) by A45,Def15;
then a+b in A1+A2 by A39,A41,Th23,Th38;
then A1+A2+A3 = a.e-eq-class(a+(b+c),M) by A44,A48,Def15;
hence thesis by A49,A46,Def15;
end;
then reconsider A as strict Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital non empty RLSStruct by A1,A6,A28,A14,
RLVECT_1:def 5,def 6,def 7,def 8;
take A;
thus thesis;
end;
uniqueness;
end;
begin :: Real Normed Space of Integrable Functions
theorem Th43:
f in L1_Functions M & g in L1_Functions M & f a.e.= g,M implies
Integral(M,f) = Integral(M,g)
proof
assume that
A1: f in L1_Functions M and
A2: g in L1_Functions M and
A3: f a.e.= 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,REAL 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;
R_EAL f is_integrable_on M by A6;
then consider E1 being Element of S such that
A10: E1 = dom R_EAL f and
A11: R_EAL f is E1-measurable;
A12: f is E1-measurable by A11;
A13: ex g1 be PartFunc of X,REAL 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
A14: M.NDg=0 and
A15: dom g = NDg` and
g is_integrable_on M;
A16: M.(EQ \/ NDg) = 0 by A14,A4,Lm4;
R_EAL g is_integrable_on M by A13;
then consider E2 being Element of S such that
A17: E2 = dom R_EAL g and
A18: R_EAL g is E2-measurable;
A19: g is E2-measurable by A18;
A20: EQ` \ (NDf \/NDg) = (EQ \/ (NDf \/NDg))` by XBOOLE_1:41
.=(NDg \/ (EQ \/NDf))` by XBOOLE_1:4
.=NDg` \ (EQ \/NDf) by XBOOLE_1:41;
A21: EQ` \ (NDf \/NDg) = (EQ \/ (NDf \/NDg))` by XBOOLE_1:41
.= (NDf \/ (EQ \/NDg))` by XBOOLE_1:4
.= NDf` \ (EQ \/NDg) by XBOOLE_1:41;
A22: 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 A22,FUNCT_1:51;
hence Integral(M,f) = Integral(M,g|(NDg` \(EQ\/NDf))) by A8,A10,A12,A21,A20
,A16,MESFUNC6:89
.= Integral(M,g) by A15,A17,A19,A9,MESFUNC6:89;
end;
theorem Th44:
f is_integrable_on M implies Integral(M,f) in REAL & Integral(M,
abs f) in REAL & abs f is_integrable_on M
proof
assume
A1: f is_integrable_on M;
then
A2: -infty < Integral(M,f) & Integral(M,f) < +infty by MESFUNC6:90;
R_EAL f is_integrable_on M by A1;
then consider A be Element of S such that
A3: A = dom R_EAL f and
A4: R_EAL f is A-measurable;
A5: f is A-measurable by A4;
then abs f is_integrable_on M by A1,A3,MESFUNC6:94;
then -infty < Integral(M,abs f) & Integral(M,abs f) < +infty by MESFUNC6:90;
hence thesis by A1,A2,A3,A5,MESFUNC6:94,XXREAL_0:14;
end;
theorem Th45:
f in L1_Functions M & g in L1_Functions M & f a.e.= g,M implies
abs f a.e.= (abs g),M & Integral(M,abs f) = Integral(M,abs g)
proof
assume that
A1: f in L1_Functions M and
A2: g in L1_Functions M and
A3: f a.e.= g,M;
A4: ex f1 be PartFunc of X,REAL 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: abs f is_integrable_on M by A4,Th44;
consider EQ being Element of S such that
A8: M.EQ = 0 and
A9: f|EQ` = g|EQ` by A3;
(abs f)|EQ` = abs(g|EQ`) by A9,RFUNCT_1:46
.= (abs g)|EQ` by RFUNCT_1:46;
then
A10: abs f a.e.= (abs g),M by A8;
A11: ex g1 be PartFunc of X,REAL 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: abs g is_integrable_on M by A11,Th44;
dom abs g = NDg` by A13,VALUED_1:def 11;
then
A15: abs g in L1_Functions M by A12,A14;
dom abs f = NDf` by A6,VALUED_1:def 11;
then abs f in L1_Functions M by A5,A7;
hence thesis by A15,A10,Th43;
end;
theorem Th46:
(ex x be VECTOR of Pre-L-Space M st f in x & g in x) implies f
a.e.= g,M & f in L1_Functions M & g in L1_Functions M
proof
assume ex x be VECTOR of Pre-L-Space M st f in x & g in x;
then consider x be VECTOR of Pre-L-Space M such that
A1: f in x and
A2: g in x;
x in the carrier of Pre-L-Space M;
then x in CosetSet M by Def18;
then consider h be PartFunc of X,REAL such that
A3: x=a.e-eq-class(h,M) and
h in L1_Functions M;
ex k be PartFunc of X,REAL st f=k & k in L1_Functions M & h in
L1_Functions M & h a.e.= k,M by A1,A3;
then
A4: f a.e.= h,M;
ex j be PartFunc of X,REAL st g=j & j in L1_Functions M & h in
L1_Functions M & h a.e.= j,M by A2,A3;
hence thesis by A1,A3,A4,Th30;
end;
reserve x for Point of Pre-L-Space M;
theorem Th47:
f in x implies f is_integrable_on M & f in L1_Functions M & abs
f is_integrable_on M
proof
x in the carrier of Pre-L-Space M;
then x in CosetSet M by Def18;
then consider h be PartFunc of X,REAL such that
A1: x=a.e-eq-class(h,M) and
h in L1_Functions M;
assume f in x;
then ex g be PartFunc of X,REAL st f=g & g in L1_Functions M & h in
L1_Functions M & h a.e.= g,M by A1;
then
ex f0 be PartFunc of X,REAL st f=f0 & ex ND be Element of S st M.ND=0 &
dom f0 = ND` & f0 is_integrable_on M;
hence thesis by Th44;
end;
theorem Th48:
f in x & g in x implies f a.e.= 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_Functions M by A2,Th46;
f a.e.= g,M & f in L1_Functions M by A1,A2,Th46;
hence thesis by A3,Th43,Th45;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func L-1-Norm M -> Function of the carrier of Pre-L-Space M,REAL means
:
Def19: for x be Point of Pre-L-Space M ex f be PartFunc of X,REAL st f in x &
it.x = Integral(M,abs f);
existence
proof
defpred P[set,set] means ex f be PartFunc of X,REAL st f in $1 & $2 =
Integral(M,abs f);
A1: for x be Point of Pre-L-Space M ex y being Element of REAL st P[x,y]
proof
let x be Point of Pre-L-Space M;
x in the carrier of Pre-L-Space M;
then x in CosetSet M by Def18;
then consider f be PartFunc of X,REAL such that
A2: x=a.e-eq-class(f,M) and
A3: f in L1_Functions M;
ex f0 be PartFunc of X,REAL 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 Th44;
hence thesis by A2,A3,Th38;
end;
consider f being Function of Pre-L-Space M,REAL such that
A4: for x being Point of Pre-L-Space M holds P[x,f.x] from FUNCT_2:sch 3
(A1 );
take f;
thus thesis by A4;
end;
uniqueness
proof
let N1,N2 be Function of the carrier of Pre-L-Space M,REAL;
assume
A5: ( for x be Point of Pre-L-Space M ex f be PartFunc of X,REAL st f
in x & N1.x = Integral(M,abs f))& for x be Point of Pre-L-Space M ex g be
PartFunc of X,REAL st g in x & N2.x = Integral(M,abs g);
now
let x be Point of Pre-L-Space M;
( ex f be PartFunc of X,REAL st f in x & N1.x = Integral(M,abs f))&
ex g be PartFunc of X,REAL st g in x & N2.x = Integral(M,abs g) by A5;
hence N1.x=N2.x by Th48;
end;
hence N1=N2 by FUNCT_2:63;
end;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
func L-1-Space M -> non empty NORMSTR equals
NORMSTR (# the carrier of
Pre-L-Space M, the ZeroF of Pre-L-Space M, the addF of Pre-L-Space M, the Mult
of Pre-L-Space M, L-1-Norm M #);
coherence;
end;
reserve x,y for Point of L-1-Space M;
theorem Th49:
( ex f be PartFunc of X,REAL st f in L1_Functions M & x=
a.e-eq-class(f,M) & ||.x.|| = Integral(M,abs f) ) & for f be PartFunc of X,REAL
st f in x holds Integral(M,abs f) = ||.x.||
proof
reconsider y=x as Point of Pre-L-Space M;
consider f be PartFunc of X,REAL such that
A1: f in y and
A2: (L-1-Norm M).y = Integral(M,abs f) by Def19;
y in the carrier of Pre-L-Space M;
then y in CosetSet M by Def18;
then consider g be PartFunc of X,REAL such that
A3: y=a.e-eq-class(g,M) & g in L1_Functions M;
g in y by A3,Th38;
then f a.e.= g,M by A1,Th46;
then x = a.e-eq-class(f,M) by A1,A3,Th39;
hence thesis by A1,A2,Th48;
end;
theorem Th50:
f in x implies x= a.e-eq-class(f,M) & ||.x.|| = Integral(M,abs f )
proof
assume
A1: f in x;
reconsider y=x as Point of Pre-L-Space M;
y in the carrier of Pre-L-Space M;
then y in CosetSet M by Def18;
then consider g be PartFunc of X,REAL such that
A2: y=a.e-eq-class(g,M) & g in L1_Functions M;
g in y by A2,Th38;
then f a.e.= g,M by A1,Th46;
hence thesis by A1,A2,Th39,Th49;
end;
theorem Th51:
(f in x & g in y implies f+g in x+y) & (f in x implies a(#)f in a*x)
proof
set C = CosetSet M;
hereby
reconsider x1=x,y1=y as Point of Pre-L-Space M;
assume that
A1: f in x and
A2: g in y;
y1 in the carrier of Pre-L-Space M;
then
A3: y1 in C by Def18;
then consider b be PartFunc of X,REAL such that
A4: y1=a.e-eq-class(b,M) and
A5: b in L1_Functions M;
A6: b in y1 by A4,A5,Th38;
ex r be PartFunc of X,REAL st g=r & r in L1_Functions M & b in
L1_Functions M & b a.e.= r,M by A2,A4;
then
A7: a.e-eq-class(b,M) = a.e-eq-class(g,M) by Th39;
x1 in the carrier of Pre-L-Space M;
then
A8: x1 in C by Def18;
then consider a be PartFunc of X,REAL such that
A9: x1=a.e-eq-class(a,M) and
A10: a in L1_Functions M;
a in x1 by A9,A10,Th38;
then (addCoset M).(x1,y1) = a.e-eq-class(a+b,M) by A8,A3,A6,Def15;
then
A11: x1+y1 = a.e-eq-class(a+b,M) by Def18;
ex r be PartFunc of X,REAL st f=r & r in L1_Functions M & a in
L1_Functions M & a a.e.= r,M by A1,A9;
then a.e-eq-class(a,M) = a.e-eq-class(f,M) by Th39;
then
a.e-eq-class(a+b,M) = a.e-eq-class(f+g,M) by A1,A2,A9,A10,A4,A5,A7,Th41;
hence f+g in x+y by A1,A2,A9,A4,A11,Th23,Th38;
end;
hereby
reconsider x1=x as Point of Pre-L-Space M;
x1 in the carrier of Pre-L-Space M;
then
A12: x1 in C by Def18;
then consider f1 be PartFunc of X,REAL such that
A13: x1=a.e-eq-class(f1,M) and
A14: f1 in L1_Functions M;
f1 in x1 by A13,A14,Th38;
then (lmultCoset M).(a,x1) = a.e-eq-class(a(#)f1,M) by A12,Def17;
then
A15: a*x1 = a.e-eq-class(a(#)f1,M) by Def18;
assume
A16: f in x;
then ex r be PartFunc of X,REAL st f=r & r in L1_Functions M & f1 in
L1_Functions M & f1 a.e.= r,M by A13;
then a.e-eq-class(f1,M) = a.e-eq-class(f,M) by Th39;
then a.e-eq-class(a(#)f1,M) = a.e-eq-class(a(#)f,M) by A16,A13,A14,Th42;
hence a(#)f in a*x by A16,A13,A15,Th24,Th38;
end;
end;
theorem Th52:
E = dom f & (for x be set st x in dom f holds f.x=r) implies f
is E-measurable
proof
assume
A1: E = dom f;
r in REAL by XREAL_0:def 1;
then reconsider r0=r as R_eal by NUMBERS:31;
set g=R_EAL f;
consider g0 be PartFunc of X,ExtREAL such that
A2: g0 is_simple_func_in S and
A3: dom g0 = E and
A4: for x be object st x in E holds g0.x=r0 by MESFUNC5:41;
assume
A5: for x be set st x in dom f holds f.x=r;
now
let x be Element of X;
assume
A6: x in dom g;
then g.x = r by A5;
hence g.x = g0.x by A1,A4,A6;
end;
then g0=g by A1,A3,PARTFUN1:5;
then g is E-measurable by A2,MESFUNC2:34;
hence thesis;
end;
theorem Th53:
f in L1_Functions M & Integral(M,abs f) = 0 implies f a.e.= X--> 0,M
proof
assume that
A1: f in L1_Functions M and
A2: Integral(M,abs f) = 0;
set g = X-->0;
defpred P[Element of NAT,set] means $2=great_eq_dom(abs f,1/($1+1)) & M.($2)
=0;
consider f1 be PartFunc of X,REAL such that
A3: f=f1 and
A4: ex ND be Element of S st M.ND=0 & dom f1 = ND` & f1 is_integrable_on
M by A1;
A5: abs f is_integrable_on M by A3,A4,Th44;
then R_EAL abs f is_integrable_on M;
then consider E be Element of S such that
A6: E = dom R_EAL abs f and
A7: R_EAL abs f is E-measurable;
A8: abs f is E-measurable by A7;
now
let x be object;
assume x in dom abs f;
then (abs f).x = |.f.x qua Complex.| by VALUED_1:def 11;
hence 0 <= (abs f).x by COMPLEX1:46;
end;
then
A9: abs f is nonnegative by MESFUNC6:52;
A10: now
let n be Element of NAT;
reconsider r=1/(n+1) as Element of REAL by XREAL_0:def 1;
reconsider Br=E /\ great_eq_dom(abs f,r) as Element of S by A6,A8,
MESFUNC6:13;
set g = Br --> r;
A11: dom g = Br by FUNCT_2:def 1;
A12: for x be set st x in dom g holds g.x = r by FUNCOP_1:7;
reconsider g as PartFunc of X,REAL by RELSET_1:7;
A13: (abs f)|Br is_integrable_on M by A5,MESFUNC6:91;
for x be object st x in dom g holds 0 <= g.x by A12;
then g is nonnegative by MESFUNC6:52;
then
A14: 0 <= Integral(M,g) by A11,A12,Th52,MESFUNC6:84;
A15: dom abs g =dom g by VALUED_1:def 11;
A16: now
let x be Element of X;
assume
A17: x in dom abs g;
then (abs g).x = |.g.x qua Complex.| by VALUED_1:def 11;
then (abs g).x = |.r qua Complex.| by A12,A15,A17;
then (abs g).x = r by ABSVALUE:def 1;
hence (abs g).x = g.x by A12,A15,A17;
end;
A18: dom ((abs f)|Br) = dom (abs f) /\ Br by RELAT_1:61
.= Br by A6,XBOOLE_1:17,28;
then
A19: dom g = dom ((abs f)|Br) by FUNCT_2:def 1;
A20: now
let x be Element of X;
assume
A21: x in dom g;
then x in E /\ great_eq_dom(abs f,r) by FUNCT_2:def 1;
then x in great_eq_dom(abs f,r) by XBOOLE_0:def 4;
then
A22: ex y being Real st y=(abs f).x & r <= y by MESFUNC6:6;
|.g.x qua Complex.| = |.r qua Complex.| by A12,A21;
then |.g.x qua Complex.| = r by ABSVALUE:def 1;
hence |.g.x qua Complex.| <= ((abs f)|Br).x by A19,A21,A22,FUNCT_1:47;
end;
g is Br-measurable by A11,A12,Th52;
then Integral(M,abs g) <= Integral(M,(abs f)|Br) by A11,A18,A13,A20,
MESFUNC6:96;
then
A23: Integral(M, g) <= Integral(M,(abs f)|Br) by A15,A16,PARTFUN1:5;
A24: for x be object st x in dom g holds g.x = r by A11,FUNCOP_1:7;
reconsider rr=r as R_eal by XXREAL_0:def 1;
AAA: 1/(n+1) = 1 qua ExtReal/(n+1);
Integral(M,(abs f)|Br) <= Integral(M,(abs f)|E)
by A6,A8,A9,MESFUNC6:87,XBOOLE_1:17;
then Integral(M,g) = 0 by A2,A6,A23,A14,RELAT_1:68;
then rr * M.Br = 0 by A11,A24,MESFUNC6:97;
then
A25: M.Br = 0 by AAA;
for x be object st x in great_eq_dom(abs f,r) holds x in dom abs f
by MESFUNC6:6;
then great_eq_dom(abs f,r) c= E by A6;
hence ex B be Element of S st P[n,B] by A25,XBOOLE_1:28;
end;
consider F be sequence of S such that
A26: for n be Element of NAT holds P[n,F.n] from FUNCT_2:sch 3(A10);
now
let y be object;
assume y in union rng F;
then consider B be set such that
A27: y in B and
A28: B in rng F by TARSKI:def 4;
consider n be object such that
A29: n in NAT and
A30: B=F.n by A28,FUNCT_2:11;
reconsider m=n as Element of NAT by A29;
A31: y in great_eq_dom(abs f,1/(m+1)) by A26,A27,A30;
then
A32: y in dom abs f by MESFUNC6:6;
then
A33: y in dom f by VALUED_1:def 11;
A34: (abs f).y = |.f.y qua Complex.| by A32,VALUED_1:def 11;
AAA: 1/(m+1) = 1 qua ExtReal/(m+1);
1/(m+1) <= (abs f).y by A31,MESFUNC1:def 14;
then (abs f).y <> 0 by AAA;
then f.y <> 0 by A34,ABSVALUE:2;
hence y in {x where x is Element of X : x in dom f & f.x <> 0} by A33;
end;
then
A35: union rng F c= {x where x is Element of X : x in dom f & f.x <> 0};
consider ND be Element of S such that
A36: M.ND=0 and
A37: dom f1 = ND` and
f1 is_integrable_on M by A4;
reconsider EQ = union rng F \/ ND as Element of S;
A38: EQ` = ND` /\ (union rng F)` by XBOOLE_1:53;
then
A39: EQ` c= dom f by A3,A37,XBOOLE_1:17;
dom g = X by FUNCOP_1:13;
then
A40: dom(g|EQ`) = EQ` by RELAT_1:62;
A41: dom(f|EQ`) = EQ` by A3,A37,A38,RELAT_1:62,XBOOLE_1:17;
now
let y be object;
assume y in {x where x is Element of X : x in dom f & f.x <> 0};
then consider z be Element of X such that
A42: y=z and
A43: z in dom f and
A44: f.z <> 0;
A45: z in dom abs f by A43,VALUED_1:def 11;
then (abs f).z = |.f.z qua Complex.| by VALUED_1:def 11;
then 0 < (abs f).z by A44,COMPLEX1:47;
then consider n be Element of NAT such that
A46: 1/(n+1) < (abs f).z - 0 by MESFUNC1:10;
z in great_eq_dom(abs f,1/(n+1)) by A45,A46,MESFUNC6:6;
then
A47: y in F.n by A26,A42;
F.n in rng F by FUNCT_2:4;
hence y in union rng F by A47,TARSKI:def 4;
end;
then {x where x is Element of X : x in dom f & f.x <> 0} c= union rng F;
then
A48: {x where x is Element of X : x in dom f & f.x <> 0 } = union rng F by A35,
XBOOLE_0:def 10;
A49: now
let x be set;
assume
A50: x in EQ`;
then x in (union rng F)` by A38,XBOOLE_0:def 4;
then not x in union rng F by XBOOLE_0:def 5;
hence f.x = 0 by A48,A39,A50;
end;
now
let y be object;
assume
A51: y in dom(f|EQ`);
then (f|EQ`).y = f.y by FUNCT_1:47;
then (f|EQ`).y =0 by A41,A49,A51;
then (f|EQ`).y =g.y by A51,FUNCOP_1:7;
hence (f|EQ`).y =(g|EQ`).y by A41,A40,A51,FUNCT_1:47;
end;
then
A52: f|EQ` = g|EQ` by A39,A40,FUNCT_1:2,RELAT_1:62;
now
let A be set;
assume A in rng F;
then consider n be object such that
A53: n in NAT and
A54: A=F.n by FUNCT_2:11;
reconsider n as Element of NAT by A53;
M.(F.n) =0 by A26;
hence A is measure_zero of M by A54,MEASURE1:def 7;
end;
then
A55: union rng F is measure_zero of M by MEASURE2:14;
ND is measure_zero of M by A36,MEASURE1:def 7;
then EQ is measure_zero of M by A55,MEASURE1:37;
then M.EQ=0 by MEASURE1:def 7;
hence thesis by A52;
end;
theorem Th54:
Integral(M,abs(X-->0)) = 0
proof
set f=X --> 0;
A1: now
let x be Element of X;
f.x = 0 by FUNCOP_1:7;
then
A2: |.f.x qua Complex.| = 0 by ABSVALUE:2;
assume x in dom abs f;
hence (abs f).x = 0 by A2,VALUED_1:def 11;
end;
dom f = X by FUNCOP_1:13;
then dom abs f = X by VALUED_1:def 11;
hence thesis by A1,Lm2;
end;
theorem Th55:
f is_integrable_on M & g is_integrable_on M implies Integral(M,
abs(f+g)) <= Integral(M,abs f) + Integral(M,abs g)
proof
set f1=R_EAL f;
set g1=R_EAL g;
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
A3: f1 is_integrable_on M by A1;
then consider B be Element of S such that
A4: B = dom f1 and
f1 is B-measurable;
A5: B= dom |.f1.| by A4,MESFUNC1:def 10;
|.f1.| is_integrable_on M by A3,MESFUNC5:100;
then
A6: ex E be Element of S st E = dom |.f1.| & |.f1.| is E-measurable;
A7: g1 is_integrable_on M by A2;
then consider C be Element of S such that
A8: C = dom g1 and
g1 is C-measurable;
A9: C= dom |.g1.| by A8,MESFUNC1:def 10;
consider E be Element of S such that
A10: E = dom(f1+g1) and
A11: Integral(M,(|.f1+g1.|)|E) <= Integral(M,(|.f1.|)|E) + Integral(M,(|.
g1.|)|E) by A3,A7,MESFUNC7:22;
dom |.f1+g1.| = E by A10,MESFUNC1:def 10;
then f1+g1 =R_EAL(f+g) & (|.f1+g1.|)|E = |.f1+g1.| by MESFUNC6:23,RELAT_1:68;
then
A12: Integral(M,(|.f1+g1.|)|E) = Integral(M,|.f+g.|) by MESFUNC6:1;
|.g1.| is_integrable_on M by A7,MESFUNC5:100;
then
A13: ex E be Element of S st E = dom |.g1.| & |.g1.| is E-measurable;
A14: E= (dom f1 /\ dom g1)\((f1"{-infty} /\ g1"{+infty}) \/ (f1"{+infty} /\
g1"{-infty})) by A10,MESFUNC1:def 3;
then E c= dom g1 by XBOOLE_1:18,36;
then E c= dom |.g1.| by MESFUNC1:def 10;
then Integral(M,(|.g1.|)|E) <= Integral(M,(|.g1.|)|C) by A9,A13,MESFUNC5:93;
then Integral(M,(|.g1.|)|E) <= Integral(M,|.g1.|) by A9,RELAT_1:68;
then
A15: Integral(M,(|.g1.|)|E) <= Integral(M,|.g.|) by MESFUNC6:1;
E c= dom f1 by A14,XBOOLE_1:18,36;
then E c= dom |.f1.| by MESFUNC1:def 10;
then Integral(M,(|.f1.|)|E) <= Integral(M,(|.f1.|)|B) by A5,A6,MESFUNC5:93;
then Integral(M,(|.f1.|)|E) <= Integral(M,|.f1.|) by A5,RELAT_1:68;
then Integral(M,(|.f1.|)|E) <= Integral(M,|.f.|) by MESFUNC6:1;
then Integral(M,(|.f1.|)|E) + Integral(M,(|.g1.|)|E) <= Integral(M,|.f.|) +
Integral(M,|.g.|) by A15,XXREAL_3:36;
hence thesis by A11,A12,XXREAL_0:2;
end;
Lm7: L-1-Space M is RealNormSpace-like vector-distributive scalar-distributive
scalar-associative scalar-unital Abelian
add-associative right_zeroed right_complementable
proof
now
let x,y be Point of L-1-Space M, a be Real;
consider f be PartFunc of X,REAL such that
A1: f in x and
A2: ||.x.|| = Integral(M,abs f) by Def19;
abs f is_integrable_on M by A1,Th47;
then Integral(M,|.a qua Complex.|(#)abs f)
=|.a qua Complex.| * Integral(M,abs f) by
MESFUNC6:102;
then Integral(M,abs(a(#)f)) = |.a qua Complex.| * Integral(M,abs f) by
RFUNCT_1:25;
then
A3: Integral(M,abs(a(#)f)) = |.a qua Complex.| * ||.x.|| by A2,EXTREAL1:1;
hereby
set g = X-->0;
reconsider x1 =x as Point of Pre-L-Space M;
consider f be PartFunc of X, REAL such that
A4: f in x1 and
(L-1-Norm M).x1 = Integral(M,abs f) by Def19;
A5: f in L1_Functions M by A4,Th47;
then
A6: a.e-eq-class(f,M) in CosetSet M;
A7: g in L1_Functions M by Lm3;
assume ||.x.|| = 0;
then Integral(M,abs f) = 0 by A4,Th49;
then f a.e.= g,M by A5,Th53;
then a.e-eq-class(g,M) = a.e-eq-class(f,M) by A5,A7,Th39;
then zeroCoset M = a.e-eq-class(f,M) by A7,A6,Def16;
then 0.(Pre-L-Space M) = a.e-eq-class(f,M) by Def18;
hence x =0.(L-1-Space M) by A4,Th50;
end;
hereby
reconsider x1 =x as Point of Pre-L-Space M;
consider f be PartFunc of X,REAL such that
A8: f = X-->0 and
A9: f in L1_Functions M & zeroCoset M = a.e-eq-class(f,M) by Def16;
assume x = 0.(L-1-Space M);
then x1 =0.(Pre-L-Space M);
then
A10: x1 = zeroCoset M by Def18;
(L-1-Norm M).x1 = ||.x.||;
then (L-1-Norm M).x1 = Integral(M,abs f) by A10,A9,Th38,Th49;
hence ||.x.||=0 by A8,Th54;
end;
A11: f is_integrable_on M by A1,Th47;
then |. Integral(M,f) .| <= Integral(M,abs f) by MESFUNC6:95;
hence 0 <= ||.x.|| by A2,EXTREAL1:14;
consider g be PartFunc of X,REAL such that
A12: g in y and
A13: ||.y.|| = Integral(M,abs g) by Def19;
A14: g is_integrable_on M by A12,Th47;
f+g in x+y by A1,A12,Th51;
then
A15: ||.x+y.|| = Integral(M,abs(f+g)) by Th49;
Integral(M,abs f) + Integral(M,abs g) = ||.x.|| + ||.y.|| by A2,A13,
SUPINF_2:1;
hence ||.x+y.|| <= ||.x.|| + ||.y.|| by A11,A15,A14,Th55;
a(#)f in a*x by A1,Th51;
hence ||.a*x.|| = |.a qua Complex.| * ||.x.|| by A3,Th49;
end;
hence thesis by NORMSP_1:def 1,RSSPACE3:2;
end;
registration
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
cluster L-1-Space M -> RealNormSpace-like vector-distributive
scalar-distributive scalar-associative scalar-unital Abelian
add-associative right_zeroed right_complementable;
coherence by Lm7;
end;