:: MESFUN6C semantic presentation
begin
theorem Th1: :: MESFUN6C:1
for a, b being real number holds
( (R_EAL a) + (R_EAL b) = a + b & - (R_EAL a) = - a & (R_EAL a) - (R_EAL b) = a - b & (R_EAL a) * (R_EAL b) = a * b )
proof
let a, b be real number ; ::_thesis: ( (R_EAL a) + (R_EAL b) = a + b & - (R_EAL a) = - a & (R_EAL a) - (R_EAL b) = a - b & (R_EAL a) * (R_EAL b) = a * b )
reconsider a9 = a, b9 = b as Real by XREAL_0:def_1;
A1: b9 = R_EAL b ;
A2: a9 = R_EAL a ;
hence (R_EAL a) + (R_EAL b) = a + b by A1, SUPINF_2:1; ::_thesis: ( - (R_EAL a) = - a & (R_EAL a) - (R_EAL b) = a - b & (R_EAL a) * (R_EAL b) = a * b )
- a9 = R_EAL (- a) ;
hence - (R_EAL a) = - a by SUPINF_2:2; ::_thesis: ( (R_EAL a) - (R_EAL b) = a - b & (R_EAL a) * (R_EAL b) = a * b )
thus (R_EAL a) - (R_EAL b) = a - b by A2, A1, SUPINF_2:3; ::_thesis: (R_EAL a) * (R_EAL b) = a * b
thus (R_EAL a) * (R_EAL b) = a * b by A2, A1, EXTREAL1:1; ::_thesis: verum
end;
begin
definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,COMPLEX;
let E be Element of S;
predf is_measurable_on E means :Def1: :: MESFUN6C:def 1
( Re f is_measurable_on E & Im f is_measurable_on E );
end;
:: deftheorem Def1 defines is_measurable_on MESFUN6C:def_1_:_
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for E being Element of S holds
( f is_measurable_on E iff ( Re f is_measurable_on E & Im f is_measurable_on E ) );
theorem Th2: :: MESFUN6C:2
for X being non empty set
for f being PartFunc of X,COMPLEX
for r being Real holds
( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX
for r being Real holds
( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) )
let f be PartFunc of X,COMPLEX; ::_thesis: for r being Real holds
( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) )
let r be Real; ::_thesis: ( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) )
A1: dom (r (#) (Re f)) = dom (Re f) by VALUED_1:def_5;
A2: Im r = 0 by COMPLEX1:def_2;
A3: dom (Re f) = dom f by COMSEQ_3:def_3;
A4: Re r = r by COMPLEX1:def_1;
A5: dom (r (#) f) = dom f by VALUED_1:def_5;
A6: dom (Re (r (#) f)) = dom (r (#) f) by COMSEQ_3:def_3;
now__::_thesis:_for_x_being_set_st_x_in_dom_(r_(#)_(Re_f))_holds_
(r_(#)_(Re_f))_._x_=_(Re_(r_(#)_f))_._x
let x be set ; ::_thesis: ( x in dom (r (#) (Re f)) implies (r (#) (Re f)) . x = (Re (r (#) f)) . x )
A7: Re (r * (f . x)) = ((Re r) * (Re (f . x))) - ((Im r) * (Im (f . x))) by COMPLEX1:9;
assume A8: x in dom (r (#) (Re f)) ; ::_thesis: (r (#) (Re f)) . x = (Re (r (#) f)) . x
then A9: (Re f) . x = Re (f . x) by A1, COMSEQ_3:def_3;
(Re (r (#) f)) . x = Re ((r (#) f) . x) by A1, A5, A6, A3, A8, COMSEQ_3:def_3;
then (Re (r (#) f)) . x = r * (Re (f . x)) by A1, A5, A3, A4, A2, A8, A7, VALUED_1:def_5;
hence (r (#) (Re f)) . x = (Re (r (#) f)) . x by A8, A9, VALUED_1:def_5; ::_thesis: verum
end;
hence r (#) (Re f) = Re (r (#) f) by A1, A5, A6, A3, FUNCT_1:2; ::_thesis: r (#) (Im f) = Im (r (#) f)
A10: dom (r (#) (Im f)) = dom (Im f) by VALUED_1:def_5;
A11: dom (Im f) = dom f by COMSEQ_3:def_4;
A12: dom (Im (r (#) f)) = dom (r (#) f) by COMSEQ_3:def_4;
now__::_thesis:_for_x_being_set_st_x_in_dom_(r_(#)_(Im_f))_holds_
(r_(#)_(Im_f))_._x_=_(Im_(r_(#)_f))_._x
let x be set ; ::_thesis: ( x in dom (r (#) (Im f)) implies (r (#) (Im f)) . x = (Im (r (#) f)) . x )
A13: Im (r * (f . x)) = ((Im r) * (Re (f . x))) + ((Re r) * (Im (f . x))) by COMPLEX1:9;
assume A14: x in dom (r (#) (Im f)) ; ::_thesis: (r (#) (Im f)) . x = (Im (r (#) f)) . x
then A15: (Im f) . x = Im (f . x) by A10, COMSEQ_3:def_4;
(Im (r (#) f)) . x = Im ((r (#) f) . x) by A10, A5, A12, A11, A14, COMSEQ_3:def_4;
then (Im (r (#) f)) . x = r * (Im (f . x)) by A10, A5, A11, A4, A2, A14, A13, VALUED_1:def_5;
hence (r (#) (Im f)) . x = (Im (r (#) f)) . x by A14, A15, VALUED_1:def_5; ::_thesis: verum
end;
hence r (#) (Im f) = Im (r (#) f) by A10, A5, A12, A11, FUNCT_1:2; ::_thesis: verum
end;
theorem Th3: :: MESFUN6C:3
for X being non empty set
for f being PartFunc of X,COMPLEX
for c being complex number holds
( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX
for c being complex number holds
( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) )
let f be PartFunc of X,COMPLEX; ::_thesis: for c being complex number holds
( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) )
let c be complex number ; ::_thesis: ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) )
A1: dom ((Re c) (#) (Re f)) = dom (Re f) by VALUED_1:def_5;
A2: dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def_5;
A3: dom (c (#) f) = dom f by VALUED_1:def_5;
A4: dom (Re (c (#) f)) = dom (c (#) f) by COMSEQ_3:def_3;
A5: dom (Re f) = dom f by COMSEQ_3:def_3;
A6: dom (Im f) = dom f by COMSEQ_3:def_4;
A7: dom (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) = (dom ((Re c) (#) (Re f))) /\ (dom ((Im c) (#) (Im f))) by VALUED_1:12;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Re_(c_(#)_f))_holds_
(Re_(c_(#)_f))_._x_=_(((Re_c)_(#)_(Re_f))_-_((Im_c)_(#)_(Im_f)))_._x
let x be set ; ::_thesis: ( x in dom (Re (c (#) f)) implies (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x )
A8: Re (c * (f . x)) = ((Re c) * (Re (f . x))) - ((Im c) * (Im (f . x))) by COMPLEX1:9;
assume A9: x in dom (Re (c (#) f)) ; ::_thesis: (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x
then A10: ((Im c) (#) (Im f)) . x = (Im c) * ((Im f) . x) by A4, A6, A2, A3, VALUED_1:def_5;
A11: (Im f) . x = Im (f . x) by A4, A6, A3, A9, COMSEQ_3:def_4;
A12: (Re f) . x = Re (f . x) by A4, A5, A3, A9, COMSEQ_3:def_3;
(Re (c (#) f)) . x = Re ((c (#) f) . x) by A9, COMSEQ_3:def_3;
then A13: (Re (c (#) f)) . x = Re (c * (f . x)) by A4, A9, VALUED_1:def_5;
((Re c) (#) (Re f)) . x = (Re c) * ((Re f) . x) by A4, A5, A1, A3, A9, VALUED_1:def_5;
hence (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x by A4, A5, A6, A1, A2, A3, A7, A9, A13, A10, A12, A11, A8, VALUED_1:13; ::_thesis: verum
end;
hence Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) by A4, A5, A6, A1, A2, A3, A7, FUNCT_1:2; ::_thesis: Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f))
A14: dom ((Im c) (#) (Re f)) = dom (Re f) by VALUED_1:def_5;
A15: dom ((Re c) (#) (Im f)) = dom (Im f) by VALUED_1:def_5;
A16: dom (Im (c (#) f)) = dom (c (#) f) by COMSEQ_3:def_4;
A17: dom (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) = (dom ((Im c) (#) (Re f))) /\ (dom ((Re c) (#) (Im f))) by VALUED_1:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Im_(c_(#)_f))_holds_
(Im_(c_(#)_f))_._x_=_(((Im_c)_(#)_(Re_f))_+_((Re_c)_(#)_(Im_f)))_._x
let x be set ; ::_thesis: ( x in dom (Im (c (#) f)) implies (Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x )
assume A18: x in dom (Im (c (#) f)) ; ::_thesis: (Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x
then A19: ((Im c) (#) (Re f)) . x = (Im c) * ((Re f) . x) by A5, A16, A14, A3, VALUED_1:def_5;
(Im (c (#) f)) . x = Im ((c (#) f) . x) by A18, COMSEQ_3:def_4;
then A20: (Im (c (#) f)) . x = Im (c * (f . x)) by A16, A18, VALUED_1:def_5;
A21: (Im f) . x = Im (f . x) by A16, A6, A3, A18, COMSEQ_3:def_4;
A22: (Re f) . x = Re (f . x) by A5, A16, A3, A18, COMSEQ_3:def_3;
A23: ((Re c) (#) (Im f)) . x = (Re c) * ((Im f) . x) by A16, A6, A15, A3, A18, VALUED_1:def_5;
(((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x = (((Im c) (#) (Re f)) . x) + (((Re c) (#) (Im f)) . x) by A5, A16, A6, A14, A15, A3, A17, A18, VALUED_1:def_1;
hence (Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x by A20, A19, A23, A22, A21, COMPLEX1:9; ::_thesis: verum
end;
hence Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) by A5, A16, A6, A14, A15, A3, A17, FUNCT_1:2; ::_thesis: verum
end;
theorem Th4: :: MESFUN6C:4
for X being non empty set
for f being PartFunc of X,COMPLEX holds
( - (Im f) = Re (* (#) f) & Re f = Im (** (#) f) )
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX holds
( - (Im f) = Re (** (#) f) & Re f = Im (** (#) f) )
let f be PartFunc of X,COMPLEX; ::_thesis: ( - (Im f) = Re (** (#) f) & Re f = Im (** (#) f) )
A1: dom (- (Im f)) = dom (Im f) by VALUED_1:8;
A2: dom (** (#) f) = dom f by VALUED_1:def_5;
A3: dom (Im f) = dom f by COMSEQ_3:def_4;
A4: dom (Re (** (#) f)) = dom (** (#) f) by COMSEQ_3:def_3;
now__::_thesis:_for_x_being_set_st_x_in_dom_(-_(Im_f))_holds_
(-_(Im_f))_._x_=_(Re_(**_(#)_f))_._x
let x be set ; ::_thesis: ( x in dom (- (Im f)) implies (- (Im f)) . x = (Re (** (#) f)) . x )
A5: (- (Im f)) . x = - ((Im f) . x) by VALUED_1:8;
A6: Re (** * (f . x)) = ((Re **) * (Re (f . x))) - ((Im **) * (Im (f . x))) by COMPLEX1:9;
assume A7: x in dom (- (Im f)) ; ::_thesis: (- (Im f)) . x = (Re (** (#) f)) . x
then (Re (** (#) f)) . x = Re ((** (#) f) . x) by A1, A4, A2, A3, COMSEQ_3:def_3;
then (Re (** (#) f)) . x = - (Im (f . x)) by A1, A2, A3, A7, A6, COMPLEX1:7, VALUED_1:def_5;
hence (- (Im f)) . x = (Re (** (#) f)) . x by A1, A7, A5, COMSEQ_3:def_4; ::_thesis: verum
end;
hence - (Im f) = Re (** (#) f) by A4, A2, A3, FUNCT_1:2, VALUED_1:8; ::_thesis: Re f = Im (** (#) f)
A8: dom (Re f) = dom f by COMSEQ_3:def_3;
A9: dom (Im (** (#) f)) = dom (** (#) f) by COMSEQ_3:def_4;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Re_f)_holds_
(Re_f)_._x_=_(Im_(**_(#)_f))_._x
let x be set ; ::_thesis: ( x in dom (Re f) implies (Re f) . x = (Im (** (#) f)) . x )
A10: Im (** * (f . x)) = ((Im **) * (Re (f . x))) + ((Re **) * (Im (f . x))) by COMPLEX1:9;
assume A11: x in dom (Re f) ; ::_thesis: (Re f) . x = (Im (** (#) f)) . x
then (Im (** (#) f)) . x = Im ((** (#) f) . x) by A8, A2, A9, COMSEQ_3:def_4;
then (Im (** (#) f)) . x = Re (f . x) by A8, A2, A11, A10, COMPLEX1:7, VALUED_1:def_5;
hence (Re f) . x = (Im (** (#) f)) . x by A11, COMSEQ_3:def_3; ::_thesis: verum
end;
hence Re f = Im (** (#) f) by A8, A2, A9, FUNCT_1:2; ::_thesis: verum
end;
theorem Th5: :: MESFUN6C:5
for X being non empty set
for f, g being PartFunc of X,COMPLEX holds
( Re (f + g) = (Re f) + (Re g) & Im (f + g) = (Im f) + (Im g) )
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,COMPLEX holds
( Re (f + g) = (Re f) + (Re g) & Im (f + g) = (Im f) + (Im g) )
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( Re (f + g) = (Re f) + (Re g) & Im (f + g) = (Im f) + (Im g) )
A1: dom (Re (f + g)) = dom (f + g) by COMSEQ_3:def_3;
A2: dom (Re g) = dom g by COMSEQ_3:def_3;
A3: dom (Re f) = dom f by COMSEQ_3:def_3;
then dom ((Re f) + (Re g)) = (dom f) /\ (dom g) by A2, VALUED_1:def_1;
then A4: dom (Re (f + g)) = dom ((Re f) + (Re g)) by A1, VALUED_1:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Re_(f_+_g))_holds_
(Re_(f_+_g))_._x_=_((Re_f)_+_(Re_g))_._x
let x be set ; ::_thesis: ( x in dom (Re (f + g)) implies (Re (f + g)) . x = ((Re f) + (Re g)) . x )
assume A5: x in dom (Re (f + g)) ; ::_thesis: (Re (f + g)) . x = ((Re f) + (Re g)) . x
then (Re (f + g)) . x = Re ((f + g) . x) by COMSEQ_3:def_3;
then (Re (f + g)) . x = Re ((f . x) + (g . x)) by A1, A5, VALUED_1:def_1;
then A6: (Re (f + g)) . x = (Re (f . x)) + (Re (g . x)) by COMPLEX1:8;
A7: x in (dom f) /\ (dom g) by A1, A5, VALUED_1:def_1;
then x in dom (Re g) by A2, XBOOLE_0:def_4;
then A8: (Re g) . x = Re (g . x) by COMSEQ_3:def_3;
x in dom (Re f) by A3, A7, XBOOLE_0:def_4;
then (Re f) . x = Re (f . x) by COMSEQ_3:def_3;
hence (Re (f + g)) . x = ((Re f) + (Re g)) . x by A4, A5, A6, A8, VALUED_1:def_1; ::_thesis: verum
end;
hence Re (f + g) = (Re f) + (Re g) by A4, FUNCT_1:2; ::_thesis: Im (f + g) = (Im f) + (Im g)
A9: dom (Im (f + g)) = dom (f + g) by COMSEQ_3:def_4;
A10: dom (Im g) = dom g by COMSEQ_3:def_4;
A11: dom (Im f) = dom f by COMSEQ_3:def_4;
then dom ((Im f) + (Im g)) = (dom f) /\ (dom g) by A10, VALUED_1:def_1;
then A12: dom (Im (f + g)) = dom ((Im f) + (Im g)) by A9, VALUED_1:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Im_(f_+_g))_holds_
(Im_(f_+_g))_._x_=_((Im_f)_+_(Im_g))_._x
let x be set ; ::_thesis: ( x in dom (Im (f + g)) implies (Im (f + g)) . x = ((Im f) + (Im g)) . x )
assume A13: x in dom (Im (f + g)) ; ::_thesis: (Im (f + g)) . x = ((Im f) + (Im g)) . x
then (Im (f + g)) . x = Im ((f + g) . x) by COMSEQ_3:def_4;
then (Im (f + g)) . x = Im ((f . x) + (g . x)) by A9, A13, VALUED_1:def_1;
then A14: (Im (f + g)) . x = (Im (f . x)) + (Im (g . x)) by COMPLEX1:8;
A15: x in (dom f) /\ (dom g) by A9, A13, VALUED_1:def_1;
then x in dom (Im g) by A10, XBOOLE_0:def_4;
then A16: (Im g) . x = Im (g . x) by COMSEQ_3:def_4;
x in dom (Im f) by A11, A15, XBOOLE_0:def_4;
then (Im f) . x = Im (f . x) by COMSEQ_3:def_4;
hence (Im (f + g)) . x = ((Im f) + (Im g)) . x by A12, A13, A14, A16, VALUED_1:def_1; ::_thesis: verum
end;
hence Im (f + g) = (Im f) + (Im g) by A12, FUNCT_1:2; ::_thesis: verum
end;
theorem Th6: :: MESFUN6C:6
for X being non empty set
for f, g being PartFunc of X,COMPLEX holds
( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) )
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,COMPLEX holds
( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) )
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) )
Re (f - g) = (Re f) + (Re (- g)) by Th5;
then A1: Re (f - g) = (Re f) + ((- 1) (#) (Re g)) by Th2;
Im (f - g) = (Im f) + (Im (- g)) by Th5;
hence ( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) ) by A1, Th2; ::_thesis: verum
end;
theorem Th7: :: MESFUN6C:7
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A being Element of S holds
( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A being Element of S holds
( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX
for A being Element of S holds
( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )
let f be PartFunc of X,COMPLEX; ::_thesis: for A being Element of S holds
( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )
let A be Element of S; ::_thesis: ( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )
dom ((Re f) | A) = (dom (Re f)) /\ A by RELAT_1:61
.= (dom f) /\ A by COMSEQ_3:def_3 ;
then A1: dom ((Re f) | A) = dom (f | A) by RELAT_1:61
.= dom (Re (f | A)) by COMSEQ_3:def_3 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_((Re_f)_|_A)_holds_
(Re_(f_|_A))_._x_=_((Re_f)_|_A)_._x
let x be set ; ::_thesis: ( x in dom ((Re f) | A) implies (Re (f | A)) . x = ((Re f) | A) . x )
assume A2: x in dom ((Re f) | A) ; ::_thesis: (Re (f | A)) . x = ((Re f) | A) . x
then A3: x in (dom (Re f)) /\ A by RELAT_1:61;
then A4: x in dom (Re f) by XBOOLE_0:def_4;
A5: x in A by A3, XBOOLE_0:def_4;
thus (Re (f | A)) . x = Re ((f | A) . x) by A1, A2, COMSEQ_3:def_3
.= Re (f . x) by A5, FUNCT_1:49
.= (Re f) . x by A4, COMSEQ_3:def_3
.= ((Re f) | A) . x by A5, FUNCT_1:49 ; ::_thesis: verum
end;
hence (Re f) | A = Re (f | A) by A1, FUNCT_1:2; ::_thesis: (Im f) | A = Im (f | A)
dom ((Im f) | A) = (dom (Im f)) /\ A by RELAT_1:61
.= (dom f) /\ A by COMSEQ_3:def_4 ;
then A6: dom ((Im f) | A) = dom (f | A) by RELAT_1:61
.= dom (Im (f | A)) by COMSEQ_3:def_4 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_((Im_f)_|_A)_holds_
(Im_(f_|_A))_._x_=_((Im_f)_|_A)_._x
let x be set ; ::_thesis: ( x in dom ((Im f) | A) implies (Im (f | A)) . x = ((Im f) | A) . x )
assume A7: x in dom ((Im f) | A) ; ::_thesis: (Im (f | A)) . x = ((Im f) | A) . x
then A8: x in (dom (Im f)) /\ A by RELAT_1:61;
then A9: x in dom (Im f) by XBOOLE_0:def_4;
A10: x in A by A8, XBOOLE_0:def_4;
thus (Im (f | A)) . x = Im ((f | A) . x) by A6, A7, COMSEQ_3:def_4
.= Im (f . x) by A10, FUNCT_1:49
.= (Im f) . x by A9, COMSEQ_3:def_4
.= ((Im f) | A) . x by A10, FUNCT_1:49 ; ::_thesis: verum
end;
hence (Im f) | A = Im (f | A) by A6, FUNCT_1:2; ::_thesis: verum
end;
theorem Th8: :: MESFUN6C:8
for X being non empty set
for f being PartFunc of X,COMPLEX holds f = (Re f) + (** (#) (Im f))
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX holds f = (Re f) + (** (#) (Im f))
let f be PartFunc of X,COMPLEX; ::_thesis: f = (Re f) + (** (#) (Im f))
A1: dom f = dom (Re f) by COMSEQ_3:def_3;
A2: dom f = dom (Im f) by COMSEQ_3:def_4;
A3: dom ((Re f) + (** (#) (Im f))) = (dom (Re f)) /\ (dom (** (#) (Im f))) by VALUED_1:def_1
.= (dom f) /\ (dom f) by A1, A2, VALUED_1:def_5 ;
A4: dom (** (#) (Im f)) = dom (Im f) by VALUED_1:def_5;
now__::_thesis:_for_x_being_set_st_x_in_dom_((Re_f)_+_(**_(#)_(Im_f)))_holds_
((Re_f)_+_(**_(#)_(Im_f)))_._x_=_f_._x
let x be set ; ::_thesis: ( x in dom ((Re f) + (** (#) (Im f))) implies ((Re f) + (** (#) (Im f))) . x = f . x )
assume A5: x in dom ((Re f) + (** (#) (Im f))) ; ::_thesis: ((Re f) + (** (#) (Im f))) . x = f . x
then ((Re f) + (** (#) (Im f))) . x = ((Re f) . x) + ((** (#) (Im f)) . x) by VALUED_1:def_1
.= (Re (f . x)) + ((** (#) (Im f)) . x) by A1, A3, A5, COMSEQ_3:def_3
.= (Re (f . x)) + (** * ((Im f) . x)) by A2, A4, A3, A5, VALUED_1:def_5
.= (Re (f . x)) + (** * (Im (f . x))) by A2, A3, A5, COMSEQ_3:def_4 ;
hence ((Re f) + (** (#) (Im f))) . x = f . x by COMPLEX1:13; ::_thesis: verum
end;
hence f = (Re f) + (** (#) (Im f)) by A3, FUNCT_1:2; ::_thesis: verum
end;
theorem :: MESFUN6C:9
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for B, A being Element of S st B c= A & f is_measurable_on A holds
f is_measurable_on B
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for B, A being Element of S st B c= A & f is_measurable_on A holds
f is_measurable_on B
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX
for B, A being Element of S st B c= A & f is_measurable_on A holds
f is_measurable_on B
let f be PartFunc of X,COMPLEX; ::_thesis: for B, A being Element of S st B c= A & f is_measurable_on A holds
f is_measurable_on B
let B, A be Element of S; ::_thesis: ( B c= A & f is_measurable_on A implies f is_measurable_on B )
assume A1: B c= A ; ::_thesis: ( not f is_measurable_on A or f is_measurable_on B )
assume A2: f is_measurable_on A ; ::_thesis: f is_measurable_on B
then Im f is_measurable_on A by Def1;
then A3: Im f is_measurable_on B by A1, MESFUNC6:16;
Re f is_measurable_on A by A2, Def1;
then Re f is_measurable_on B by A1, MESFUNC6:16;
hence f is_measurable_on B by A3, Def1; ::_thesis: verum
end;
theorem :: MESFUN6C:10
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds
f is_measurable_on A \/ B
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds
f is_measurable_on A \/ B
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX
for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds
f is_measurable_on A \/ B
let f be PartFunc of X,COMPLEX; ::_thesis: for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds
f is_measurable_on A \/ B
let A, B be Element of S; ::_thesis: ( f is_measurable_on A & f is_measurable_on B implies f is_measurable_on A \/ B )
assume that
A1: f is_measurable_on A and
A2: f is_measurable_on B ; ::_thesis: f is_measurable_on A \/ B
A3: Im f is_measurable_on B by A2, Def1;
Im f is_measurable_on A by A1, Def1;
then A4: Im f is_measurable_on A \/ B by A3, MESFUNC6:17;
A5: Re f is_measurable_on B by A2, Def1;
Re f is_measurable_on A by A1, Def1;
then Re f is_measurable_on A \/ B by A5, MESFUNC6:17;
hence f is_measurable_on A \/ B by A4, Def1; ::_thesis: verum
end;
theorem :: MESFUN6C:11
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
let f, g be PartFunc of X,COMPLEX; ::_thesis: for A being Element of S st f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A
let A be Element of S; ::_thesis: ( f is_measurable_on A & g is_measurable_on A implies f + g is_measurable_on A )
assume that
A1: f is_measurable_on A and
A2: g is_measurable_on A ; ::_thesis: f + g is_measurable_on A
A3: Im g is_measurable_on A by A2, Def1;
Im f is_measurable_on A by A1, Def1;
then (Im f) + (Im g) is_measurable_on A by A3, MESFUNC6:26;
then A4: Im (f + g) is_measurable_on A by Th5;
A5: Re g is_measurable_on A by A2, Def1;
Re f is_measurable_on A by A1, Def1;
then (Re f) + (Re g) is_measurable_on A by A5, MESFUNC6:26;
then Re (f + g) is_measurable_on A by Th5;
hence f + g is_measurable_on A by A4, Def1; ::_thesis: verum
end;
theorem :: MESFUN6C:12
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
f - g is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
f - g is_measurable_on A
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
f - g is_measurable_on A
let f, g be PartFunc of X,COMPLEX; ::_thesis: for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds
f - g is_measurable_on A
let A be Element of S; ::_thesis: ( f is_measurable_on A & g is_measurable_on A & A c= dom g implies f - g is_measurable_on A )
assume that
A1: f is_measurable_on A and
A2: g is_measurable_on A and
A3: A c= dom g ; ::_thesis: f - g is_measurable_on A
A4: Im g is_measurable_on A by A2, Def1;
A5: A c= dom (Re g) by A3, COMSEQ_3:def_3;
A6: Re g is_measurable_on A by A2, Def1;
A7: A c= dom (Im g) by A3, COMSEQ_3:def_4;
Im f is_measurable_on A by A1, Def1;
then (Im f) - (Im g) is_measurable_on A by A4, A7, MESFUNC6:29;
then A8: Im (f - g) is_measurable_on A by Th6;
Re f is_measurable_on A by A1, Def1;
then (Re f) - (Re g) is_measurable_on A by A6, A5, MESFUNC6:29;
then Re (f - g) is_measurable_on A by Th6;
hence f - g is_measurable_on A by A8, Def1; ::_thesis: verum
end;
theorem :: MESFUN6C:13
for X being non empty set
for Y being set
for f, g being PartFunc of X,COMPLEX st Y c= dom (f + g) holds
( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
proof
let X be non empty set ; ::_thesis: for Y being set
for f, g being PartFunc of X,COMPLEX st Y c= dom (f + g) holds
( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
let Y be set ; ::_thesis: for f, g being PartFunc of X,COMPLEX st Y c= dom (f + g) holds
( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( Y c= dom (f + g) implies ( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) )
A1: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1;
assume A2: Y c= dom (f + g) ; ::_thesis: ( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
then A3: dom ((f + g) | Y) = Y by RELAT_1:62;
dom (g | Y) = (dom g) /\ Y by RELAT_1:61;
then A4: dom (g | Y) = Y by A2, A1, XBOOLE_1:18, XBOOLE_1:28;
dom (f | Y) = (dom f) /\ Y by RELAT_1:61;
then A5: dom (f | Y) = Y by A2, A1, XBOOLE_1:18, XBOOLE_1:28;
then A6: dom ((f | Y) + (g | Y)) = Y /\ Y by A4, VALUED_1:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_((f_+_g)_|_Y)_holds_
((f_+_g)_|_Y)_._x_=_((f_|_Y)_+_(g_|_Y))_._x
let x be set ; ::_thesis: ( x in dom ((f + g) | Y) implies ((f + g) | Y) . x = ((f | Y) + (g | Y)) . x )
assume A7: x in dom ((f + g) | Y) ; ::_thesis: ((f + g) | Y) . x = ((f | Y) + (g | Y)) . x
hence ((f + g) | Y) . x = (f + g) . x by FUNCT_1:47
.= (f . x) + (g . x) by A2, A3, A7, VALUED_1:def_1
.= ((f | Y) . x) + (g . x) by A3, A5, A7, FUNCT_1:47
.= ((f | Y) . x) + ((g | Y) . x) by A3, A4, A7, FUNCT_1:47
.= ((f | Y) + (g | Y)) . x by A3, A6, A7, VALUED_1:def_1 ;
::_thesis: verum
end;
hence ( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) by A2, A6, FUNCT_1:2, RELAT_1:62; ::_thesis: verum
end;
theorem :: MESFUN6C:14
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds
f | B is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds
f | B is_measurable_on A
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX
for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds
f | B is_measurable_on A
let f be PartFunc of X,COMPLEX; ::_thesis: for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds
f | B is_measurable_on A
let B, A be Element of S; ::_thesis: ( f is_measurable_on B & A = (dom f) /\ B implies f | B is_measurable_on A )
assume that
A1: f is_measurable_on B and
A2: A = (dom f) /\ B ; ::_thesis: f | B is_measurable_on A
A3: A = (dom (Im f)) /\ B by A2, COMSEQ_3:def_4;
Im f is_measurable_on B by A1, Def1;
then (Im f) | B is_measurable_on A by A3, MESFUNC6:76;
then A4: Im (f | B) is_measurable_on A by Th7;
A5: A = (dom (Re f)) /\ B by A2, COMSEQ_3:def_3;
Re f is_measurable_on B by A1, Def1;
then (Re f) | B is_measurable_on A by A5, MESFUNC6:76;
then Re (f | B) is_measurable_on A by Th7;
hence f | B is_measurable_on A by A4, Def1; ::_thesis: verum
end;
theorem :: MESFUN6C:15
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX st dom f in S & dom g in S holds
dom (f + g) in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX st dom f in S & dom g in S holds
dom (f + g) in S
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,COMPLEX st dom f in S & dom g in S holds
dom (f + g) in S
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( dom f in S & dom g in S implies dom (f + g) in S )
assume that
A1: dom f in S and
A2: dom g in S ; ::_thesis: dom (f + g) in S
reconsider E1 = dom f, E2 = dom g as Element of S by A1, A2;
dom (f + g) = E1 /\ E2 by VALUED_1:def_1;
hence dom (f + g) in S ; ::_thesis: verum
end;
theorem :: MESFUN6C:16
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A, B being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A, B being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX
for A, B being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
let f be PartFunc of X,COMPLEX; ::_thesis: for A, B being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
let A, B be Element of S; ::_thesis: ( dom f = A implies ( f is_measurable_on B iff f is_measurable_on A /\ B ) )
assume A1: dom f = A ; ::_thesis: ( f is_measurable_on B iff f is_measurable_on A /\ B )
then A2: dom (Re f) = A by COMSEQ_3:def_3;
A3: dom (Im f) = A by A1, COMSEQ_3:def_4;
hereby ::_thesis: ( f is_measurable_on A /\ B implies f is_measurable_on B )
assume A4: f is_measurable_on B ; ::_thesis: f is_measurable_on A /\ B
then Im f is_measurable_on B by Def1;
then A5: Im f is_measurable_on A /\ B by A3, MESFUNC6:80;
Re f is_measurable_on B by A4, Def1;
then Re f is_measurable_on A /\ B by A2, MESFUNC6:80;
hence f is_measurable_on A /\ B by A5, Def1; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A6: f is_measurable_on A /\ B ; ::_thesis: f is_measurable_on B
then Im f is_measurable_on A /\ B by Def1;
then A7: Im f is_measurable_on B by A3, MESFUNC6:80;
Re f is_measurable_on A /\ B by A6, Def1;
then Re f is_measurable_on B by A2, MESFUNC6:80;
hence f is_measurable_on B by A7, Def1; ::_thesis: verum
end;
end;
theorem Th17: :: MESFUN6C:17
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for c being complex number
for A being Element of S st f is_measurable_on A & A c= dom f holds
c (#) f is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for c being complex number
for A being Element of S st f is_measurable_on A & A c= dom f holds
c (#) f is_measurable_on A
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX
for c being complex number
for A being Element of S st f is_measurable_on A & A c= dom f holds
c (#) f is_measurable_on A
let f be PartFunc of X,COMPLEX; ::_thesis: for c being complex number
for A being Element of S st f is_measurable_on A & A c= dom f holds
c (#) f is_measurable_on A
let c be complex number ; ::_thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds
c (#) f is_measurable_on A
let A be Element of S; ::_thesis: ( f is_measurable_on A & A c= dom f implies c (#) f is_measurable_on A )
assume that
A1: f is_measurable_on A and
A2: A c= dom f ; ::_thesis: c (#) f is_measurable_on A
A3: dom (Im f) = dom f by COMSEQ_3:def_4;
A4: Im f is_measurable_on A by A1, Def1;
then A5: (Re c) (#) (Im f) is_measurable_on A by A2, A3, MESFUNC6:21;
A6: (Im c) (#) (Im f) is_measurable_on A by A2, A4, A3, MESFUNC6:21;
A7: dom (Re f) = dom f by COMSEQ_3:def_3;
A8: Re f is_measurable_on A by A1, Def1;
then (Im c) (#) (Re f) is_measurable_on A by A2, A7, MESFUNC6:21;
then ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) is_measurable_on A by A5, MESFUNC6:26;
then A9: Im (c (#) f) is_measurable_on A by Th3;
dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def_5;
then A10: A c= dom ((Im c) (#) (Im f)) by A2, COMSEQ_3:def_4;
(Re c) (#) (Re f) is_measurable_on A by A2, A8, A7, MESFUNC6:21;
then ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) is_measurable_on A by A6, A10, MESFUNC6:29;
then Re (c (#) f) is_measurable_on A by Th3;
hence c (#) f is_measurable_on A by A9, Def1; ::_thesis: verum
end;
theorem :: MESFUN6C:18
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX st ex A being Element of S st dom f = A holds
for c being complex number
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX st ex A being Element of S st dom f = A holds
for c being complex number
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX st ex A being Element of S st dom f = A holds
for c being complex number
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
let f be PartFunc of X,COMPLEX; ::_thesis: ( ex A being Element of S st dom f = A implies for c being complex number
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B )
assume ex A being Element of S st A = dom f ; ::_thesis: for c being complex number
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
then consider A being Element of S such that
A1: A = dom f ;
hereby ::_thesis: verum
let c be complex number ; ::_thesis: for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
let B be Element of S; ::_thesis: ( f is_measurable_on B implies c (#) f is_measurable_on B )
A2: dom ((Re c) (#) (Re f)) = dom (Re f) by VALUED_1:def_5;
A3: dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def_5;
dom (Re (c (#) f)) = dom (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) by Th3;
then A4: dom (Re (c (#) f)) = (dom ((Re c) (#) (Re f))) /\ (dom ((Im c) (#) (Im f))) by VALUED_1:12;
A5: dom ((Im c) (#) (Re f)) = dom (Re f) by VALUED_1:def_5;
dom (Im (c (#) f)) = dom (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) by Th3;
then A6: dom (Im (c (#) f)) = (dom ((Im c) (#) (Re f))) /\ (dom ((Re c) (#) (Im f))) by VALUED_1:def_1;
A7: dom ((Re c) (#) (Im f)) = dom (Im f) by VALUED_1:def_5;
A8: dom (Re f) = dom f by COMSEQ_3:def_3;
A9: dom (Im f) = dom f by COMSEQ_3:def_4;
assume A10: f is_measurable_on B ; ::_thesis: c (#) f is_measurable_on B
then Im f is_measurable_on B by Def1;
then A11: Im f is_measurable_on A /\ B by A1, A9, MESFUNC6:80;
Re f is_measurable_on B by A10, Def1;
then Re f is_measurable_on A /\ B by A1, A8, MESFUNC6:80;
then f is_measurable_on A /\ B by A11, Def1;
then A12: c (#) f is_measurable_on A /\ B by A1, Th17, XBOOLE_1:17;
then Im (c (#) f) is_measurable_on A /\ B by Def1;
then A13: Im (c (#) f) is_measurable_on B by A1, A8, A9, A5, A7, A6, MESFUNC6:80;
Re (c (#) f) is_measurable_on A /\ B by A12, Def1;
then Re (c (#) f) is_measurable_on B by A1, A8, A9, A2, A3, A4, MESFUNC6:80;
hence c (#) f is_measurable_on B by A13, Def1; ::_thesis: verum
end;
end;
begin
definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,COMPLEX;
predf is_integrable_on M means :Def2: :: MESFUN6C:def 2
( Re f is_integrable_on M & Im f is_integrable_on M );
end;
:: deftheorem Def2 defines is_integrable_on MESFUN6C:def_2_:_
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX holds
( f is_integrable_on M iff ( Re f is_integrable_on M & Im f is_integrable_on M ) );
definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,COMPLEX;
assume A1: f is_integrable_on M ;
func Integral (M,f) -> complex number means :Def3: :: MESFUN6C:def 3
ex R, I being Real st
( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & it = R + (I * **) );
existence
ex b1 being complex number ex R, I being Real st
( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b1 = R + (I * **) )
proof
A2: Im f is_integrable_on M by A1, Def2;
then A3: -infty < Integral (M,(Im f)) by MESFUNC6:90;
A4: Re f is_integrable_on M by A1, Def2;
then A5: Integral (M,(Re f)) < +infty by MESFUNC6:90;
A6: Integral (M,(Im f)) < +infty by A2, MESFUNC6:90;
-infty < Integral (M,(Re f)) by A4, MESFUNC6:90;
then reconsider R = Integral (M,(Re f)), I = Integral (M,(Im f)) as Real by A5, A3, A6, XXREAL_0:14;
take R + (I * **) ; ::_thesis: ex R, I being Real st
( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & R + (I * **) = R + (I * **) )
thus ex R, I being Real st
( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & R + (I * **) = R + (I * **) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being complex number st ex R, I being Real st
( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b1 = R + (I * **) ) & ex R, I being Real st
( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b2 = R + (I * **) ) holds
b1 = b2 ;
end;
:: deftheorem Def3 defines Integral MESFUN6C:def_3_:_
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
for b5 being complex number holds
( b5 = Integral (M,f) iff ex R, I being Real st
( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b5 = R + (I * **) ) );
Lm1: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL holds
( max+ f is nonnegative & max- f is nonnegative )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL holds
( max+ f is nonnegative & max- f is nonnegative )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL holds
( max+ f is nonnegative & max- f is nonnegative )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,ExtREAL holds
( max+ f is nonnegative & max- f is nonnegative )
let f be PartFunc of X,ExtREAL; ::_thesis: ( max+ f is nonnegative & max- f is nonnegative )
A1: for x being set st x in dom (max- f) holds
0 <= (max- f) . x by MESFUNC2:13;
for x being set st x in dom (max+ f) holds
0 <= (max+ f) . x by MESFUNC2:12;
hence ( max+ f is nonnegative & max- f is nonnegative ) by A1, SUPINF_2:52; ::_thesis: verum
end;
theorem Th19: :: MESFUN6C:19
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
f | A is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
f | A is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
f | A is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,ExtREAL
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
f | A is_integrable_on M
let f be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
f | A is_integrable_on M
let A be Element of S; ::_thesis: ( ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 implies f | A is_integrable_on M )
assume that
A1: ex E being Element of S st
( E = dom f & f is_measurable_on E ) and
A2: M . A = 0 ; ::_thesis: f | A is_integrable_on M
A3: dom f = dom (max+ f) by MESFUNC2:def_2;
max+ f is nonnegative by Lm1;
then integral+ (M,((max+ f) | A)) = 0 by A1, A2, A3, MESFUNC2:25, MESFUNC5:82;
then A4: integral+ (M,(max+ (f | A))) < +infty by MESFUNC5:28;
consider E being Element of S such that
A5: E = dom f and
A6: f is_measurable_on E by A1;
A7: (dom f) /\ (A /\ E) = A /\ E by A5, XBOOLE_1:17, XBOOLE_1:28;
A8: dom f = dom (max- f) by MESFUNC2:def_3;
max- f is nonnegative by Lm1;
then integral+ (M,((max- f) | A)) = 0 by A1, A2, A8, MESFUNC2:26, MESFUNC5:82;
then A9: integral+ (M,(max- (f | A))) < +infty by MESFUNC5:28;
A10: dom (f | A) = (dom f) /\ A by RELAT_1:61;
f is_measurable_on A /\ E by A6, MESFUNC1:30, XBOOLE_1:17;
then A11: f | (A /\ E) is_measurable_on A /\ E by A7, MESFUNC5:42;
f | (A /\ E) = (f | A) /\ (f | E) by RELAT_1:79
.= (f | A) /\ f by A5, RELAT_1:69
.= f | A by RELAT_1:59, XBOOLE_1:28 ;
hence f | A is_integrable_on M by A5, A11, A10, A4, A9, MESFUNC5:def_17; ::_thesis: verum
end;
theorem Th20: :: MESFUN6C:20
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for E, A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
f | A is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL
for E, A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
f | A is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for E, A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
f | A is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL
for E, A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
f | A is_integrable_on M
let f be PartFunc of X,REAL; ::_thesis: for E, A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
f | A is_integrable_on M
let E, A be Element of S; ::_thesis: ( ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 implies f | A is_integrable_on M )
assume that
A1: ex E being Element of S st
( E = dom f & f is_measurable_on E ) and
A2: M . A = 0 ; ::_thesis: f | A is_integrable_on M
consider E being Element of S such that
A3: E = dom f and
A4: f is_measurable_on E by A1;
R_EAL f is_measurable_on E by A4, MESFUNC6:def_1;
then R_EAL (f | A) is_integrable_on M by A2, A3, Th19;
hence f | A is_integrable_on M by MESFUNC6:def_4; ::_thesis: verum
end;
theorem :: MESFUN6C:21
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
( f | A is_integrable_on M & Integral (M,(f | A)) = 0 )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
( f | A is_integrable_on M & Integral (M,(f | A)) = 0 )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
( f | A is_integrable_on M & Integral (M,(f | A)) = 0 )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX
for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
( f | A is_integrable_on M & Integral (M,(f | A)) = 0 )
let f be PartFunc of X,COMPLEX; ::_thesis: for A being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 holds
( f | A is_integrable_on M & Integral (M,(f | A)) = 0 )
let A be Element of S; ::_thesis: ( ex E being Element of S st
( E = dom f & f is_measurable_on E ) & M . A = 0 implies ( f | A is_integrable_on M & Integral (M,(f | A)) = 0 ) )
set g = f | A;
assume that
A1: ex E being Element of S st
( E = dom f & f is_measurable_on E ) and
A2: M . A = 0 ; ::_thesis: ( f | A is_integrable_on M & Integral (M,(f | A)) = 0 )
consider E being Element of S such that
A3: E = dom f and
A4: f is_measurable_on E by A1;
A5: dom (Im f) = dom f by COMSEQ_3:def_4;
A6: Im f is_measurable_on E by A4, Def1;
then A7: Integral (M,((Im f) | A)) = 0 by A2, A3, A5, MESFUNC6:88;
(Im f) | A is_integrable_on M by A2, A3, A6, A5, Th20;
then A8: Im (f | A) is_integrable_on M by Th7;
A9: dom (Re f) = dom f by COMSEQ_3:def_3;
A10: Im (f | A) = (Im f) | A by Th7;
A11: Re f is_measurable_on E by A4, Def1;
A12: Re (f | A) = (Re f) | A by Th7;
then reconsider R = Integral (M,(Re (f | A))), I = Integral (M,(Im (f | A))) as Real by A2, A3, A11, A6, A9, A5, A10, MESFUNC6:88;
(Re f) | A is_integrable_on M by A2, A3, A11, A9, Th20;
then Re (f | A) is_integrable_on M by Th7;
hence f | A is_integrable_on M by A8, Def2; ::_thesis: Integral (M,(f | A)) = 0
hence Integral (M,(f | A)) = R + (I * **) by Def3
.= 0 by A2, A3, A11, A9, A7, A12, A10, MESFUNC6:88 ;
::_thesis: verum
end;
theorem :: MESFUN6C:22
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for E, A being Element of S st E = dom f & f is_integrable_on M & M . A = 0 holds
Integral (M,(f | (E \ A))) = Integral (M,f)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for E, A being Element of S st E = dom f & f is_integrable_on M & M . A = 0 holds
Integral (M,(f | (E \ A))) = Integral (M,f)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for E, A being Element of S st E = dom f & f is_integrable_on M & M . A = 0 holds
Integral (M,(f | (E \ A))) = Integral (M,f)
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX
for E, A being Element of S st E = dom f & f is_integrable_on M & M . A = 0 holds
Integral (M,(f | (E \ A))) = Integral (M,f)
let f be PartFunc of X,COMPLEX; ::_thesis: for E, A being Element of S st E = dom f & f is_integrable_on M & M . A = 0 holds
Integral (M,(f | (E \ A))) = Integral (M,f)
let E, A be Element of S; ::_thesis: ( E = dom f & f is_integrable_on M & M . A = 0 implies Integral (M,(f | (E \ A))) = Integral (M,f) )
assume that
A1: E = dom f and
A2: f is_integrable_on M and
A3: M . A = 0 ; ::_thesis: Integral (M,(f | (E \ A))) = Integral (M,f)
set C = E \ A;
A4: dom f = dom (Re f) by COMSEQ_3:def_3;
A5: Im f is_integrable_on M by A2, Def2;
then R_EAL (Im f) is_integrable_on M by MESFUNC6:def_4;
then consider IE being Element of S such that
A6: IE = dom (R_EAL (Im f)) and
A7: R_EAL (Im f) is_measurable_on IE by MESFUNC5:def_17;
A8: dom f = dom (Im f) by COMSEQ_3:def_4;
A9: Integral (M,((Im f) | (E \ A))) = Integral (M,(Im (f | (E \ A)))) by Th7;
Im f is_measurable_on IE by A7, MESFUNC6:def_1;
then A10: Integral (M,(Im (f | (E \ A)))) = Integral (M,(Im f)) by A1, A3, A8, A6, A9, MESFUNC6:89;
(Im f) | (E \ A) is_integrable_on M by A5, MESFUNC6:91;
then A11: Im (f | (E \ A)) is_integrable_on M by Th7;
then A12: -infty < Integral (M,(Im (f | (E \ A)))) by MESFUNC6:90;
A13: Re f is_integrable_on M by A2, Def2;
then R_EAL (Re f) is_integrable_on M by MESFUNC6:def_4;
then consider RE being Element of S such that
A14: RE = dom (R_EAL (Re f)) and
A15: R_EAL (Re f) is_measurable_on RE by MESFUNC5:def_17;
A16: Integral (M,((Re f) | (E \ A))) = Integral (M,(Re (f | (E \ A)))) by Th7;
Re f is_measurable_on RE by A15, MESFUNC6:def_1;
then A17: Integral (M,(Re (f | (E \ A)))) = Integral (M,(Re f)) by A1, A3, A4, A14, A16, MESFUNC6:89;
(Re f) | (E \ A) is_integrable_on M by A13, MESFUNC6:91;
then A18: Re (f | (E \ A)) is_integrable_on M by Th7;
then A19: Integral (M,(Re (f | (E \ A)))) < +infty by MESFUNC6:90;
A20: Integral (M,(Im (f | (E \ A)))) < +infty by A11, MESFUNC6:90;
-infty < Integral (M,(Re (f | (E \ A)))) by A18, MESFUNC6:90;
then reconsider R2 = Integral (M,(Re (f | (E \ A)))), I2 = Integral (M,(Im (f | (E \ A)))) as Real by A19, A12, A20, XXREAL_0:14;
f | (E \ A) is_integrable_on M by A18, A11, Def2;
hence Integral (M,(f | (E \ A))) = R2 + (I2 * **) by Def3
.= Integral (M,f) by A2, A17, A10, Def3 ;
::_thesis: verum
end;
theorem Th23: :: MESFUN6C:23
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for A being Element of S st f is_integrable_on M holds
f | A is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for A being Element of S st f is_integrable_on M holds
f | A is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for A being Element of S st f is_integrable_on M holds
f | A is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX
for A being Element of S st f is_integrable_on M holds
f | A is_integrable_on M
let f be PartFunc of X,COMPLEX; ::_thesis: for A being Element of S st f is_integrable_on M holds
f | A is_integrable_on M
let A be Element of S; ::_thesis: ( f is_integrable_on M implies f | A is_integrable_on M )
assume A1: f is_integrable_on M ; ::_thesis: f | A is_integrable_on M
then Im f is_integrable_on M by Def2;
then (Im f) | A is_integrable_on M by MESFUNC6:91;
then A2: Im (f | A) is_integrable_on M by Th7;
Re f is_integrable_on M by A1, Def2;
then (Re f) | A is_integrable_on M by MESFUNC6:91;
then Re (f | A) is_integrable_on M by Th7;
hence f | A is_integrable_on M by A2, Def2; ::_thesis: verum
end;
theorem :: MESFUN6C:24
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for A, B being Element of S st f is_integrable_on M & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for A, B being Element of S st f is_integrable_on M & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for A, B being Element of S st f is_integrable_on M & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX
for A, B being Element of S st f is_integrable_on M & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let f be PartFunc of X,COMPLEX; ::_thesis: for A, B being Element of S st f is_integrable_on M & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let A, B be Element of S; ::_thesis: ( f is_integrable_on M & A misses B implies Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
assume that
A1: f is_integrable_on M and
A2: A misses B ; ::_thesis: Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
A3: f | B is_integrable_on M by A1, Th23;
then A4: Re (f | B) is_integrable_on M by Def2;
then A5: Integral (M,(Re (f | B))) < +infty by MESFUNC6:90;
A6: Im (f | B) is_integrable_on M by A3, Def2;
then A7: -infty < Integral (M,(Im (f | B))) by MESFUNC6:90;
A8: Integral (M,(Im (f | B))) < +infty by A6, MESFUNC6:90;
-infty < Integral (M,(Re (f | B))) by A4, MESFUNC6:90;
then reconsider R2 = Integral (M,(Re (f | B))), I2 = Integral (M,(Im (f | B))) as Real by A5, A7, A8, XXREAL_0:14;
A9: f | A is_integrable_on M by A1, Th23;
then A10: Re (f | A) is_integrable_on M by Def2;
then A11: Integral (M,(Re (f | A))) < +infty by MESFUNC6:90;
set C = A \/ B;
A12: f | (A \/ B) is_integrable_on M by A1, Th23;
then A13: Re (f | (A \/ B)) is_integrable_on M by Def2;
then A14: Integral (M,(Re (f | (A \/ B)))) < +infty by MESFUNC6:90;
A15: Im (f | (A \/ B)) is_integrable_on M by A12, Def2;
then A16: -infty < Integral (M,(Im (f | (A \/ B)))) by MESFUNC6:90;
A17: Integral (M,(Im (f | (A \/ B)))) < +infty by A15, MESFUNC6:90;
-infty < Integral (M,(Re (f | (A \/ B)))) by A13, MESFUNC6:90;
then reconsider R3 = Integral (M,(Re (f | (A \/ B)))), I3 = Integral (M,(Im (f | (A \/ B)))) as Real by A14, A16, A17, XXREAL_0:14;
A18: Integral (M,(f | (A \/ B))) = R3 + (I3 * **) by A12, Def3;
A19: Im (f | A) is_integrable_on M by A9, Def2;
then A20: -infty < Integral (M,(Im (f | A))) by MESFUNC6:90;
A21: Integral (M,(Im (f | A))) < +infty by A19, MESFUNC6:90;
-infty < Integral (M,(Re (f | A))) by A10, MESFUNC6:90;
then reconsider R1 = Integral (M,(Re (f | A))), I1 = Integral (M,(Im (f | A))) as Real by A11, A20, A21, XXREAL_0:14;
Im f is_integrable_on M by A1, Def2;
then Integral (M,((Im f) | (A \/ B))) = (Integral (M,((Im f) | A))) + (Integral (M,((Im f) | B))) by A2, MESFUNC6:92;
then Integral (M,((Im f) | (A \/ B))) = (Integral (M,(Im (f | A)))) + (Integral (M,((Im f) | B))) by Th7
.= (Integral (M,(Im (f | A)))) + (Integral (M,(Im (f | B)))) by Th7 ;
then R_EAL I3 = (R_EAL I1) + (R_EAL I2) by Th7;
then A22: I3 = I1 + I2 by SUPINF_2:1;
Re f is_integrable_on M by A1, Def2;
then Integral (M,((Re f) | (A \/ B))) = (Integral (M,((Re f) | A))) + (Integral (M,((Re f) | B))) by A2, MESFUNC6:92;
then Integral (M,((Re f) | (A \/ B))) = (Integral (M,(Re (f | A)))) + (Integral (M,((Re f) | B))) by Th7
.= (Integral (M,(Re (f | A)))) + (Integral (M,(Re (f | B)))) by Th7 ;
then R_EAL R3 = (R_EAL R1) + (R_EAL R2) by Th7;
then R3 = R1 + R2 by SUPINF_2:1;
then Integral (M,(f | (A \/ B))) = (R1 + (I1 * **)) + (R2 + (I2 * **)) by A22, A18;
then Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (R2 + (I2 * **)) by A9, Def3;
hence Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A3, Def3; ::_thesis: verum
end;
theorem :: MESFUN6C:25
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds
( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds
( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds
( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX
for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds
( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
let f be PartFunc of X,COMPLEX; ::_thesis: for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds
( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
let B, A be Element of S; ::_thesis: ( f is_integrable_on M & B = (dom f) \ A implies ( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) )
assume that
A1: f is_integrable_on M and
A2: B = (dom f) \ A ; ::_thesis: ( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
A3: Re f is_integrable_on M by A1, Def2;
then A4: Integral (M,(Re f)) < +infty by MESFUNC6:90;
A5: Im f is_integrable_on M by A1, Def2;
then A6: -infty < Integral (M,(Im f)) by MESFUNC6:90;
A7: Integral (M,(Im f)) < +infty by A5, MESFUNC6:90;
-infty < Integral (M,(Re f)) by A3, MESFUNC6:90;
then reconsider R = Integral (M,(Re f)), I = Integral (M,(Im f)) as Real by A4, A6, A7, XXREAL_0:14;
A8: Integral (M,f) = R + (I * **) by A1, Def3;
A9: f | B is_integrable_on M by A1, Th23;
then A10: Re (f | B) is_integrable_on M by Def2;
then A11: Integral (M,(Re (f | B))) < +infty by MESFUNC6:90;
A12: Im (f | B) is_integrable_on M by A9, Def2;
then A13: -infty < Integral (M,(Im (f | B))) by MESFUNC6:90;
A14: Integral (M,(Im (f | B))) < +infty by A12, MESFUNC6:90;
-infty < Integral (M,(Re (f | B))) by A10, MESFUNC6:90;
then reconsider R2 = Integral (M,(Re (f | B))), I2 = Integral (M,(Im (f | B))) as Real by A11, A13, A14, XXREAL_0:14;
A15: f | A is_integrable_on M by A1, Th23;
then A16: Re (f | A) is_integrable_on M by Def2;
then A17: Integral (M,(Re (f | A))) < +infty by MESFUNC6:90;
A18: Im (f | A) is_integrable_on M by A15, Def2;
then A19: -infty < Integral (M,(Im (f | A))) by MESFUNC6:90;
A20: Integral (M,(Im (f | A))) < +infty by A18, MESFUNC6:90;
-infty < Integral (M,(Re (f | A))) by A16, MESFUNC6:90;
then reconsider R1 = Integral (M,(Re (f | A))), I1 = Integral (M,(Im (f | A))) as Real by A17, A19, A20, XXREAL_0:14;
dom f = dom (Im f) by COMSEQ_3:def_4;
then Integral (M,(Im f)) = (Integral (M,((Im f) | A))) + (Integral (M,((Im f) | B))) by A2, A5, MESFUNC6:93;
then Integral (M,(Im f)) = (Integral (M,(Im (f | A)))) + (Integral (M,((Im f) | B))) by Th7
.= (Integral (M,(Im (f | A)))) + (Integral (M,(Im (f | B)))) by Th7 ;
then A21: I = I1 + I2 by SUPINF_2:1;
dom f = dom (Re f) by COMSEQ_3:def_3;
then Integral (M,(Re f)) = (Integral (M,((Re f) | A))) + (Integral (M,((Re f) | B))) by A2, A3, MESFUNC6:93;
then Integral (M,(Re f)) = (Integral (M,(Re (f | A)))) + (Integral (M,((Re f) | B))) by Th7
.= (Integral (M,(Re (f | A)))) + (Integral (M,(Re (f | B)))) by Th7 ;
then R = R1 + R2 by SUPINF_2:1;
then Integral (M,f) = (R1 + (I1 * **)) + (R2 + (I2 * **)) by A21, A8;
then Integral (M,f) = (Integral (M,(f | A))) + (R2 + (I2 * **)) by A15, Def3;
hence ( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) by A1, A9, Def3, Th23; ::_thesis: verum
end;
definition
let k be real number ;
let X be non empty set ;
let f be PartFunc of X,REAL;
funcf to_power k -> PartFunc of X,REAL means :Def4: :: MESFUN6C:def 4
( dom it = dom f & ( for x being Element of X st x in dom it holds
it . x = (f . x) to_power k ) );
existence
ex b1 being PartFunc of X,REAL st
( dom b1 = dom f & ( for x being Element of X st x in dom b1 holds
b1 . x = (f . x) to_power k ) )
proof
defpred S1[ set , set ] means ( $1 in dom f & $2 = (f . $1) to_power k );
consider F being PartFunc of X,REAL such that
A1: for z being Element of X holds
( z in dom F iff ex c being Element of REAL st S1[z,c] ) and
A2: for z being Element of X st z in dom F holds
S1[z,F . z] from SEQ_1:sch_2();
take F ; ::_thesis: ( dom F = dom f & ( for x being Element of X st x in dom F holds
F . x = (f . x) to_power k ) )
now__::_thesis:_for_z_being_Element_of_X_holds_
(_(_z_in_dom_f_implies_z_in_dom_F_)_&_(_z_in_dom_F_implies_z_in_dom_f_)_)
let z be Element of X; ::_thesis: ( ( z in dom f implies z in dom F ) & ( z in dom F implies z in dom f ) )
hereby ::_thesis: ( z in dom F implies z in dom f )
A3: (f . z) to_power k is Element of REAL by XREAL_0:def_1;
assume z in dom f ; ::_thesis: z in dom F
hence z in dom F by A1, A3; ::_thesis: verum
end;
hereby ::_thesis: verum
assume z in dom F ; ::_thesis: z in dom f
then ex c being Element of REAL st S1[z,c] by A1;
hence z in dom f ; ::_thesis: verum
end;
end;
hence dom F = dom f by SUBSET_1:3; ::_thesis: for x being Element of X st x in dom F holds
F . x = (f . x) to_power k
thus for x being Element of X st x in dom F holds
F . x = (f . x) to_power k by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of X,REAL st dom b1 = dom f & ( for x being Element of X st x in dom b1 holds
b1 . x = (f . x) to_power k ) & dom b2 = dom f & ( for x being Element of X st x in dom b2 holds
b2 . x = (f . x) to_power k ) holds
b1 = b2
proof
deffunc H1( set ) -> set = (f . $1) to_power k;
thus for h, g being PartFunc of X,REAL st dom h = dom f & ( for z being Element of X st z in dom h holds
h . z = H1(z) ) & dom g = dom f & ( for z being Element of X st z in dom g holds
g . z = H1(z) ) holds
h = g from SEQ_1:sch_4(); ::_thesis: verum
end;
end;
:: deftheorem Def4 defines to_power MESFUN6C:def_4_:_
for k being real number
for X being non empty set
for f, b4 being PartFunc of X,REAL holds
( b4 = f to_power k iff ( dom b4 = dom f & ( for x being Element of X st x in dom b4 holds
b4 . x = (f . x) to_power k ) ) );
registration
let X be non empty set ;
cluster Relation-like X -defined REAL -valued Function-like V33() V34() V35() nonnegative for Element of K6(K7(X,REAL));
existence
ex b1 being PartFunc of X,REAL st b1 is nonnegative
proof
reconsider f = {} as Function ;
reconsider f = f as PartFunc of X,REAL by RELSET_1:12;
take f ; ::_thesis: f is nonnegative
let x be Element of ExtREAL ; :: according to SUPINF_2:def_9,SUPINF_2:def_16 ::_thesis: ( not x in rng f or 0. <= x )
thus ( not x in rng f or 0. <= x ) ; ::_thesis: verum
end;
end;
registration
let k be real non negative number ;
let X be non empty set ;
let f be nonnegative PartFunc of X,REAL;
clusterf to_power k -> nonnegative ;
coherence
f to_power k is nonnegative
proof
now__::_thesis:_for_x_being_set_st_x_in_dom_(f_to_power_k)_holds_
0_<=_(f_to_power_k)_._x
let x be set ; ::_thesis: ( x in dom (f to_power k) implies 0 <= (f to_power k) . b1 )
assume A1: x in dom (f to_power k) ; ::_thesis: 0 <= (f to_power k) . b1
percases ( k = 0 or k > 0 ) ;
suppose k = 0 ; ::_thesis: 0 <= (f to_power k) . b1
then (f . x) to_power k = 1 by POWER:24;
hence 0 <= (f to_power k) . x by A1, Def4; ::_thesis: verum
end;
supposeA2: k > 0 ; ::_thesis: 0 <= (f to_power k) . b1
percases ( 0 < f . x or 0 = f . x ) by MESFUNC6:51;
suppose 0 < f . x ; ::_thesis: 0 <= (f to_power k) . b1
then 0 < (f . x) to_power k by POWER:34;
hence 0 <= (f to_power k) . x by A1, Def4; ::_thesis: verum
end;
suppose 0 = f . x ; ::_thesis: 0 <= (f to_power k) . b1
then 0 = (f . x) to_power k by A2, POWER:def_2;
hence 0 <= (f to_power k) . x by A1, Def4; ::_thesis: verum
end;
end;
end;
end;
end;
hence f to_power k is nonnegative by MESFUNC6:52; ::_thesis: verum
end;
end;
theorem Th26: :: MESFUN6C:26
for k being real number
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative & 0 <= k holds
f to_power k is nonnegative ;
theorem Th27: :: MESFUN6C:27
for x being set
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative holds
(f . x) to_power (1 / 2) = sqrt (f . x)
proof
let x be set ; ::_thesis: for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative holds
(f . x) to_power (1 / 2) = sqrt (f . x)
let X be non empty set ; ::_thesis: for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative holds
(f . x) to_power (1 / 2) = sqrt (f . x)
let S be SigmaField of X; ::_thesis: for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative holds
(f . x) to_power (1 / 2) = sqrt (f . x)
let E be Element of S; ::_thesis: for f being PartFunc of X,REAL st f is nonnegative holds
(f . x) to_power (1 / 2) = sqrt (f . x)
let f be PartFunc of X,REAL; ::_thesis: ( f is nonnegative implies (f . x) to_power (1 / 2) = sqrt (f . x) )
assume f is nonnegative ; ::_thesis: (f . x) to_power (1 / 2) = sqrt (f . x)
then A1: 0 <= f . x by MESFUNC6:51;
hence (f . x) to_power (1 / 2) = 2 -root (f . x) by POWER:45
.= 2 -Root (f . x) by A1, POWER:def_1
.= sqrt (f . x) by A1, PREPOWER:32 ;
::_thesis: verum
end;
theorem Th28: :: MESFUN6C:28
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a)))
let S be SigmaField of X; ::_thesis: for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a)))
let A be Element of S; ::_thesis: for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a)))
let f be PartFunc of X,REAL; ::_thesis: for a being Real st A c= dom f holds
A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a)))
let a be Real; ::_thesis: ( A c= dom f implies A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) )
now__::_thesis:_for_x_being_set_st_x_in_A_/\_(less_dom_(f,a))_holds_
x_in_A_\_(A_/\_(great_eq_dom_(f,a)))
let x be set ; ::_thesis: ( x in A /\ (less_dom (f,a)) implies x in A \ (A /\ (great_eq_dom (f,a))) )
assume A1: x in A /\ (less_dom (f,a)) ; ::_thesis: x in A \ (A /\ (great_eq_dom (f,a)))
then x in less_dom (f,a) by XBOOLE_0:def_4;
then ex y being Real st
( y = f . x & y < a ) by MESFUNC6:3;
then for y1 being Real holds
( not y1 = f . x or not a <= y1 ) ;
then not x in great_eq_dom (f,a) by MESFUNC6:6;
then A2: not x in A /\ (great_eq_dom (f,a)) by XBOOLE_0:def_4;
x in A by A1, XBOOLE_0:def_4;
hence x in A \ (A /\ (great_eq_dom (f,a))) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
then A3: A /\ (less_dom (f,a)) c= A \ (A /\ (great_eq_dom (f,a))) by TARSKI:def_3;
assume A4: A c= dom f ; ::_thesis: A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a)))
now__::_thesis:_for_x_being_set_st_x_in_A_\_(A_/\_(great_eq_dom_(f,a)))_holds_
x_in_A_/\_(less_dom_(f,a))
let x be set ; ::_thesis: ( x in A \ (A /\ (great_eq_dom (f,a))) implies x in A /\ (less_dom (f,a)) )
assume A5: x in A \ (A /\ (great_eq_dom (f,a))) ; ::_thesis: x in A /\ (less_dom (f,a))
then A6: x in A by XBOOLE_0:def_5;
not x in A /\ (great_eq_dom (f,a)) by A5, XBOOLE_0:def_5;
then not x in great_eq_dom (f,a) by A6, XBOOLE_0:def_4;
then not a <= f . x by A4, A6, MESFUNC6:6;
then x in less_dom (f,a) by A4, A6, MESFUNC6:3;
hence x in A /\ (less_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
then A \ (A /\ (great_eq_dom (f,a))) c= A /\ (less_dom (f,a)) by TARSKI:def_3;
hence A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th29: :: MESFUN6C:29
for k being real number
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds
f to_power k is_measurable_on E
proof
let k be real number ; ::_thesis: for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds
f to_power k is_measurable_on E
let X be non empty set ; ::_thesis: for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds
f to_power k is_measurable_on E
let S be SigmaField of X; ::_thesis: for E being Element of S
for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds
f to_power k is_measurable_on E
let E be Element of S; ::_thesis: for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds
f to_power k is_measurable_on E
let f be PartFunc of X,REAL; ::_thesis: ( f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E implies f to_power k is_measurable_on E )
reconsider k1 = k as Real by XREAL_0:def_1;
assume that
A1: f is nonnegative and
A2: 0 <= k and
A3: E c= dom f and
A4: f is_measurable_on E ; ::_thesis: f to_power k is_measurable_on E
A5: dom (f to_power k) = dom f by Def4;
percases ( k = 0 or k > 0 ) by A2;
supposeA6: k = 0 ; ::_thesis: f to_power k is_measurable_on E
A7: E c= dom (f to_power k) by A3, Def4;
now__::_thesis:_for_r_being_real_number_holds_E_/\_(less_dom_((f_to_power_k),r))_in_S
let r be real number ; ::_thesis: E /\ (less_dom ((f to_power k),b1)) in S
reconsider r1 = r as Real by XREAL_0:def_1;
percases ( r <= 1 or 1 < r ) ;
supposeA8: r <= 1 ; ::_thesis: E /\ (less_dom ((f to_power k),b1)) in S
now__::_thesis:_for_x_being_set_st_x_in_E_holds_
x_in_great_eq_dom_((f_to_power_k),r1)
let x be set ; ::_thesis: ( x in E implies x in great_eq_dom ((f to_power k),r1) )
assume A9: x in E ; ::_thesis: x in great_eq_dom ((f to_power k),r1)
then (f to_power k) . x = (f . x) to_power k by A3, A5, Def4;
then r <= (f to_power k) . x by A6, A8, POWER:24;
hence x in great_eq_dom ((f to_power k),r1) by A3, A5, A9, MESFUNC6:6; ::_thesis: verum
end;
then E c= great_eq_dom ((f to_power k),r) by TARSKI:def_3;
then E /\ (great_eq_dom ((f to_power k),r)) = E by XBOOLE_1:28;
then E /\ (less_dom ((f to_power k),r1)) = E \ E by A7, Th28;
hence E /\ (less_dom ((f to_power k),r)) in S ; ::_thesis: verum
end;
supposeA10: 1 < r ; ::_thesis: E /\ (less_dom ((f to_power k),b1)) in S
now__::_thesis:_for_x_being_set_st_x_in_E_holds_
x_in_less_dom_((f_to_power_k),r)
let x be set ; ::_thesis: ( x in E implies x in less_dom ((f to_power k),r) )
assume A11: x in E ; ::_thesis: x in less_dom ((f to_power k),r)
then (f to_power k) . x = (f . x) to_power k by A3, A5, Def4;
then (f to_power k) . x < r by A6, A10, POWER:24;
hence x in less_dom ((f to_power k),r) by A3, A5, A11, MESFUNC6:3; ::_thesis: verum
end;
then E c= less_dom ((f to_power k),r) by TARSKI:def_3;
then E /\ (less_dom ((f to_power k),r)) = E by XBOOLE_1:28;
hence E /\ (less_dom ((f to_power k),r)) in S ; ::_thesis: verum
end;
end;
end;
hence f to_power k is_measurable_on E by MESFUNC6:12; ::_thesis: verum
end;
supposeA12: k > 0 ; ::_thesis: f to_power k is_measurable_on E
for r being real number holds E /\ (great_eq_dom ((f to_power k),r)) in S
proof
let r be real number ; ::_thesis: E /\ (great_eq_dom ((f to_power k),r)) in S
reconsider r1 = r as Real by XREAL_0:def_1;
percases ( r1 <= 0 or 0 < r1 ) ;
supposeA13: r1 <= 0 ; ::_thesis: E /\ (great_eq_dom ((f to_power k),r)) in S
now__::_thesis:_for_x_being_set_st_x_in_E_holds_
x_in_great_eq_dom_((f_to_power_k),r1)
let x be set ; ::_thesis: ( x in E implies x in great_eq_dom ((f to_power k),r1) )
assume x in E ; ::_thesis: x in great_eq_dom ((f to_power k),r1)
then x in dom f by A3;
then A14: x in dom (f to_power k) by Def4;
0 <= (f to_power k) . x by A1, A12, MESFUNC6:51;
hence x in great_eq_dom ((f to_power k),r1) by A13, A14, MESFUNC6:6; ::_thesis: verum
end;
then E c= great_eq_dom ((f to_power k),r) by TARSKI:def_3;
then E /\ (great_eq_dom ((f to_power k),r)) = E by XBOOLE_1:28;
hence E /\ (great_eq_dom ((f to_power k),r)) in S ; ::_thesis: verum
end;
supposeA15: 0 < r1 ; ::_thesis: E /\ (great_eq_dom ((f to_power k),r)) in S
A16: now__::_thesis:_for_x_being_set_st_x_in_great_eq_dom_(f,(r1_to_power_(1_/_k)))_holds_
x_in_great_eq_dom_((f_to_power_k),r1)
set R = r to_power (1 / k);
let x be set ; ::_thesis: ( x in great_eq_dom (f,(r1 to_power (1 / k))) implies x in great_eq_dom ((f to_power k),r1) )
A17: 0 < r to_power (1 / k) by A15, POWER:34;
assume A18: x in great_eq_dom (f,(r1 to_power (1 / k))) ; ::_thesis: x in great_eq_dom ((f to_power k),r1)
then A19: x in dom (f to_power k) by A5, MESFUNC6:6;
(r to_power (1 / k)) to_power k = r to_power ((1 / k) * k) by A15, POWER:33;
then A20: (r to_power (1 / k)) to_power k = r to_power 1 by A12, XCMPLX_1:87;
ex y being Real st
( y = f . x & r1 to_power (1 / k) <= y ) by A18, MESFUNC6:6;
then r1 to_power 1 <= (f . x) to_power k1 by A12, A17, A20, HOLDER_1:3;
then r <= (f . x) to_power k by POWER:25;
then r <= (f to_power k) . x by A19, Def4;
hence x in great_eq_dom ((f to_power k),r1) by A19, MESFUNC6:6; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_great_eq_dom_((f_to_power_k),r1)_holds_
x_in_great_eq_dom_(f,(r1_to_power_(1_/_k)))
let x be set ; ::_thesis: ( x in great_eq_dom ((f to_power k),r1) implies x in great_eq_dom (f,(r1 to_power (1 / k))) )
assume A21: x in great_eq_dom ((f to_power k),r1) ; ::_thesis: x in great_eq_dom (f,(r1 to_power (1 / k)))
then A22: x in dom (f to_power k) by MESFUNC6:6;
0 <= f . x by A1, MESFUNC6:51;
then ((f . x) to_power k1) to_power (1 / k1) = (f . x) to_power ((k1 * 1) / k1) by A12, HOLDER_1:2;
then ((f . x) to_power k1) to_power (1 / k1) = (f . x) to_power 1 by A12, XCMPLX_1:87;
then A23: ((f . x) to_power k) to_power (1 / k) = f . x by POWER:25;
ex y2 being Real st
( y2 = (f to_power k) . x & r1 <= y2 ) by A21, MESFUNC6:6;
then r <= (f . x) to_power k by A22, Def4;
then r to_power (1 / k1) <= ((f . x) to_power k1) to_power (1 / k1) by A12, A15, HOLDER_1:3;
hence x in great_eq_dom (f,(r1 to_power (1 / k))) by A5, A22, A23, MESFUNC6:6; ::_thesis: verum
end;
then E /\ (great_eq_dom ((f to_power k),r1)) = E /\ (great_eq_dom (f,(r1 to_power (1 / k)))) by A16, TARSKI:1;
hence E /\ (great_eq_dom ((f to_power k),r)) in S by A3, A4, MESFUNC6:13; ::_thesis: verum
end;
end;
end;
hence f to_power k is_measurable_on E by A3, A5, MESFUNC6:13; ::_thesis: verum
end;
end;
end;
theorem Th30: :: MESFUN6C:30
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A & A c= dom f holds
|.f.| is_measurable_on A
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A & A c= dom f holds
|.f.| is_measurable_on A
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX
for A being Element of S st f is_measurable_on A & A c= dom f holds
|.f.| is_measurable_on A
let f be PartFunc of X,COMPLEX; ::_thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds
|.f.| is_measurable_on A
let A be Element of S; ::_thesis: ( f is_measurable_on A & A c= dom f implies |.f.| is_measurable_on A )
assume that
A1: f is_measurable_on A and
A2: A c= dom f ; ::_thesis: |.f.| is_measurable_on A
A3: dom (Im f) = dom f by COMSEQ_3:def_4;
A4: now__::_thesis:_for_x_being_set_st_x_in_dom_|.(Im_f).|_holds_
0_<=_|.(Im_f).|_._x
let x be set ; ::_thesis: ( x in dom |.(Im f).| implies 0 <= |.(Im f).| . x )
assume x in dom |.(Im f).| ; ::_thesis: 0 <= |.(Im f).| . x
then |.(Im f).| . x = |.((Im f) . x).| by VALUED_1:def_11;
hence 0 <= |.(Im f).| . x by COMPLEX1:46; ::_thesis: verum
end;
then A5: |.(Im f).| to_power 2 is nonnegative by Th26, MESFUNC6:52;
A6: dom |.(Im f).| = dom (Im f) by VALUED_1:def_11;
then A7: dom (|.(Im f).| to_power 2) = dom f by A3, Def4;
Im f is_measurable_on A by A1, Def1;
then |.(Im f).| is_measurable_on A by A2, A3, MESFUNC6:48;
then A8: |.(Im f).| to_power 2 is_measurable_on A by A2, A6, A3, A4, Th29, MESFUNC6:52;
A9: dom (Re f) = dom f by COMSEQ_3:def_3;
A10: now__::_thesis:_for_x_being_set_st_x_in_dom_|.(Re_f).|_holds_
0_<=_|.(Re_f).|_._x
let x be set ; ::_thesis: ( x in dom |.(Re f).| implies 0 <= |.(Re f).| . x )
A11: 0 <= |.((Re f) . x).| by COMPLEX1:46;
assume x in dom |.(Re f).| ; ::_thesis: 0 <= |.(Re f).| . x
hence 0 <= |.(Re f).| . x by A11, VALUED_1:def_11; ::_thesis: verum
end;
then A12: |.(Re f).| to_power 2 is nonnegative by Th26, MESFUNC6:52;
set F = (|.(Re f).| to_power 2) + (|.(Im f).| to_power 2);
A13: dom |.f.| = dom f by VALUED_1:def_11;
A14: dom |.(Re f).| = dom (Re f) by VALUED_1:def_11;
then A15: dom (|.(Re f).| to_power 2) = dom f by A9, Def4;
A16: dom ((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) = (dom (|.(Re f).| to_power 2)) /\ (dom (|.(Im f).| to_power 2)) by VALUED_1:def_1;
then A17: dom |.f.| = dom (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) by A13, A15, A7, Def4;
now__::_thesis:_for_x_being_set_st_x_in_dom_|.f.|_holds_
|.f.|_._x_=_(((|.(Re_f).|_to_power_2)_+_(|.(Im_f).|_to_power_2))_to_power_(1_/_2))_._x
let x be set ; ::_thesis: ( x in dom |.f.| implies |.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x )
assume A18: x in dom |.f.| ; ::_thesis: |.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x
then (|.(Re f).| to_power 2) . x = (|.(Re f).| . x) to_power 2 by A13, A15, Def4;
then (|.(Re f).| to_power 2) . x = |.((Re f) . x).| to_power 2 by A14, A13, A9, A18, VALUED_1:def_11;
then (|.(Re f).| to_power 2) . x = |.(Re (f . x)).| to_power 2 by A13, A9, A18, COMSEQ_3:def_3;
then (|.(Re f).| to_power 2) . x = |.(Re (f . x)).| ^2 by POWER:46;
then A19: (|.(Re f).| to_power 2) . x = (Re (f . x)) ^2 by COMPLEX1:75;
(|.(Im f).| to_power 2) . x = (|.(Im f).| . x) to_power 2 by A13, A7, A18, Def4;
then (|.(Im f).| to_power 2) . x = |.((Im f) . x).| to_power 2 by A6, A13, A3, A18, VALUED_1:def_11;
then (|.(Im f).| to_power 2) . x = |.(Im (f . x)).| to_power 2 by A13, A3, A18, COMSEQ_3:def_4;
then (|.(Im f).| to_power 2) . x = |.(Im (f . x)).| ^2 by POWER:46;
then A20: (|.(Im f).| to_power 2) . x = (Im (f . x)) ^2 by COMPLEX1:75;
(((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) . x) to_power (1 / 2) = sqrt (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) . x) by A12, A5, Th27, MESFUNC6:56
.= sqrt (((Re (f . x)) ^2) + ((Im (f . x)) ^2)) by A13, A16, A15, A7, A18, A19, A20, VALUED_1:def_1 ;
then (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x = |.(f . x).| by A17, A18, Def4;
hence |.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x by A18, VALUED_1:def_11; ::_thesis: verum
end;
then A21: |.f.| = ((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2) by A17, FUNCT_1:2;
Re f is_measurable_on A by A1, Def1;
then |.(Re f).| is_measurable_on A by A2, A9, MESFUNC6:48;
then |.(Re f).| to_power 2 is_measurable_on A by A2, A14, A9, A10, Th29, MESFUNC6:52;
then (|.(Re f).| to_power 2) + (|.(Im f).| to_power 2) is_measurable_on A by A8, MESFUNC6:26;
hence |.f.| is_measurable_on A by A2, A12, A5, A16, A15, A7, A21, Th29, MESFUNC6:56; ::_thesis: verum
end;
theorem Th31: :: MESFUN6C:31
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
let f be PartFunc of X,COMPLEX; ::_thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) implies ( f is_integrable_on M iff |.f.| is_integrable_on M ) )
A1: dom (|.(Re f).| + |.(Im f).|) = (dom |.(Re f).|) /\ (dom |.(Im f).|) by VALUED_1:def_1;
A2: dom |.(Re f).| = dom (Re f) by VALUED_1:def_11;
A3: dom |.(Im f).| = dom (Im f) by VALUED_1:def_11;
A4: dom |.f.| = dom f by VALUED_1:def_11;
assume ex A being Element of S st
( A = dom f & f is_measurable_on A ) ; ::_thesis: ( f is_integrable_on M iff |.f.| is_integrable_on M )
then consider A being Element of S such that
A5: A = dom f and
A6: f is_measurable_on A ;
A7: dom (Re f) = A by A5, COMSEQ_3:def_3;
A8: Im f is_measurable_on A by A6, Def1;
A9: Re f is_measurable_on A by A6, Def1;
A10: dom (Im f) = A by A5, COMSEQ_3:def_4;
A11: |.f.| is_measurable_on A by A5, A6, Th30;
hereby ::_thesis: ( |.f.| is_integrable_on M implies f is_integrable_on M )
A12: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_|.f.|_holds_
|.(|.f.|_._x).|_<=_(|.(Re_f).|_+_|.(Im_f).|)_._x
let x be Element of X; ::_thesis: ( x in dom |.f.| implies |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x )
assume A13: x in dom |.f.| ; ::_thesis: |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x
then A14: |.f.| . x = |.(f . x).| by VALUED_1:def_11;
A15: |.((Im f) . x).| = |.(Im f).| . x by A5, A10, A3, A4, A13, VALUED_1:def_11;
A16: |.((Re f) . x).| = |.(Re f).| . x by A5, A7, A2, A4, A13, VALUED_1:def_11;
A17: (Im f) . x = Im (f . x) by A5, A10, A4, A13, COMSEQ_3:def_4;
A18: (Re f) . x = Re (f . x) by A5, A7, A4, A13, COMSEQ_3:def_3;
(|.(Re f).| + |.(Im f).|) . x = (|.(Re f).| . x) + (|.(Im f).| . x) by A5, A7, A10, A1, A2, A3, A4, A13, VALUED_1:def_1;
hence |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x by A18, A17, A14, A16, A15, COMPLEX1:78; ::_thesis: verum
end;
assume A19: f is_integrable_on M ; ::_thesis: |.f.| is_integrable_on M
then Im f is_integrable_on M by Def2;
then A20: |.(Im f).| is_integrable_on M by A10, A8, MESFUNC6:94;
Re f is_integrable_on M by A19, Def2;
then |.(Re f).| is_integrable_on M by A7, A9, MESFUNC6:94;
then |.(Re f).| + |.(Im f).| is_integrable_on M by A20, MESFUNC6:100;
hence |.f.| is_integrable_on M by A5, A7, A10, A1, A2, A3, A4, A11, A12, MESFUNC6:96; ::_thesis: verum
end;
hereby ::_thesis: verum
assume A21: |.f.| is_integrable_on M ; ::_thesis: f is_integrable_on M
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(Im_f)_holds_
|.((Im_f)_._x).|_<=_|.f.|_._x
let x be Element of X; ::_thesis: ( x in dom (Im f) implies |.((Im f) . x).| <= |.f.| . x )
A22: |.(Im (f . x)).| <= |.(f . x).| by COMPLEX1:79;
assume A23: x in dom (Im f) ; ::_thesis: |.((Im f) . x).| <= |.f.| . x
then |.f.| . x = |.(f . x).| by A5, A10, A4, VALUED_1:def_11;
hence |.((Im f) . x).| <= |.f.| . x by A23, A22, COMSEQ_3:def_4; ::_thesis: verum
end;
then A24: Im f is_integrable_on M by A5, A10, A8, A4, A21, MESFUNC6:96;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(Re_f)_holds_
|.((Re_f)_._x).|_<=_|.f.|_._x
let x be Element of X; ::_thesis: ( x in dom (Re f) implies |.((Re f) . x).| <= |.f.| . x )
A25: |.(Re (f . x)).| <= |.(f . x).| by COMPLEX1:79;
assume A26: x in dom (Re f) ; ::_thesis: |.((Re f) . x).| <= |.f.| . x
then |.f.| . x = |.(f . x).| by A5, A7, A4, VALUED_1:def_11;
hence |.((Re f) . x).| <= |.f.| . x by A26, A25, COMSEQ_3:def_3; ::_thesis: verum
end;
then Re f is_integrable_on M by A5, A7, A9, A4, A21, MESFUNC6:96;
hence f is_integrable_on M by A24, Def2; ::_thesis: verum
end;
end;
theorem :: MESFUN6C:32
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
dom (f + g) in S
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
dom (f + g) in S
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
dom (f + g) in S
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
dom (f + g) in S
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies dom (f + g) in S )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; ::_thesis: dom (f + g) in S
A3: Re g is_integrable_on M by A2, Def2;
A4: Im g is_integrable_on M by A2, Def2;
Im f is_integrable_on M by A1, Def2;
then dom ((Im f) + (Im g)) in S by A4, MESFUNC6:99;
then A5: dom (Im (f + g)) in S by Th5;
Re f is_integrable_on M by A1, Def2;
then dom ((Re f) + (Re g)) in S by A3, MESFUNC6:99;
then A6: dom (Re (f + g)) in S by Th5;
dom (** (#) (Im (f + g))) = dom (Im (f + g)) by VALUED_1:def_5;
then dom ((Re (f + g)) + (** (#) (Im (f + g)))) = (dom (Re (f + g))) /\ (dom (Im (f + g))) by VALUED_1:def_1;
then dom ((Re (f + g)) + (** (#) (Im (f + g)))) in S by A6, A5, FINSUB_1:def_2;
hence dom (f + g) in S by Th8; ::_thesis: verum
end;
theorem Th33: :: MESFUN6C:33
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
f + g is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
f + g is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
f + g is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
f + g is_integrable_on M
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies f + g is_integrable_on M )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; ::_thesis: f + g is_integrable_on M
A3: Im g is_integrable_on M by A2, Def2;
Im f is_integrable_on M by A1, Def2;
then (Im f) + (Im g) is_integrable_on M by A3, MESFUNC6:100;
then A4: Im (f + g) is_integrable_on M by Th5;
A5: Re g is_integrable_on M by A2, Def2;
Re f is_integrable_on M by A1, Def2;
then (Re f) + (Re g) is_integrable_on M by A5, MESFUNC6:100;
then Re (f + g) is_integrable_on M by Th5;
hence f + g is_integrable_on M by A4, Def2; ::_thesis: verum
end;
theorem Th34: :: MESFUN6C:34
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
f - g is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
f - g is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
f - g is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
f - g is_integrable_on M
let f, g be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies f - g is_integrable_on M )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; ::_thesis: f - g is_integrable_on M
R_EAL g is_integrable_on M by A2, MESFUNC6:def_4;
then (- 1) (#) (R_EAL g) is_integrable_on M by MESFUNC5:110;
then - (R_EAL g) is_integrable_on M by MESFUNC2:9;
then A3: R_EAL (- g) is_integrable_on M by MESFUNC6:28;
R_EAL f is_integrable_on M by A1, MESFUNC6:def_4;
then (R_EAL f) + (R_EAL (- g)) is_integrable_on M by A3, MESFUNC5:108;
then R_EAL (f - g) is_integrable_on M by MESFUNC6:23;
hence f - g is_integrable_on M by MESFUNC6:def_4; ::_thesis: verum
end;
theorem :: MESFUN6C:35
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
f - g is_integrable_on M
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
f - g is_integrable_on M
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
f - g is_integrable_on M
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
f - g is_integrable_on M
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies f - g is_integrable_on M )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; ::_thesis: f - g is_integrable_on M
A3: Im g is_integrable_on M by A2, Def2;
Im f is_integrable_on M by A1, Def2;
then (Im f) - (Im g) is_integrable_on M by A3, Th34;
then A4: Im (f - g) is_integrable_on M by Th6;
A5: Re g is_integrable_on M by A2, Def2;
Re f is_integrable_on M by A1, Def2;
then (Re f) - (Re g) is_integrable_on M by A5, Th34;
then Re (f - g) is_integrable_on M by Th6;
hence f - g is_integrable_on M by A4, Def2; ::_thesis: verum
end;
theorem Th36: :: MESFUN6C:36
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; ::_thesis: ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
A3: Re g is_integrable_on M by A2, Def2;
Re f is_integrable_on M by A1, Def2;
then consider E being Element of S such that
A4: E = (dom (Re f)) /\ (dom (Re g)) and
A5: Integral (M,((Re f) + (Re g))) = (Integral (M,((Re f) | E))) + (Integral (M,((Re g) | E))) by A3, MESFUNC6:101;
A6: f | E is_integrable_on M by A1, Th23;
then A7: Re (f | E) is_integrable_on M by Def2;
then A8: Integral (M,(Re (f | E))) < +infty by MESFUNC6:90;
A9: Im (f | E) is_integrable_on M by A6, Def2;
then A10: -infty < Integral (M,(Im (f | E))) by MESFUNC6:90;
A11: Integral (M,(Im (f | E))) < +infty by A9, MESFUNC6:90;
-infty < Integral (M,(Re (f | E))) by A7, MESFUNC6:90;
then reconsider R1 = Integral (M,(Re (f | E))), I1 = Integral (M,(Im (f | E))) as Real by A8, A10, A11, XXREAL_0:14;
A12: dom f = dom (Re f) by COMSEQ_3:def_3;
A13: Im g is_integrable_on M by A2, Def2;
Im f is_integrable_on M by A1, Def2;
then A14: ex Ei being Element of S st
( Ei = (dom (Im f)) /\ (dom (Im g)) & Integral (M,((Im f) + (Im g))) = (Integral (M,((Im f) | Ei))) + (Integral (M,((Im g) | Ei))) ) by A13, MESFUNC6:101;
A15: Integral (M,((Im f) + (Im g))) = Integral (M,(Im (f + g))) by Th5;
A16: f + g is_integrable_on M by A1, A2, Th33;
then A17: Re (f + g) is_integrable_on M by Def2;
then A18: Integral (M,(Re (f + g))) < +infty by MESFUNC6:90;
A19: Im (f + g) is_integrable_on M by A16, Def2;
then A20: -infty < Integral (M,(Im (f + g))) by MESFUNC6:90;
A21: Integral (M,(Im (f + g))) < +infty by A19, MESFUNC6:90;
-infty < Integral (M,(Re (f + g))) by A17, MESFUNC6:90;
then reconsider R = Integral (M,(Re (f + g))), I = Integral (M,(Im (f + g))) as Real by A18, A20, A21, XXREAL_0:14;
A22: Integral (M,(f + g)) = R + (I * **) by A16, Def3;
A23: dom g = dom (Im g) by COMSEQ_3:def_4;
A24: g | E is_integrable_on M by A2, Th23;
then A25: Re (g | E) is_integrable_on M by Def2;
then A26: Integral (M,(Re (g | E))) < +infty by MESFUNC6:90;
A27: Im (g | E) is_integrable_on M by A24, Def2;
then A28: -infty < Integral (M,(Im (g | E))) by MESFUNC6:90;
A29: Integral (M,(Im (g | E))) < +infty by A27, MESFUNC6:90;
-infty < Integral (M,(Re (g | E))) by A25, MESFUNC6:90;
then reconsider R2 = Integral (M,(Re (g | E))), I2 = Integral (M,(Im (g | E))) as Real by A26, A28, A29, XXREAL_0:14;
A30: dom g = dom (Re g) by COMSEQ_3:def_3;
Integral (M,((Re f) + (Re g))) = Integral (M,(Re (f + g))) by Th5;
then Integral (M,(Re (f + g))) = (Integral (M,(Re (f | E)))) + (Integral (M,((Re g) | E))) by A5, Th7
.= (Integral (M,(Re (f | E)))) + (Integral (M,(Re (g | E)))) by Th7 ;
then A31: R = R1 + R2 by SUPINF_2:1;
dom f = dom (Im f) by COMSEQ_3:def_4;
then Integral (M,(Im (f + g))) = (Integral (M,(Im (f | E)))) + (Integral (M,((Im g) | E))) by A4, A12, A30, A23, A14, A15, Th7;
then R_EAL I = (R_EAL I1) + (R_EAL I2) by Th7;
then I = I1 + I2 by SUPINF_2:1;
then Integral (M,(f + g)) = (R1 + (I1 * **)) + (R2 + (I2 * **)) by A31, A22;
then Integral (M,(f + g)) = (Integral (M,(f | E))) + (R2 + (I2 * **)) by A6, Def3;
then Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) by A24, Def3;
hence ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) by A4, A12, A30; ::_thesis: verum
end;
theorem :: MESFUN6C:37
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )
let f, g be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; ::_thesis: ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )
R_EAL g is_integrable_on M by A2, MESFUNC6:def_4;
then (- 1) (#) (R_EAL g) is_integrable_on M by MESFUNC5:110;
then - (R_EAL g) is_integrable_on M by MESFUNC2:9;
then A3: R_EAL (- g) is_integrable_on M by MESFUNC6:28;
R_EAL f is_integrable_on M by A1, MESFUNC6:def_4;
then consider E being Element of S such that
A4: E = (dom (R_EAL f)) /\ (dom (R_EAL (- g))) and
A5: Integral (M,((R_EAL f) + (R_EAL (- g)))) = (Integral (M,((R_EAL f) | E))) + (Integral (M,((R_EAL (- g)) | E))) by A3, MESFUNC5:109;
take E ; ::_thesis: ( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) )
dom (R_EAL (- g)) = dom (- (R_EAL g)) by MESFUNC6:28;
hence ( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) by A4, A5, MESFUNC1:def_7, MESFUNC6:23; ::_thesis: verum
end;
theorem Th38: :: MESFUN6C:38
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for r being Real st f is_integrable_on M holds
( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for r being Real st f is_integrable_on M holds
( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for r being Real st f is_integrable_on M holds
( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX
for r being Real st f is_integrable_on M holds
( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )
let f be PartFunc of X,COMPLEX; ::_thesis: for r being Real st f is_integrable_on M holds
( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )
let r be Real; ::_thesis: ( f is_integrable_on M implies ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) ) )
A1: Integral (M,(r (#) (Re f))) = Integral (M,(Re (r (#) f))) by Th2;
A2: Integral (M,(r (#) (Im f))) = Integral (M,(Im (r (#) f))) by Th2;
assume A3: f is_integrable_on M ; ::_thesis: ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )
then A4: Re f is_integrable_on M by Def2;
then A5: Integral (M,(Re f)) < +infty by MESFUNC6:90;
r (#) (Re f) is_integrable_on M by A4, MESFUNC6:102;
then A6: Re (r (#) f) is_integrable_on M by Th2;
then A7: Integral (M,(Re (r (#) f))) < +infty by MESFUNC6:90;
A8: Im f is_integrable_on M by A3, Def2;
then A9: -infty < Integral (M,(Im f)) by MESFUNC6:90;
A10: Integral (M,(Im f)) < +infty by A8, MESFUNC6:90;
-infty < Integral (M,(Re f)) by A4, MESFUNC6:90;
then reconsider R1 = Integral (M,(Re f)), I1 = Integral (M,(Im f)) as Real by A5, A9, A10, XXREAL_0:14;
A11: (R_EAL r) * (R_EAL R1) = r * R1 by Th1;
A12: (R_EAL r) * (R_EAL I1) = r * I1 by Th1;
r (#) (Im f) is_integrable_on M by A8, MESFUNC6:102;
then A13: Im (r (#) f) is_integrable_on M by Th2;
then A14: -infty < Integral (M,(Im (r (#) f))) by MESFUNC6:90;
A15: Integral (M,(Im (r (#) f))) < +infty by A13, MESFUNC6:90;
-infty < Integral (M,(Re (r (#) f))) by A6, MESFUNC6:90;
then reconsider R2 = Integral (M,(Re (r (#) f))), I2 = Integral (M,(Im (r (#) f))) as Real by A7, A14, A15, XXREAL_0:14;
A16: Integral (M,(r (#) (Im f))) = (R_EAL r) * (Integral (M,(Im f))) by A8, MESFUNC6:102;
A17: r (#) f is_integrable_on M by A6, A13, Def2;
Integral (M,(r (#) (Re f))) = (R_EAL r) * (Integral (M,(Re f))) by A4, MESFUNC6:102;
then R2 + (I2 * **) = r * (R1 + (I1 * **)) by A16, A1, A2, A11, A12;
then Integral (M,(r (#) f)) = r * (R1 + (I1 * **)) by A17, Def3;
hence ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) ) by A3, A6, A13, Def2, Def3; ::_thesis: verum
end;
theorem Th39: :: MESFUN6C:39
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
( ** (#) f is_integrable_on M & Integral (M,(** (#) f)) = ** * (Integral (M,f)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
( ** (#) f is_integrable_on M & Integral (M,(** (#) f)) = ** * (Integral (M,f)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
( ** (#) f is_integrable_on M & Integral (M,(** (#) f)) = ** * (Integral (M,f)) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
( ** (#) f is_integrable_on M & Integral (M,(** (#) f)) = ** * (Integral (M,f)) )
let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M implies ( ** (#) f is_integrable_on M & Integral (M,(** (#) f)) = ** * (Integral (M,f)) ) )
A1: Re (** (#) f) = - (Im f) by Th4;
assume A2: f is_integrable_on M ; ::_thesis: ( ** (#) f is_integrable_on M & Integral (M,(** (#) f)) = ** * (Integral (M,f)) )
then A3: Im f is_integrable_on M by Def2;
A4: Im (** (#) f) = Re f by Th4;
then A5: Im (** (#) f) is_integrable_on M by A2, Def2;
- (Im f) = (- 1) (#) (Im f) ;
then Re (** (#) f) is_integrable_on M by A3, A1, MESFUNC6:102;
hence ** (#) f is_integrable_on M by A5, Def2; ::_thesis: Integral (M,(** (#) f)) = ** * (Integral (M,f))
then consider R1, I1 being Real such that
A6: R1 = Integral (M,(Re (** (#) f))) and
A7: I1 = Integral (M,(Im (** (#) f))) and
A8: Integral (M,(** (#) f)) = R1 + (I1 * **) by Def3;
consider R, I being Real such that
A9: R = Integral (M,(Re f)) and
A10: I = Integral (M,(Im f)) and
A11: Integral (M,f) = R + (I * **) by A2, Def3;
R1 = (R_EAL (- 1)) * (R_EAL I) by A3, A1, A10, A6, MESFUNC6:102
.= (- 1) * I by EXTREAL1:5 ;
hence Integral (M,(** (#) f)) = ** * (Integral (M,f)) by A4, A9, A11, A7, A8; ::_thesis: verum
end;
theorem Th40: :: MESFUN6C:40
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for c being complex number st f is_integrable_on M holds
( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for c being complex number st f is_integrable_on M holds
( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for c being complex number st f is_integrable_on M holds
( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX
for c being complex number st f is_integrable_on M holds
( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) )
let f be PartFunc of X,COMPLEX; ::_thesis: for c being complex number st f is_integrable_on M holds
( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) )
let c be complex number ; ::_thesis: ( f is_integrable_on M implies ( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) ) )
A1: c = (Re c) + ((Im c) * **) by COMPLEX1:13;
A2: dom (** (#) f) = dom f by VALUED_1:def_5;
assume A3: f is_integrable_on M ; ::_thesis: ( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) )
then A4: Integral (M,((Re c) (#) f)) = (Re c) * (Integral (M,f)) by Th38;
A5: ** (#) f is_integrable_on M by A3, Th39;
then A6: (Im c) (#) (** (#) f) is_integrable_on M by Th38;
A7: (Re c) (#) f is_integrable_on M by A3, Th38;
then consider E being Element of S such that
A8: E = (dom ((Re c) (#) f)) /\ (dom ((Im c) (#) (** (#) f))) and
A9: Integral (M,(((Re c) (#) f) + ((Im c) (#) (** (#) f)))) = (Integral (M,(((Re c) (#) f) | E))) + (Integral (M,(((Im c) (#) (** (#) f)) | E))) by A6, Th36;
A10: dom (c (#) f) = dom f by VALUED_1:def_5;
A11: Integral (M,((Im c) (#) (** (#) f))) = (Im c) * (Integral (M,(** (#) f))) by A5, Th38;
A12: dom ((Re c) (#) f) = dom f by VALUED_1:def_5;
A13: dom ((Im c) (#) (** (#) f)) = dom (** (#) f) by VALUED_1:def_5;
A14: dom (((Re c) (#) f) + ((Im c) (#) (** (#) f))) = (dom ((Re c) (#) f)) /\ (dom ((Im c) (#) (** (#) f))) by VALUED_1:def_1;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(c_(#)_f)_holds_
(c_(#)_f)_._x_=_(((Re_c)_(#)_f)_+_((Im_c)_(#)_(**_(#)_f)))_._x
let x be Element of X; ::_thesis: ( x in dom (c (#) f) implies (c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) (** (#) f))) . x )
assume A15: x in dom (c (#) f) ; ::_thesis: (c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) (** (#) f))) . x
then A16: (c (#) f) . x = c * (f . x) by VALUED_1:def_5;
A17: ((Im c) (#) (** (#) f)) . x = (Im c) * ((** (#) f) . x) by A10, A2, A13, A15, VALUED_1:def_5;
A18: ((Re c) (#) f) . x = (Re c) * (f . x) by A10, A12, A15, VALUED_1:def_5;
A19: (** (#) f) . x = ** * (f . x) by A10, A2, A15, VALUED_1:def_5;
(((Re c) (#) f) + ((Im c) (#) (** (#) f))) . x = (((Re c) (#) f) . x) + (((Im c) (#) (** (#) f)) . x) by A10, A12, A2, A13, A14, A15, VALUED_1:def_1;
hence (c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) (** (#) f))) . x by A1, A16, A18, A17, A19; ::_thesis: verum
end;
then A20: c (#) f = ((Re c) (#) f) + ((Im c) (#) (** (#) f)) by A10, A12, A2, A13, A14, PARTFUN1:5;
hence c (#) f is_integrable_on M by A7, A6, Th33; ::_thesis: Integral (M,(c (#) f)) = c * (Integral (M,f))
A21: Integral (M,(** (#) f)) = ** * (Integral (M,f)) by A3, Th39;
((Re c) (#) f) | E = (Re c) (#) f by A12, A2, A13, A8, RELAT_1:68;
hence Integral (M,(c (#) f)) = ((Re c) * (Integral (M,f))) + (((Im c) * **) * (Integral (M,f))) by A12, A2, A13, A20, A4, A21, A11, A8, A9, RELAT_1:68
.= c * (Integral (M,f)) by A1 ;
::_thesis: verum
end;
Lm2: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) = 0 holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) = 0 holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) = 0 holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) = 0 holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
let f be PartFunc of X,COMPLEX; ::_thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) = 0 implies |.(Integral (M,f)).| <= Integral (M,|.f.|) )
assume that
A1: ex A being Element of S st
( A = dom f & f is_measurable_on A ) and
A2: f is_integrable_on M and
A3: Integral (M,f) = 0 ; ::_thesis: |.(Integral (M,f)).| <= Integral (M,|.f.|)
A4: |.f.| is_integrable_on M by A1, A2, Th31;
consider R, I being Real such that
A5: R = Integral (M,(Re f)) and
I = Integral (M,(Im f)) and
A6: Integral (M,f) = R + (I * **) by A2, Def3;
R = 0 by A3, A6, COMPLEX1:4, COMPLEX1:12;
then A7: |.(Integral (M,(Re f))).| = 0 by A5, EXTREAL2:5;
Re f is_integrable_on M by A2, Def2;
then A8: |.(Integral (M,(Re f))).| <= Integral (M,|.(Re f).|) by MESFUNC6:95;
A9: dom |.f.| = dom f by VALUED_1:def_11;
consider A being Element of S such that
A10: A = dom f and
A11: f is_measurable_on A by A1;
A12: dom (Re f) = A by A10, COMSEQ_3:def_3;
A13: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(Re_f)_holds_
|.((Re_f)_._x).|_<=_|.f.|_._x
let x be Element of X; ::_thesis: ( x in dom (Re f) implies |.((Re f) . x).| <= |.f.| . x )
assume A14: x in dom (Re f) ; ::_thesis: |.((Re f) . x).| <= |.f.| . x
then A15: (Re f) . x = Re (f . x) by COMSEQ_3:def_3;
|.f.| . x = |.(f . x).| by A10, A12, A9, A14, VALUED_1:def_11;
hence |.((Re f) . x).| <= |.f.| . x by A15, COMPLEX1:79; ::_thesis: verum
end;
Re f is_measurable_on A by A11, Def1;
hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A3, A4, A8, A10, A12, A9, A13, A7, COMPLEX1:44, MESFUNC6:96; ::_thesis: verum
end;
theorem Th41: :: MESFUN6C:41
for X being non empty set
for f being PartFunc of X,REAL
for Y being set
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for Y being set
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let f be PartFunc of X,REAL; ::_thesis: for Y being set
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let Y be set ; ::_thesis: for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let r be Real; ::_thesis: (r (#) f) | Y = r (#) (f | Y)
A1: dom ((r (#) f) | Y) = (dom (r (#) f)) /\ Y by RELAT_1:61
.= (dom f) /\ Y by VALUED_1:def_5
.= dom (f | Y) by RELAT_1:61 ;
A2: dom ((r (#) f) | Y) c= dom (r (#) f) by RELAT_1:60;
A3: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((r_(#)_f)_|_Y)_holds_
(r_(#)_(f_|_Y))_._x_=_((r_(#)_f)_|_Y)_._x
let x be Element of X; ::_thesis: ( x in dom ((r (#) f) | Y) implies (r (#) (f | Y)) . x = ((r (#) f) | Y) . x )
assume A4: x in dom ((r (#) f) | Y) ; ::_thesis: (r (#) (f | Y)) . x = ((r (#) f) | Y) . x
then x in dom (r (#) (f | Y)) by A1, VALUED_1:def_5;
then (r (#) (f | Y)) . x = r * ((f | Y) . x) by VALUED_1:def_5;
then (r (#) (f | Y)) . x = r * (f . x) by A1, A4, FUNCT_1:47;
then (r (#) (f | Y)) . x = (r (#) f) . x by A2, A4, VALUED_1:def_5;
hence (r (#) (f | Y)) . x = ((r (#) f) | Y) . x by A4, FUNCT_1:47; ::_thesis: verum
end;
dom ((r (#) f) | Y) = dom (r (#) (f | Y)) by A1, VALUED_1:def_5;
hence (r (#) f) | Y = r (#) (f | Y) by A3, PARTFUN1:5; ::_thesis: verum
end;
theorem Th42: :: MESFUN6C:42
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex A being Element of S st
( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex A being Element of S st
( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex A being Element of S st
( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st ex A being Element of S st
( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
let f, g be PartFunc of X,REAL; ::_thesis: ( ex A being Element of S st
( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative implies ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) )
assume that
A1: ex A being Element of S st
( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) and
A2: f is_integrable_on M and
A3: g is_integrable_on M and
A4: g - f is nonnegative ; ::_thesis: ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
set h = (- 1) (#) f;
(- 1) (#) f is_integrable_on M by A2, MESFUNC6:102;
then consider E being Element of S such that
A5: E = (dom ((- 1) (#) f)) /\ (dom g) and
A6: Integral (M,(((- 1) (#) f) + g)) = (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E))) by A3, MESFUNC6:101;
A7: f | E is_integrable_on M by A2, MESFUNC6:91;
then A8: Integral (M,(f | E)) < +infty by MESFUNC6:90;
-infty < Integral (M,(f | E)) by A7, MESFUNC6:90;
then reconsider c1 = Integral (M,(f | E)) as Real by A8, XXREAL_0:14;
A9: (R_EAL (- 1)) * (Integral (M,(f | E))) = (- 1) * c1 by EXTREAL1:1;
A10: g | E is_integrable_on M by A3, MESFUNC6:91;
then A11: Integral (M,(g | E)) < +infty by MESFUNC6:90;
-infty < Integral (M,(g | E)) by A10, MESFUNC6:90;
then reconsider c2 = Integral (M,(g | E)) as Real by A11, XXREAL_0:14;
take E ; ::_thesis: ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) )
A12: ((- 1) (#) f) | E = (- 1) (#) (f | E) by Th41;
consider A being Element of S such that
A13: A = (dom f) /\ (dom g) and
A14: f is_measurable_on A and
A15: g is_measurable_on A by A1;
dom ((- 1) (#) f) = dom f by VALUED_1:def_5;
then A16: dom (((- 1) (#) f) + g) = A by A13, VALUED_1:def_1;
(- 1) (#) f is_measurable_on A by A13, A14, MESFUNC6:21, XBOOLE_1:17;
then 0 <= (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E))) by A4, A6, A15, A16, MESFUNC6:26, MESFUNC6:84;
then 0 <= ((R_EAL (- 1)) * (Integral (M,(f | E)))) + (Integral (M,(g | E))) by A7, A12, MESFUNC6:102;
then 0 <= (- c1) + c2 by A9, SUPINF_2:1;
then 0 + c1 <= ((- c1) + c2) + c1 by XREAL_1:6;
hence ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) by A5, VALUED_1:def_5; ::_thesis: verum
end;
Lm3: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) <> 0 holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) <> 0 holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) <> 0 holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) <> 0 holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
let f be PartFunc of X,COMPLEX; ::_thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) <> 0 implies |.(Integral (M,f)).| <= Integral (M,|.f.|) )
assume that
A1: ex A being Element of S st
( A = dom f & f is_measurable_on A ) and
A2: f is_integrable_on M and
A3: Integral (M,f) <> 0 ; ::_thesis: |.(Integral (M,f)).| <= Integral (M,|.f.|)
A4: |.f.| is_integrable_on M by A1, A2, Th31;
set a = Integral (M,f);
0 < |.(Integral (M,f)).| by A3, COMPLEX1:47;
then A5: |.(Integral (M,f)).| / |.(Integral (M,f)).| = 1 by XCMPLX_1:60;
set h = f (#) (|.f.| ");
set b = (Integral (M,f)) / |.(Integral (M,f)).|;
A6: dom |.f.| = dom f by VALUED_1:def_11;
|.((Integral (M,f)) / |.(Integral (M,f)).|).| * |.(((Integral (M,f)) / |.(Integral (M,f)).|) *').| = |.(((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *')).| by COMPLEX1:65;
then |.((Integral (M,f)) / |.(Integral (M,f)).|).| * |.(((Integral (M,f)) / |.(Integral (M,f)).|) *').| = |.(((Integral (M,f)) / |.(Integral (M,f)).|) * ((Integral (M,f)) / |.(Integral (M,f)).|)).| by COMPLEX1:69;
then A7: |.((Integral (M,f)) / |.(Integral (M,f)).|).| * |.(((Integral (M,f)) / |.(Integral (M,f)).|) *').| = |.((Integral (M,f)) / |.(Integral (M,f)).|).| * |.((Integral (M,f)) / |.(Integral (M,f)).|).| by COMPLEX1:65;
A8: f (#) (|.f.| ") = f /" |.f.| ;
then A9: dom (f (#) (|.f.| ")) = (dom f) /\ (dom |.f.|) by VALUED_1:16;
then A10: dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) = dom f by A6, VALUED_1:def_5;
then A11: dom (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) = (dom f) /\ (dom f) by A6, VALUED_1:def_4;
then A12: dom (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) = dom f by COMSEQ_3:def_3;
A13: dom (|.f.| (#) (f (#) (|.f.| "))) = (dom |.f.|) /\ (dom (f (#) (|.f.| "))) by VALUED_1:def_4;
then A14: dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) = dom f by A6, A9, VALUED_1:def_5;
now__::_thesis:_for_x_being_set_st_x_in_dom_((((Integral_(M,f))_/_|.(Integral_(M,f)).|)_*')_(#)_(|.f.|_(#)_(f_(#)_(|.f.|_"))))_holds_
((((Integral_(M,f))_/_|.(Integral_(M,f)).|)_*')_(#)_(|.f.|_(#)_(f_(#)_(|.f.|_"))))_._x_=_(|.f.|_(#)_((((Integral_(M,f))_/_|.(Integral_(M,f)).|)_*')_(#)_(f_(#)_(|.f.|_"))))_._x
let x be set ; ::_thesis: ( x in dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) implies ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x )
assume A15: x in dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) ; ::_thesis: ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x
then x in dom (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) by A6, A9, A13, A11, VALUED_1:def_5;
then (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = (|.f.| . x) * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by VALUED_1:def_4;
then (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = |.(f . x).| * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A14, A15, VALUED_1:def_11;
then A16: (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = ((((Integral (M,f)) / |.(Integral (M,f)).|) *') * ((f (#) (|.f.| ")) . x)) * |.(f . x).| by A14, A10, A15, VALUED_1:def_5;
((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (((Integral (M,f)) / |.(Integral (M,f)).|) *') * ((|.f.| (#) (f (#) (|.f.| "))) . x) by A15, VALUED_1:def_5;
then ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (((Integral (M,f)) / |.(Integral (M,f)).|) *') * ((|.f.| . x) * ((f (#) (|.f.| ")) . x)) by A6, A9, A13, A14, A15, VALUED_1:def_4;
then ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (((Integral (M,f)) / |.(Integral (M,f)).|) *') * (|.(f . x).| * ((f (#) (|.f.| ")) . x)) by A6, A14, A15, VALUED_1:def_11;
hence ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x by A16; ::_thesis: verum
end;
then A17: (((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| "))) = |.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) by A14, A11, FUNCT_1:2;
A18: |.((Integral (M,f)) / |.(Integral (M,f)).|).| = |.(Integral (M,f)).| / |.|.(Integral (M,f)).|.| by COMPLEX1:67;
now__::_thesis:_for_x_being_set_st_x_in_(dom_(Re_(|.f.|_(#)_((((Integral_(M,f))_/_|.(Integral_(M,f)).|)_*')_(#)_(f_(#)_(|.f.|_"))))))_/\_(dom_|.f.|)_holds_
(Re_(|.f.|_(#)_((((Integral_(M,f))_/_|.(Integral_(M,f)).|)_*')_(#)_(f_(#)_(|.f.|_")))))_._x_<=_|.f.|_._x
let x be set ; ::_thesis: ( x in (dom (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) /\ (dom |.f.|) implies (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . b1 <= |.f.| . b1 )
A19: (f (#) (|.f.| ")) . x = (f . x) / (|.f.| . x) by A8, VALUED_1:17;
assume A20: x in (dom (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) /\ (dom |.f.|) ; ::_thesis: (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . b1 <= |.f.| . b1
then |.f.| . x = |.(f . x).| by A6, A12, VALUED_1:def_11;
then A21: |.((f (#) (|.f.| ")) . x).| = |.(f . x).| / |.|.(f . x).|.| by A19, COMPLEX1:67;
percases ( f . x <> 0 or f . x = 0 ) ;
supposeA22: f . x <> 0 ; ::_thesis: (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . b1 <= |.f.| . b1
A23: Re ((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x) = (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . x by A6, A12, A20, COMSEQ_3:def_3;
(|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = (|.f.| . x) * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A11, A12, A20, VALUED_1:def_4;
then (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = |.(f . x).| * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A12, A20, VALUED_1:def_11;
then A24: |.((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x).| = |.|.(f . x).|.| * |.(((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x).| by COMPLEX1:65;
x in dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) by A9, A12, A20, VALUED_1:def_5;
then ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x = (((Integral (M,f)) / |.(Integral (M,f)).|) *') * ((f (#) (|.f.| ")) . x) by VALUED_1:def_5;
then A25: |.(((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x).| = |.(((Integral (M,f)) / |.(Integral (M,f)).|) *').| * |.((f (#) (|.f.| ")) . x).| by COMPLEX1:65;
0 < |.(f . x).| by A22, COMPLEX1:47;
then |.(f . x).| / |.(f . x).| = 1 by XCMPLX_1:60;
then Re ((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x) <= |.(f . x).| by A7, A18, A5, A21, A25, A24, COMPLEX1:54;
hence (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . x <= |.f.| . x by A6, A12, A20, A23, VALUED_1:def_11; ::_thesis: verum
end;
supposeA26: f . x = 0 ; ::_thesis: (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . b1 <= |.f.| . b1
(|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = (|.f.| . x) * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A11, A12, A20, VALUED_1:def_4;
then (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = |.(f . x).| * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A12, A20, VALUED_1:def_11;
then A27: |.((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x).| = |.|.(f . x).|.| * |.(((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x).| by COMPLEX1:65;
((Re (f . x)) ^2) + ((Im (f . x)) ^2) = 0 by A26, COMPLEX1:5;
then A28: Re ((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x) <= |.(f . x).| by A27, COMPLEX1:54, SQUARE_1:17;
Re ((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x) = (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . x by A6, A12, A20, COMSEQ_3:def_3;
hence (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . x <= |.f.| . x by A6, A12, A20, A28, VALUED_1:def_11; ::_thesis: verum
end;
end;
end;
then A29: |.f.| - (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) is nonnegative by MESFUNC6:58;
set F = Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))));
reconsider b1 = (Integral (M,f)) / |.(Integral (M,f)).| as Element of COMPLEX ;
A30: Re (b1 * (b1 *')) = ((Re b1) ^2) + ((Im b1) ^2) by COMPLEX1:40;
consider A being Element of S such that
A31: A = dom f and
A32: f is_measurable_on A by A1;
A33: |.f.| is_measurable_on A by A31, A32, Th30;
A34: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_=_(|.f.|_(#)_(f_(#)_(|.f.|_")))_._x
let x be set ; ::_thesis: ( x in dom f implies f . b1 = (|.f.| (#) (f (#) (|.f.| "))) . b1 )
A35: (f (#) (|.f.| ")) . x = (f . x) / (|.f.| . x) by A8, VALUED_1:17;
assume A36: x in dom f ; ::_thesis: f . b1 = (|.f.| (#) (f (#) (|.f.| "))) . b1
then A37: |.f.| . x = |.(f . x).| by A6, VALUED_1:def_11;
A38: (|.f.| (#) (f (#) (|.f.| "))) . x = (|.f.| . x) * ((f (#) (|.f.| ")) . x) by A6, A9, A13, A36, VALUED_1:def_4;
percases ( f . x <> 0 or f . x = 0 ) ;
suppose f . x <> 0 ; ::_thesis: f . b1 = (|.f.| (#) (f (#) (|.f.| "))) . b1
then 0 < |.(f . x).| by COMPLEX1:47;
hence f . x = (|.f.| (#) (f (#) (|.f.| "))) . x by A38, A37, A35, XCMPLX_1:87; ::_thesis: verum
end;
supposeA39: f . x = 0 ; ::_thesis: f . b1 = (|.f.| (#) (f (#) (|.f.| "))) . b1
then ((Re (f . x)) ^2) + ((Im (f . x)) ^2) = 0 by COMPLEX1:5;
then f . x = ((f (#) (|.f.| ")) . x) * |.(f . x).| by A39, SQUARE_1:17;
hence f . x = (|.f.| (#) (f (#) (|.f.| "))) . x by A6, A36, A38, VALUED_1:def_11; ::_thesis: verum
end;
end;
end;
then A40: f = |.f.| (#) (f (#) (|.f.| ")) by A6, A9, A13, FUNCT_1:2;
then A41: (((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| "))) is_integrable_on M by A2, Th40;
then consider R1, I1 being Real such that
A42: R1 = Integral (M,(Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) and
I1 = Integral (M,(Im (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) and
A43: Integral (M,(|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) = R1 + (I1 * **) by A17, Def3;
A44: Im (b1 * (b1 *')) = 0 by COMPLEX1:40;
((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *') = (Re (((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *'))) + ((Im (((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *'))) * **) by COMPLEX1:13;
then ((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *') = |.(((Integral (M,f)) / |.(Integral (M,f)).|) * ((Integral (M,f)) / |.(Integral (M,f)).|)).| by A30, A44, COMPLEX1:68;
then ((((Integral (M,f)) / |.(Integral (M,f)).|) *') * (Integral (M,f))) / |.(Integral (M,f)).| = 1 by A7, A18, A5, COMPLEX1:65;
then A45: (((Integral (M,f)) / |.(Integral (M,f)).|) *') * (Integral (M,f)) = |.(Integral (M,f)).| by XCMPLX_1:58;
Re (R1 + (I1 * **)) = R1 by COMPLEX1:12;
then Re |.(Integral (M,f)).| = R1 by A2, A45, A40, A17, A43, Th40;
then A46: |.(Integral (M,f)).| = Integral (M,(Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) by A42, COMPLEX1:def_1;
|.f.| (#) (f (#) (|.f.| ")) is_measurable_on A by A32, A6, A9, A13, A34, FUNCT_1:2;
then (((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| "))) is_measurable_on A by A31, A6, A9, A13, Th17;
then A47: Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) is_measurable_on A by A17, Def1;
Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) is_integrable_on M by A17, A41, Def2;
then consider E being Element of S such that
A48: E = (dom (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) /\ (dom |.f.|) and
A49: Integral (M,((Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) | E)) <= Integral (M,(|.f.| | E)) by A4, A31, A6, A33, A47, A12, A29, Th42;
|.f.| | E = |.f.| by A6, A12, A48, RELAT_1:68;
hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A6, A46, A12, A48, A49, RELAT_1:68; ::_thesis: verum
end;
theorem :: MESFUN6C:43
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
let f be PartFunc of X,COMPLEX; ::_thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is_integrable_on M implies |.(Integral (M,f)).| <= Integral (M,|.f.|) )
assume that
A1: ex A being Element of S st
( A = dom f & f is_measurable_on A ) and
A2: f is_integrable_on M ; ::_thesis: |.(Integral (M,f)).| <= Integral (M,|.f.|)
percases ( Integral (M,f) = 0 or Integral (M,f) <> 0 ) ;
suppose Integral (M,f) = 0 ; ::_thesis: |.(Integral (M,f)).| <= Integral (M,|.f.|)
hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A1, A2, Lm2; ::_thesis: verum
end;
suppose Integral (M,f) <> 0 ; ::_thesis: |.(Integral (M,f)).| <= Integral (M,|.f.|)
hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A1, A2, Lm3; ::_thesis: verum
end;
end;
end;
definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,COMPLEX;
let B be Element of S;
func Integral_on (M,B,f) -> complex number equals :: MESFUN6C:def 5
Integral (M,(f | B));
coherence
Integral (M,(f | B)) is complex number ;
end;
:: deftheorem defines Integral_on MESFUN6C:def_5_:_
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for B being Element of S holds Integral_on (M,B,f) = Integral (M,(f | B));
theorem :: MESFUN6C:44
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX
for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX
for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX
for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,COMPLEX
for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
let f, g be PartFunc of X,COMPLEX; ::_thesis: for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
let B be Element of S; ::_thesis: ( f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) implies ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M and
A3: B c= dom (f + g) ; ::_thesis: ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
A4: Re f is_integrable_on M by A1, Def2;
then (Re f) | B is_integrable_on M by MESFUNC6:91;
then A5: Re (f | B) is_integrable_on M by Th7;
then A6: Integral (M,(Re (f | B))) < +infty by MESFUNC6:90;
A7: Im f is_integrable_on M by A1, Def2;
then (Im f) | B is_integrable_on M by MESFUNC6:91;
then A8: Im (f | B) is_integrable_on M by Th7;
then A9: -infty < Integral (M,(Im (f | B))) by MESFUNC6:90;
A10: Integral (M,(Im (f | B))) < +infty by A8, MESFUNC6:90;
-infty < Integral (M,(Re (f | B))) by A5, MESFUNC6:90;
then reconsider R1 = Integral (M,(Re (f | B))), I1 = Integral (M,(Im (f | B))) as Real by A6, A9, A10, XXREAL_0:14;
f | B is_integrable_on M by A5, A8, Def2;
then A11: Integral (M,(f | B)) = R1 + (I1 * **) by Def3;
A12: Im g is_integrable_on M by A2, Def2;
then (Im g) | B is_integrable_on M by MESFUNC6:91;
then A13: Im (g | B) is_integrable_on M by Th7;
then A14: -infty < Integral (M,(Im (g | B))) by MESFUNC6:90;
A15: Re g is_integrable_on M by A2, Def2;
then (Re g) | B is_integrable_on M by MESFUNC6:91;
then A16: Re (g | B) is_integrable_on M by Th7;
then A17: Integral (M,(Re (g | B))) < +infty by MESFUNC6:90;
B c= dom (Im (f + g)) by A3, COMSEQ_3:def_4;
then A18: B c= dom ((Im f) + (Im g)) by Th5;
then Integral_on (M,B,((Im f) + (Im g))) = (Integral_on (M,B,(Im f))) + (Integral_on (M,B,(Im g))) by A7, A12, MESFUNC6:103;
then A19: Integral (M,((Im (f + g)) | B)) = (Integral (M,((Im f) | B))) + (Integral (M,((Im g) | B))) by Th5;
A20: Integral (M,(Im (g | B))) < +infty by A13, MESFUNC6:90;
-infty < Integral (M,(Re (g | B))) by A16, MESFUNC6:90;
then reconsider R2 = Integral (M,(Re (g | B))), I2 = Integral (M,(Im (g | B))) as Real by A17, A14, A20, XXREAL_0:14;
g | B is_integrable_on M by A16, A13, Def2;
then A21: Integral (M,(g | B)) = R2 + (I2 * **) by Def3;
A22: Integral (M,((Im g) | B)) = I2 by Th7;
(Im f) + (Im g) is_integrable_on M by A7, A12, A18, MESFUNC6:103;
then A23: Im (f + g) is_integrable_on M by Th5;
then (Im (f + g)) | B is_integrable_on M by MESFUNC6:91;
then A24: Im ((f + g) | B) is_integrable_on M by Th7;
then A25: -infty < Integral (M,(Im ((f + g) | B))) by MESFUNC6:90;
B c= dom (Re (f + g)) by A3, COMSEQ_3:def_3;
then A26: B c= dom ((Re f) + (Re g)) by Th5;
then Integral_on (M,B,((Re f) + (Re g))) = (Integral_on (M,B,(Re f))) + (Integral_on (M,B,(Re g))) by A4, A15, MESFUNC6:103;
then A27: Integral (M,((Re (f + g)) | B)) = (Integral (M,((Re f) | B))) + (Integral (M,((Re g) | B))) by Th5;
(Re f) + (Re g) is_integrable_on M by A4, A15, A26, MESFUNC6:103;
then A28: Re (f + g) is_integrable_on M by Th5;
then (Re (f + g)) | B is_integrable_on M by MESFUNC6:91;
then A29: Re ((f + g) | B) is_integrable_on M by Th7;
then A30: Integral (M,(Re ((f + g) | B))) < +infty by MESFUNC6:90;
A31: Integral (M,(Im ((f + g) | B))) < +infty by A24, MESFUNC6:90;
-infty < Integral (M,(Re ((f + g) | B))) by A29, MESFUNC6:90;
then reconsider R = Integral (M,(Re ((f + g) | B))), I = Integral (M,(Im ((f + g) | B))) as Real by A30, A25, A31, XXREAL_0:14;
A32: Integral (M,((Re g) | B)) = R2 by Th7;
Integral (M,((Im f) | B)) = I1 by Th7;
then R_EAL I = (R_EAL I1) + (R_EAL I2) by A19, A22, Th7;
then A33: I = I1 + I2 by SUPINF_2:1;
Integral (M,((Re f) | B)) = R1 by Th7;
then R_EAL R = (R_EAL R1) + (R_EAL R2) by A27, A32, Th7;
then A34: R = R1 + R2 by SUPINF_2:1;
(f + g) | B is_integrable_on M by A29, A24, Def2;
then Integral_on (M,B,(f + g)) = R + (I * **) by Def3
.= (Integral_on (M,B,f)) + (Integral_on (M,B,g)) by A34, A33, A11, A21 ;
hence ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) by A28, A23, Def2; ::_thesis: verum
end;
theorem :: MESFUN6C:45
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for c being complex number
for B being Element of S st f is_integrable_on M holds
Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for c being complex number
for B being Element of S st f is_integrable_on M holds
Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f))
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for c being complex number
for B being Element of S st f is_integrable_on M holds
Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f))
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX
for c being complex number
for B being Element of S st f is_integrable_on M holds
Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f))
let f be PartFunc of X,COMPLEX; ::_thesis: for c being complex number
for B being Element of S st f is_integrable_on M holds
Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f))
let c be complex number ; ::_thesis: for B being Element of S st f is_integrable_on M holds
Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f))
let B be Element of S; ::_thesis: ( f is_integrable_on M implies Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) )
assume f is_integrable_on M ; ::_thesis: Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f))
then A1: f | B is_integrable_on M by Th23;
A2: dom ((c (#) f) | B) = (dom (c (#) f)) /\ B by RELAT_1:61;
then dom ((c (#) f) | B) = (dom f) /\ B by VALUED_1:def_5;
then A3: dom ((c (#) f) | B) = dom (f | B) by RELAT_1:61;
A4: now__::_thesis:_for_x_being_set_st_x_in_dom_((c_(#)_f)_|_B)_holds_
((c_(#)_f)_|_B)_._x_=_(c_(#)_(f_|_B))_._x
let x be set ; ::_thesis: ( x in dom ((c (#) f) | B) implies ((c (#) f) | B) . x = (c (#) (f | B)) . x )
assume A5: x in dom ((c (#) f) | B) ; ::_thesis: ((c (#) f) | B) . x = (c (#) (f | B)) . x
then A6: ((c (#) f) | B) . x = (c (#) f) . x by FUNCT_1:47;
x in dom (c (#) f) by A2, A5, XBOOLE_0:def_4;
then ((c (#) f) | B) . x = c * (f . x) by A6, VALUED_1:def_5;
then A7: ((c (#) f) | B) . x = c * ((f | B) . x) by A3, A5, FUNCT_1:47;
x in dom (c (#) (f | B)) by A3, A5, VALUED_1:def_5;
hence ((c (#) f) | B) . x = (c (#) (f | B)) . x by A7, VALUED_1:def_5; ::_thesis: verum
end;
dom ((c (#) f) | B) = dom (c (#) (f | B)) by A3, VALUED_1:def_5;
then (c (#) f) | B = c (#) (f | B) by A4, FUNCT_1:2;
hence Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) by A1, Th40; ::_thesis: verum
end;
begin
theorem :: MESFUN6C:46
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a)))
let S be SigmaField of X; ::_thesis: for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a)))
let A be Element of S; ::_thesis: for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a)))
let f be PartFunc of X,REAL; ::_thesis: for a being Real st A c= dom f holds
A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a)))
let a be Real; ::_thesis: ( A c= dom f implies A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) )
now__::_thesis:_for_x_being_set_st_x_in_A_/\_(great_eq_dom_(f,a))_holds_
x_in_A_\_(A_/\_(less_dom_(f,a)))
let x be set ; ::_thesis: ( x in A /\ (great_eq_dom (f,a)) implies x in A \ (A /\ (less_dom (f,a))) )
assume A1: x in A /\ (great_eq_dom (f,a)) ; ::_thesis: x in A \ (A /\ (less_dom (f,a)))
then x in great_eq_dom (f,a) by XBOOLE_0:def_4;
then ex y being Real st
( y = f . x & a <= y ) by MESFUNC6:6;
then for y1 being Real holds
( not y1 = f . x or not y1 < a ) ;
then not x in less_dom (f,a) by MESFUNC6:3;
then A2: not x in A /\ (less_dom (f,a)) by XBOOLE_0:def_4;
x in A by A1, XBOOLE_0:def_4;
hence x in A \ (A /\ (less_dom (f,a))) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
then A3: A /\ (great_eq_dom (f,a)) c= A \ (A /\ (less_dom (f,a))) by TARSKI:def_3;
assume A4: A c= dom f ; ::_thesis: A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a)))
now__::_thesis:_for_x_being_set_st_x_in_A_\_(A_/\_(less_dom_(f,a)))_holds_
x_in_A_/\_(great_eq_dom_(f,a))
let x be set ; ::_thesis: ( x in A \ (A /\ (less_dom (f,a))) implies x in A /\ (great_eq_dom (f,a)) )
assume A5: x in A \ (A /\ (less_dom (f,a))) ; ::_thesis: x in A /\ (great_eq_dom (f,a))
then A6: x in A by XBOOLE_0:def_5;
not x in A /\ (less_dom (f,a)) by A5, XBOOLE_0:def_5;
then not x in less_dom (f,a) by A6, XBOOLE_0:def_4;
then not f . x < a by A4, A6, MESFUNC6:3;
then x in great_eq_dom (f,a) by A4, A6, MESFUNC6:6;
hence x in A /\ (great_eq_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
then A \ (A /\ (less_dom (f,a))) c= A /\ (great_eq_dom (f,a)) by TARSKI:def_3;
hence A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: MESFUN6C:47
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))
let S be SigmaField of X; ::_thesis: for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))
let A be Element of S; ::_thesis: for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))
let f be PartFunc of X,REAL; ::_thesis: for a being Real st A c= dom f holds
A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))
let a be Real; ::_thesis: ( A c= dom f implies A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) )
now__::_thesis:_for_x_being_set_st_x_in_A_/\_(great_dom_(f,a))_holds_
x_in_A_\_(A_/\_(less_eq_dom_(f,a)))
let x be set ; ::_thesis: ( x in A /\ (great_dom (f,a)) implies x in A \ (A /\ (less_eq_dom (f,a))) )
assume A1: x in A /\ (great_dom (f,a)) ; ::_thesis: x in A \ (A /\ (less_eq_dom (f,a)))
then x in great_dom (f,a) by XBOOLE_0:def_4;
then ex y being Real st
( y = f . x & a < y ) by MESFUNC6:5;
then for y1 being Real holds
( not y1 = f . x or not y1 <= a ) ;
then not x in less_eq_dom (f,a) by MESFUNC6:4;
then A2: not x in A /\ (less_eq_dom (f,a)) by XBOOLE_0:def_4;
x in A by A1, XBOOLE_0:def_4;
hence x in A \ (A /\ (less_eq_dom (f,a))) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
then A3: A /\ (great_dom (f,a)) c= A \ (A /\ (less_eq_dom (f,a))) by TARSKI:def_3;
assume A4: A c= dom f ; ::_thesis: A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a)))
now__::_thesis:_for_x_being_set_st_x_in_A_\_(A_/\_(less_eq_dom_(f,a)))_holds_
x_in_A_/\_(great_dom_(f,a))
let x be set ; ::_thesis: ( x in A \ (A /\ (less_eq_dom (f,a))) implies x in A /\ (great_dom (f,a)) )
assume A5: x in A \ (A /\ (less_eq_dom (f,a))) ; ::_thesis: x in A /\ (great_dom (f,a))
then A6: x in A by XBOOLE_0:def_5;
not x in A /\ (less_eq_dom (f,a)) by A5, XBOOLE_0:def_5;
then not x in less_eq_dom (f,a) by A6, XBOOLE_0:def_4;
then not f . x <= a by A4, A6, MESFUNC6:4;
then x in great_dom (f,a) by A4, A6, MESFUNC6:5;
hence x in A /\ (great_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
then A \ (A /\ (less_eq_dom (f,a))) c= A /\ (great_dom (f,a)) by TARSKI:def_3;
hence A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: MESFUN6C:48
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
let S be SigmaField of X; ::_thesis: for A being Element of S
for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
let A be Element of S; ::_thesis: for f being PartFunc of X,REAL
for a being Real st A c= dom f holds
A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
let f be PartFunc of X,REAL; ::_thesis: for a being Real st A c= dom f holds
A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
let a be Real; ::_thesis: ( A c= dom f implies A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) )
now__::_thesis:_for_x_being_set_st_x_in_A_/\_(less_eq_dom_(f,a))_holds_
x_in_A_\_(A_/\_(great_dom_(f,a)))
let x be set ; ::_thesis: ( x in A /\ (less_eq_dom (f,a)) implies x in A \ (A /\ (great_dom (f,a))) )
assume A1: x in A /\ (less_eq_dom (f,a)) ; ::_thesis: x in A \ (A /\ (great_dom (f,a)))
then x in less_eq_dom (f,a) by XBOOLE_0:def_4;
then ex y being Real st
( y = f . x & y <= a ) by MESFUNC6:4;
then for y1 being Real holds
( not y1 = f . x or not a < y1 ) ;
then not x in great_dom (f,a) by MESFUNC6:5;
then A2: not x in A /\ (great_dom (f,a)) by XBOOLE_0:def_4;
x in A by A1, XBOOLE_0:def_4;
hence x in A \ (A /\ (great_dom (f,a))) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
then A3: A /\ (less_eq_dom (f,a)) c= A \ (A /\ (great_dom (f,a))) by TARSKI:def_3;
assume A4: A c= dom f ; ::_thesis: A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a)))
now__::_thesis:_for_x_being_set_st_x_in_A_\_(A_/\_(great_dom_(f,a)))_holds_
x_in_A_/\_(less_eq_dom_(f,a))
let x be set ; ::_thesis: ( x in A \ (A /\ (great_dom (f,a))) implies x in A /\ (less_eq_dom (f,a)) )
assume A5: x in A \ (A /\ (great_dom (f,a))) ; ::_thesis: x in A /\ (less_eq_dom (f,a))
then A6: x in A by XBOOLE_0:def_5;
not x in A /\ (great_dom (f,a)) by A5, XBOOLE_0:def_5;
then not x in great_dom (f,a) by A6, XBOOLE_0:def_4;
then not a < f . x by A4, A6, MESFUNC6:5;
then x in less_eq_dom (f,a) by A4, A6, MESFUNC6:4;
hence x in A /\ (less_eq_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
then A \ (A /\ (great_dom (f,a))) c= A /\ (less_eq_dom (f,a)) by TARSKI:def_3;
hence A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: MESFUN6C:49
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
let S be SigmaField of X; ::_thesis: for A being Element of S
for f being PartFunc of X,REAL
for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
let A be Element of S; ::_thesis: for f being PartFunc of X,REAL
for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
let f be PartFunc of X,REAL; ::_thesis: for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
let a be Real; ::_thesis: A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
now__::_thesis:_for_x_being_set_st_x_in_(A_/\_(great_eq_dom_(f,a)))_/\_(less_eq_dom_(f,a))_holds_
x_in_A_/\_(eq_dom_(f,a))
let x be set ; ::_thesis: ( x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) implies x in A /\ (eq_dom (f,a)) )
assume A1: x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) ; ::_thesis: x in A /\ (eq_dom (f,a))
then A2: x in less_eq_dom (f,a) by XBOOLE_0:def_4;
then A3: x in dom f by MESFUNC6:4;
A4: x in A /\ (great_eq_dom (f,a)) by A1, XBOOLE_0:def_4;
then x in great_eq_dom (f,a) by XBOOLE_0:def_4;
then A5: ex y1 being Real st
( y1 = f . x & a <= y1 ) by MESFUNC6:6;
ex y2 being Real st
( y2 = f . x & y2 <= a ) by A2, MESFUNC6:4;
then a = f . x by A5, XXREAL_0:1;
then A6: x in eq_dom (f,a) by A3, MESFUNC6:7;
x in A by A4, XBOOLE_0:def_4;
hence x in A /\ (eq_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
then A7: (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) c= A /\ (eq_dom (f,a)) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_A_/\_(eq_dom_(f,a))_holds_
x_in_(A_/\_(great_eq_dom_(f,a)))_/\_(less_eq_dom_(f,a))
let x be set ; ::_thesis: ( x in A /\ (eq_dom (f,a)) implies x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) )
assume A8: x in A /\ (eq_dom (f,a)) ; ::_thesis: x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
then A9: x in A by XBOOLE_0:def_4;
A10: x in eq_dom (f,a) by A8, XBOOLE_0:def_4;
then A11: ex y being Real st
( y = f . x & a = y ) by MESFUNC6:7;
A12: x in dom f by A10, MESFUNC6:7;
then x in great_eq_dom (f,a) by A11, MESFUNC6:6;
then A13: x in A /\ (great_eq_dom (f,a)) by A9, XBOOLE_0:def_4;
x in less_eq_dom (f,a) by A11, A12, MESFUNC6:4;
hence x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by A13, XBOOLE_0:def_4; ::_thesis: verum
end;
then A /\ (eq_dom (f,a)) c= (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by TARSKI:def_3;
hence A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by A7, XBOOLE_0:def_10; ::_thesis: verum
end;
*