:: MESFUN7C semantic presentation
begin
definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func R_EAL f -> Functional_Sequence of X,ExtREAL equals :: MESFUN7C:def 1
f;
coherence
f is Functional_Sequence of X,ExtREAL
proof
( dom f = NAT & ( for n being Element of NAT holds f . n is PartFunc of X,ExtREAL ) ) by NUMBERS:31, RELSET_1:7, SEQFUNC:1;
hence f is Functional_Sequence of X,ExtREAL by SEQFUNC:1; ::_thesis: verum
end;
end;
:: deftheorem defines R_EAL MESFUN7C:def_1_:_
for X being non empty set
for f being Functional_Sequence of X,REAL holds R_EAL f = f;
theorem Th1: :: MESFUN7C:1
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X holds f # x = (R_EAL f) # x
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X holds f # x = (R_EAL f) # x
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X holds f # x = (R_EAL f) # x
let x be Element of X; ::_thesis: f # x = (R_EAL f) # x
now__::_thesis:_for_r_being_set_st_r_in_rng_((R_EAL_f)_#_x)_holds_
r_in_REAL
let r be set ; ::_thesis: ( r in rng ((R_EAL f) # x) implies r in REAL )
assume r in rng ((R_EAL f) # x) ; ::_thesis: r in REAL
then consider n being set such that
A1: n in NAT and
A2: ((R_EAL f) # x) . n = r by FUNCT_2:11;
reconsider n = n as Element of NAT by A1;
r = ((R_EAL f) . n) . x by A2, MESFUNC5:def_13
.= (R_EAL (f . n)) . x
.= (f . n) . x ;
hence r in REAL ; ::_thesis: verum
end;
then rng ((R_EAL f) # x) c= REAL by TARSKI:def_3;
then reconsider RFx = (R_EAL f) # x as Function of NAT,REAL by FUNCT_2:6;
reconsider RFx = RFx as Real_Sequence ;
now__::_thesis:_for_n_being_set_st_n_in_NAT_holds_
RFx_._n_=_(f_#_x)_._n
let n be set ; ::_thesis: ( n in NAT implies RFx . n = (f # x) . n )
assume n in NAT ; ::_thesis: RFx . n = (f # x) . n
then reconsider n1 = n as Element of NAT ;
RFx . n = ((R_EAL f) . n1) . x by MESFUNC5:def_13
.= (R_EAL (f . n1)) . x ;
hence RFx . n = (f # x) . n by SEQFUNC:def_10; ::_thesis: verum
end;
hence f # x = (R_EAL f) # x by FUNCT_2:12; ::_thesis: verum
end;
registration
let X be non empty set ;
let f be Function of X,REAL;
cluster R_EAL f -> total ;
coherence
R_EAL f is total ;
end;
definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func inf f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 2
inf (R_EAL f);
coherence
inf (R_EAL f) is PartFunc of X,ExtREAL ;
end;
:: deftheorem defines inf MESFUN7C:def_2_:_
for X being non empty set
for f being Functional_Sequence of X,REAL holds inf f = inf (R_EAL f);
theorem Th2: :: MESFUN7C:2
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (inf f) holds
(inf f) . x = inf (rng (R_EAL (f # x)))
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (inf f) holds
(inf f) . x = inf (rng (R_EAL (f # x)))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (inf f) holds
(inf f) . x = inf (rng (R_EAL (f # x)))
let x be Element of X; ::_thesis: ( x in dom (inf f) implies (inf f) . x = inf (rng (R_EAL (f # x))) )
assume x in dom (inf f) ; ::_thesis: (inf f) . x = inf (rng (R_EAL (f # x)))
then (inf f) . x = inf ((R_EAL f) # x) by MESFUNC8:def_3;
hence (inf f) . x = inf (rng (R_EAL (f # x))) by Th1; ::_thesis: verum
end;
definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func sup f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 3
sup (R_EAL f);
coherence
sup (R_EAL f) is PartFunc of X,ExtREAL ;
end;
:: deftheorem defines sup MESFUN7C:def_3_:_
for X being non empty set
for f being Functional_Sequence of X,REAL holds sup f = sup (R_EAL f);
theorem Th3: :: MESFUN7C:3
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (sup f) holds
(sup f) . x = sup (rng (R_EAL (f # x)))
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (sup f) holds
(sup f) . x = sup (rng (R_EAL (f # x)))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (sup f) holds
(sup f) . x = sup (rng (R_EAL (f # x)))
let x be Element of X; ::_thesis: ( x in dom (sup f) implies (sup f) . x = sup (rng (R_EAL (f # x))) )
assume x in dom (sup f) ; ::_thesis: (sup f) . x = sup (rng (R_EAL (f # x)))
then (sup f) . x = sup ((R_EAL f) # x) by MESFUNC8:def_4;
hence (sup f) . x = sup (rng (R_EAL (f # x))) by Th1; ::_thesis: verum
end;
definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func inferior_realsequence f -> with_the_same_dom Functional_Sequence of X,ExtREAL equals :: MESFUN7C:def 4
inferior_realsequence (R_EAL f);
coherence
inferior_realsequence (R_EAL f) is with_the_same_dom Functional_Sequence of X,ExtREAL ;
end;
:: deftheorem defines inferior_realsequence MESFUN7C:def_4_:_
for X being non empty set
for f being Functional_Sequence of X,REAL holds inferior_realsequence f = inferior_realsequence (R_EAL f);
theorem Th4: :: MESFUN7C:4
for X being non empty set
for f being Functional_Sequence of X,REAL
for n being Nat holds
( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) )
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for n being Nat holds
( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) )
let f be Functional_Sequence of X,REAL; ::_thesis: for n being Nat holds
( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) )
let n be Nat; ::_thesis: ( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) )
set IF = inferior_realsequence f;
dom ((inferior_realsequence f) . n) = dom ((R_EAL f) . 0) by MESFUNC8:def_5
.= dom (R_EAL (f . 0)) ;
hence dom ((inferior_realsequence f) . n) = dom (f . 0) ; ::_thesis: for x being Element of X st x in dom ((inferior_realsequence f) . n) holds
((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n
A1: n in NAT by ORDINAL1:def_12;
hereby ::_thesis: verum
let x be Element of X; ::_thesis: ( x in dom ((inferior_realsequence f) . n) implies ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n )
assume x in dom ((inferior_realsequence f) . n) ; ::_thesis: ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n
then A2: ((inferior_realsequence f) . n) . x = (inferior_realsequence ((R_EAL f) # x)) . n by MESFUNC8:def_5
.= inf (((R_EAL f) # x) ^\ n) by A1, RINFSUP2:27 ;
(R_EAL f) # x = f # x by Th1;
hence ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n by A1, A2, RINFSUP2:27; ::_thesis: verum
end;
end;
definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func superior_realsequence f -> with_the_same_dom Functional_Sequence of X,ExtREAL equals :: MESFUN7C:def 5
superior_realsequence (R_EAL f);
coherence
superior_realsequence (R_EAL f) is with_the_same_dom Functional_Sequence of X,ExtREAL ;
end;
:: deftheorem defines superior_realsequence MESFUN7C:def_5_:_
for X being non empty set
for f being Functional_Sequence of X,REAL holds superior_realsequence f = superior_realsequence (R_EAL f);
theorem Th5: :: MESFUN7C:5
for X being non empty set
for f being Functional_Sequence of X,REAL
for n being Nat holds
( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds
((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) )
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for n being Nat holds
( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds
((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) )
let f be Functional_Sequence of X,REAL; ::_thesis: for n being Nat holds
( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds
((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) )
let n be Nat; ::_thesis: ( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds
((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) )
set SF = superior_realsequence f;
thus dom ((superior_realsequence f) . n) = dom (f . 0) by MESFUNC8:def_6; ::_thesis: for x being Element of X st x in dom ((superior_realsequence f) . n) holds
((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n
hereby ::_thesis: verum
let x be Element of X; ::_thesis: ( x in dom ((superior_realsequence f) . n) implies ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n )
assume x in dom ((superior_realsequence f) . n) ; ::_thesis: ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n
then ((superior_realsequence f) . n) . x = (superior_realsequence ((R_EAL f) # x)) . n by MESFUNC8:def_6;
hence ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n by Th1; ::_thesis: verum
end;
end;
theorem :: MESFUN7C:6
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (f . 0) holds
(inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x))
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (f . 0) holds
(inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (f . 0) holds
(inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x))
let x be Element of X; ::_thesis: ( x in dom (f . 0) implies (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x)) )
set F = inferior_realsequence f;
assume A1: x in dom (f . 0) ; ::_thesis: (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x))
now__::_thesis:_for_n_being_Element_of_NAT_holds_((inferior_realsequence_f)_#_x)_._n_=_(inferior_realsequence_(R_EAL_(f_#_x)))_._n
let n be Element of NAT ; ::_thesis: ((inferior_realsequence f) # x) . n = (inferior_realsequence (R_EAL (f # x))) . n
( dom ((inferior_realsequence f) . n) = dom (f . 0) & ((inferior_realsequence f) # x) . n = ((inferior_realsequence f) . n) . x ) by Th4, MESFUNC5:def_13;
hence ((inferior_realsequence f) # x) . n = (inferior_realsequence (R_EAL (f # x))) . n by A1, Th4; ::_thesis: verum
end;
hence (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x)) by FUNCT_2:63; ::_thesis: verum
end;
registration
let X be non empty set ;
let f be with_the_same_dom Functional_Sequence of X,REAL;
cluster R_EAL f -> with_the_same_dom ;
coherence
R_EAL f is with_the_same_dom
proof
for n, m being Nat holds dom ((R_EAL f) . n) = dom ((R_EAL f) . m) by MESFUNC8:def_2;
hence R_EAL f is with_the_same_dom by MESFUNC8:def_2; ::_thesis: verum
end;
end;
theorem Th7: :: MESFUN7C:7
for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,REAL
for S being SigmaField of X
for E being Element of S
for n being Nat st f . n is_measurable_on E holds
(R_EAL f) . n is_measurable_on E
proof
let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for S being SigmaField of X
for E being Element of S
for n being Nat st f . n is_measurable_on E holds
(R_EAL f) . n is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for S being SigmaField of X
for E being Element of S
for n being Nat st f . n is_measurable_on E holds
(R_EAL f) . n is_measurable_on E
let S be SigmaField of X; ::_thesis: for E being Element of S
for n being Nat st f . n is_measurable_on E holds
(R_EAL f) . n is_measurable_on E
let E be Element of S; ::_thesis: for n being Nat st f . n is_measurable_on E holds
(R_EAL f) . n is_measurable_on E
let n be Nat; ::_thesis: ( f . n is_measurable_on E implies (R_EAL f) . n is_measurable_on E )
assume f . n is_measurable_on E ; ::_thesis: (R_EAL f) . n is_measurable_on E
then R_EAL (f . n) is_measurable_on E by MESFUNC6:def_1;
hence (R_EAL f) . n is_measurable_on E ; ::_thesis: verum
end;
theorem :: MESFUN7C:8
for X being non empty set
for f being Functional_Sequence of X,REAL
for n being Nat holds (R_EAL f) ^\ n = R_EAL (f ^\ n) ;
theorem :: MESFUN7C:9
for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,REAL
for n being Nat holds (inferior_realsequence f) . n = inf (f ^\ n)
proof
let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for n being Nat holds (inferior_realsequence f) . n = inf (f ^\ n)
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for n being Nat holds (inferior_realsequence f) . n = inf (f ^\ n)
let n be Nat; ::_thesis: (inferior_realsequence f) . n = inf (f ^\ n)
n in NAT by ORDINAL1:def_12;
then (inferior_realsequence (R_EAL f)) . n = inf ((R_EAL f) ^\ n) by MESFUNC8:8;
hence (inferior_realsequence f) . n = inf (f ^\ n) ; ::_thesis: verum
end;
theorem :: MESFUN7C:10
for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,REAL
for n being Nat holds (superior_realsequence f) . n = sup (f ^\ n)
proof
let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for n being Nat holds (superior_realsequence f) . n = sup (f ^\ n)
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for n being Nat holds (superior_realsequence f) . n = sup (f ^\ n)
let n be Nat; ::_thesis: (superior_realsequence f) . n = sup (f ^\ n)
n in NAT by ORDINAL1:def_12;
then (superior_realsequence (R_EAL f)) . n = sup ((R_EAL f) ^\ n) by MESFUNC8:9;
hence (superior_realsequence f) . n = sup (f ^\ n) ; ::_thesis: verum
end;
theorem Th11: :: MESFUN7C:11
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (f . 0) holds
(superior_realsequence f) # x = superior_realsequence (R_EAL (f # x))
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (f . 0) holds
(superior_realsequence f) # x = superior_realsequence (R_EAL (f # x))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (f . 0) holds
(superior_realsequence f) # x = superior_realsequence (R_EAL (f # x))
let x be Element of X; ::_thesis: ( x in dom (f . 0) implies (superior_realsequence f) # x = superior_realsequence (R_EAL (f # x)) )
set F = superior_realsequence f;
assume A1: x in dom (f . 0) ; ::_thesis: (superior_realsequence f) # x = superior_realsequence (R_EAL (f # x))
now__::_thesis:_for_n_being_Element_of_NAT_holds_((superior_realsequence_f)_#_x)_._n_=_(superior_realsequence_(R_EAL_(f_#_x)))_._n
let n be Element of NAT ; ::_thesis: ((superior_realsequence f) # x) . n = (superior_realsequence (R_EAL (f # x))) . n
( dom ((superior_realsequence f) . n) = dom (f . 0) & ((superior_realsequence f) # x) . n = ((superior_realsequence f) . n) . x ) by Th5, MESFUNC5:def_13;
hence ((superior_realsequence f) # x) . n = (superior_realsequence (R_EAL (f # x))) . n by A1, Th5; ::_thesis: verum
end;
hence (superior_realsequence f) # x = superior_realsequence (R_EAL (f # x)) by FUNCT_2:63; ::_thesis: verum
end;
definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func lim_inf f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 6
lim_inf (R_EAL f);
coherence
lim_inf (R_EAL f) is PartFunc of X,ExtREAL ;
end;
:: deftheorem defines lim_inf MESFUN7C:def_6_:_
for X being non empty set
for f being Functional_Sequence of X,REAL holds lim_inf f = lim_inf (R_EAL f);
theorem Th12: :: MESFUN7C:12
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (lim_inf f) holds
(lim_inf f) . x = lim_inf (R_EAL (f # x))
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (lim_inf f) holds
(lim_inf f) . x = lim_inf (R_EAL (f # x))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (lim_inf f) holds
(lim_inf f) . x = lim_inf (R_EAL (f # x))
let x be Element of X; ::_thesis: ( x in dom (lim_inf f) implies (lim_inf f) . x = lim_inf (R_EAL (f # x)) )
assume x in dom (lim_inf f) ; ::_thesis: (lim_inf f) . x = lim_inf (R_EAL (f # x))
then (lim_inf f) . x = lim_inf ((R_EAL f) # x) by MESFUNC8:def_7;
hence (lim_inf f) . x = lim_inf (R_EAL (f # x)) by Th1; ::_thesis: verum
end;
definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func lim_sup f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 7
lim_sup (R_EAL f);
coherence
lim_sup (R_EAL f) is PartFunc of X,ExtREAL ;
end;
:: deftheorem defines lim_sup MESFUN7C:def_7_:_
for X being non empty set
for f being Functional_Sequence of X,REAL holds lim_sup f = lim_sup (R_EAL f);
theorem Th13: :: MESFUN7C:13
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (lim_sup f) holds
(lim_sup f) . x = lim_sup (R_EAL (f # x))
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (lim_sup f) holds
(lim_sup f) . x = lim_sup (R_EAL (f # x))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (lim_sup f) holds
(lim_sup f) . x = lim_sup (R_EAL (f # x))
let x be Element of X; ::_thesis: ( x in dom (lim_sup f) implies (lim_sup f) . x = lim_sup (R_EAL (f # x)) )
assume x in dom (lim_sup f) ; ::_thesis: (lim_sup f) . x = lim_sup (R_EAL (f # x))
then (lim_sup f) . x = lim_sup ((R_EAL f) # x) by MESFUNC8:def_8;
hence (lim_sup f) . x = lim_sup (R_EAL (f # x)) by Th1; ::_thesis: verum
end;
definition
let X be non empty set ;
let f be Functional_Sequence of X,REAL;
func lim f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 8
lim (R_EAL f);
coherence
lim (R_EAL f) is PartFunc of X,ExtREAL ;
end;
:: deftheorem defines lim MESFUN7C:def_8_:_
for X being non empty set
for f being Functional_Sequence of X,REAL holds lim f = lim (R_EAL f);
theorem Th14: :: MESFUN7C:14
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (lim f) holds
(lim f) . x = lim (R_EAL (f # x))
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (lim f) holds
(lim f) . x = lim (R_EAL (f # x))
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (lim f) holds
(lim f) . x = lim (R_EAL (f # x))
let x be Element of X; ::_thesis: ( x in dom (lim f) implies (lim f) . x = lim (R_EAL (f # x)) )
assume x in dom (lim f) ; ::_thesis: (lim f) . x = lim (R_EAL (f # x))
then (lim f) . x = lim ((R_EAL f) # x) by MESFUNC8:def_9;
hence (lim f) . x = lim (R_EAL (f # x)) by Th1; ::_thesis: verum
end;
theorem Th15: :: MESFUN7C:15
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (lim f) & f # x is convergent holds
( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (lim f) & f # x is convergent holds
( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (lim f) & f # x is convergent holds
( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
let x be Element of X; ::_thesis: ( x in dom (lim f) & f # x is convergent implies ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) )
assume that
A1: x in dom (lim f) and
A2: f # x is convergent ; ::_thesis: ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )
R_EAL (f # x) is convergent by A2, RINFSUP2:14;
then A3: ( lim (R_EAL (f # x)) = lim_sup (R_EAL (f # x)) & lim (R_EAL (f # x)) = lim_inf (R_EAL (f # x)) ) by RINFSUP2:41;
A4: x in dom (f . 0) by A1, MESFUNC8:def_9;
then x in dom (lim_inf f) by MESFUNC8:def_7;
then A5: (lim_inf f) . x = lim_inf (R_EAL (f # x)) by Th12;
x in dom (lim_sup f) by A4, MESFUNC8:def_8;
then (lim_sup f) . x = lim_sup (R_EAL (f # x)) by Th13;
hence ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) by A1, A5, A3, Th14; ::_thesis: verum
end;
theorem :: MESFUN7C:16
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))
let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))
let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) implies union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) )
set E = dom (f . 0);
assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ; ::_thesis: union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))
now__::_thesis:_for_x_being_set_st_x_in_(dom_(f_._0))_/\_(great_dom_((sup_f),r))_holds_
x_in_union_(rng_F)
let x be set ; ::_thesis: ( x in (dom (f . 0)) /\ (great_dom ((sup f),r)) implies x in union (rng F) )
assume A2: x in (dom (f . 0)) /\ (great_dom ((sup f),r)) ; ::_thesis: x in union (rng F)
then reconsider z = x as Element of X ;
A3: x in dom (f . 0) by A2, XBOOLE_0:def_4;
x in great_dom ((sup f),r) by A2, XBOOLE_0:def_4;
then A4: r < (sup f) . z by MESFUNC1:def_13;
ex n being Element of NAT st r < (f # z) . n
proof
assume A5: for n being Element of NAT holds (f # z) . n <= r ; ::_thesis: contradiction
for p being ext-real number st p in rng (R_EAL (f # z)) holds
p <= r
proof
let p be ext-real number ; ::_thesis: ( p in rng (R_EAL (f # z)) implies p <= r )
assume p in rng (R_EAL (f # z)) ; ::_thesis: p <= r
then ex n being set st
( n in NAT & (R_EAL (f # z)) . n = p ) by FUNCT_2:11;
hence p <= r by A5; ::_thesis: verum
end;
then r is UpperBound of rng (R_EAL (f # z)) by XXREAL_2:def_1;
then A6: sup (rng (R_EAL (f # z))) <= r by XXREAL_2:def_3;
x in dom (sup f) by A3, MESFUNC8:def_4;
hence contradiction by A4, A6, Th3; ::_thesis: verum
end;
then consider n being Element of NAT such that
A7: r < (f # z) . n ;
A8: x in dom (f . n) by A3, MESFUNC8:def_2;
r < (f . n) . z by A7, SEQFUNC:def_10;
then A9: x in great_dom ((f . n),r) by A8, MESFUNC1:def_13;
A10: F . n in rng F by FUNCT_2:4;
F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) by A1;
then x in F . n by A3, A9, XBOOLE_0:def_4;
hence x in union (rng F) by A10, TARSKI:def_4; ::_thesis: verum
end;
then A11: (dom (f . 0)) /\ (great_dom ((sup f),r)) c= union (rng F) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_union_(rng_F)_holds_
x_in_(dom_(f_._0))_/\_(great_dom_((sup_f),r))
let x be set ; ::_thesis: ( x in union (rng F) implies x in (dom (f . 0)) /\ (great_dom ((sup f),r)) )
assume x in union (rng F) ; ::_thesis: x in (dom (f . 0)) /\ (great_dom ((sup f),r))
then consider y being set such that
A12: x in y and
A13: y in rng F by TARSKI:def_4;
reconsider z = x as Element of X by A12, A13;
consider n being set such that
A14: n in dom F and
A15: y = F . n by A13, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A14;
A16: F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) by A1;
then x in great_dom ((f . n),r) by A12, A15, XBOOLE_0:def_4;
then A17: r < (f . n) . z by MESFUNC1:def_13;
f # z = (R_EAL f) # z by Th1;
then (f . n) . z = ((R_EAL f) # z) . n by SEQFUNC:def_10;
then A18: (f . n) . z <= sup (rng ((R_EAL f) # z)) by FUNCT_2:4, XXREAL_2:4;
A19: x in dom (f . 0) by A12, A15, A16, XBOOLE_0:def_4;
then A20: x in dom (sup f) by MESFUNC8:def_4;
then (sup f) . z = sup ((R_EAL f) # z) by MESFUNC8:def_4;
then r < (sup f) . z by A17, A18, XXREAL_0:2;
then x in great_dom ((sup f),r) by A20, MESFUNC1:def_13;
hence x in (dom (f . 0)) /\ (great_dom ((sup f),r)) by A19, XBOOLE_0:def_4; ::_thesis: verum
end;
then union (rng F) c= (dom (f . 0)) /\ (great_dom ((sup f),r)) by TARSKI:def_3;
hence union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) by A11, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem :: MESFUN7C:17
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) implies meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) )
set E = dom (f . 0);
assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ; ::_thesis: meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
now__::_thesis:_for_x_being_set_st_x_in_meet_(rng_F)_holds_
x_in_(dom_(f_._0))_/\_(great_eq_dom_((inf_f),r))
let x be set ; ::_thesis: ( x in meet (rng F) implies x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) )
assume A2: x in meet (rng F) ; ::_thesis: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r))
then reconsider z = x as Element of X ;
A3: F . 0 = (dom (f . 0)) /\ (great_eq_dom ((f . 0),r)) by A1;
F . 0 in rng F by FUNCT_2:4;
then x in F . 0 by A2, SETFAM_1:def_1;
then A4: x in dom (f . 0) by A3, XBOOLE_0:def_4;
then A5: x in dom (inf f) by MESFUNC8:def_3;
A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_r_<=_(R_EAL_(f_#_z))_._n
let n be Element of NAT ; ::_thesis: r <= (R_EAL (f # z)) . n
F . n in rng F by FUNCT_2:4;
then A7: z in F . n by A2, SETFAM_1:def_1;
F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) by A1;
then x in great_eq_dom ((f . n),r) by A7, XBOOLE_0:def_4;
then r <= (f . n) . z by MESFUNC1:def_14;
hence r <= (R_EAL (f # z)) . n by SEQFUNC:def_10; ::_thesis: verum
end;
for p being ext-real number st p in rng (R_EAL (f # z)) holds
r <= p
proof
let p be ext-real number ; ::_thesis: ( p in rng (R_EAL (f # z)) implies r <= p )
assume p in rng (R_EAL (f # z)) ; ::_thesis: r <= p
then ex n being set st
( n in NAT & (R_EAL (f # z)) . n = p ) by FUNCT_2:11;
hence r <= p by A6; ::_thesis: verum
end;
then r is LowerBound of rng (R_EAL (f # z)) by XXREAL_2:def_2;
then r <= inf (rng (R_EAL (f # z))) by XXREAL_2:def_4;
then r <= (inf f) . x by A5, Th2;
then x in great_eq_dom ((inf f),r) by A5, MESFUNC1:def_14;
hence x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
then A8: meet (rng F) c= (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_(dom_(f_._0))_/\_(great_eq_dom_((inf_f),r))_holds_
x_in_meet_(rng_F)
let x be set ; ::_thesis: ( x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) implies x in meet (rng F) )
assume A9: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) ; ::_thesis: x in meet (rng F)
then reconsider z = x as Element of X ;
A10: x in dom (f . 0) by A9, XBOOLE_0:def_4;
x in great_eq_dom ((inf f),r) by A9, XBOOLE_0:def_4;
then A11: r <= (inf f) . z by MESFUNC1:def_14;
now__::_thesis:_for_y_being_set_st_y_in_rng_F_holds_
x_in_y
let y be set ; ::_thesis: ( y in rng F implies x in y )
assume y in rng F ; ::_thesis: x in y
then consider n being set such that
A12: n in NAT and
A13: y = F . n by FUNCT_2:11;
reconsider n = n as Element of NAT by A12;
A14: x in dom (f . n) by A10, MESFUNC8:def_2;
x in dom (inf f) by A10, MESFUNC8:def_3;
then A15: (inf f) . z = inf (rng (R_EAL (f # z))) by Th2;
(f . n) . z = (R_EAL (f # z)) . n by SEQFUNC:def_10;
then (f . n) . z >= inf (rng (R_EAL (f # z))) by FUNCT_2:4, XXREAL_2:3;
then r <= (f . n) . z by A11, A15, XXREAL_0:2;
then A16: x in great_eq_dom ((f . n),r) by A14, MESFUNC1:def_14;
F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) by A1;
hence x in y by A10, A13, A16, XBOOLE_0:def_4; ::_thesis: verum
end;
hence x in meet (rng F) by SETFAM_1:def_1; ::_thesis: verum
end;
then (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) c= meet (rng F) by TARSKI:def_3;
hence meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) by A8, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th18: :: MESFUN7C:18
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_sup f is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_sup f is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_sup f is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_sup f is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies lim_sup f is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: lim_sup f is_measurable_on E
for n being Nat holds (R_EAL f) . n is_measurable_on E by A2, Th7;
hence lim_sup f is_measurable_on E by A1, MESFUNC8:23; ::_thesis: verum
end;
theorem :: MESFUN7C:19
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_inf f is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_inf f is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_inf f is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds
lim_inf f is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies lim_inf f is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: lim_inf f is_measurable_on E
for n being Nat holds (R_EAL f) . n is_measurable_on E by A2, Th7;
hence lim_inf f is_measurable_on E by A1, MESFUNC8:24; ::_thesis: verum
end;
theorem :: MESFUN7C:20
for X being non empty set
for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (f . 0) & f # x is convergent holds
(superior_realsequence f) # x is bounded_below
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL
for x being Element of X st x in dom (f . 0) & f # x is convergent holds
(superior_realsequence f) # x is bounded_below
let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (f . 0) & f # x is convergent holds
(superior_realsequence f) # x is bounded_below
let x be Element of X; ::_thesis: ( x in dom (f . 0) & f # x is convergent implies (superior_realsequence f) # x is bounded_below )
assume A1: x in dom (f . 0) ; ::_thesis: ( not f # x is convergent or (superior_realsequence f) # x is bounded_below )
assume f # x is convergent ; ::_thesis: (superior_realsequence f) # x is bounded_below
then A2: f # x is bounded ;
then superior_realsequence (R_EAL (f # x)) = superior_realsequence (f # x) by RINFSUP2:9;
then A3: (superior_realsequence f) # x = superior_realsequence (f # x) by A1, Th11;
superior_realsequence (f # x) is bounded by A2, RINFSUP1:56;
hence (superior_realsequence f) # x is bounded_below by A3, RINFSUP2:13; ::_thesis: verum
end;
theorem Th21: :: MESFUN7C:21
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) implies lim f is_measurable_on E )
assume A1: dom (f . 0) = E ; ::_thesis: ( ex n being Nat st not f . n is_measurable_on E or ex x being Element of X st
( x in E & not f # x is convergent ) or lim f is_measurable_on E )
then A2: dom (lim f) = E by MESFUNC8:def_9;
assume for n being Nat holds f . n is_measurable_on E ; ::_thesis: ( ex x being Element of X st
( x in E & not f # x is convergent ) or lim f is_measurable_on E )
then A3: lim_sup f is_measurable_on E by A1, Th18;
assume A4: for x being Element of X st x in E holds
f # x is convergent ; ::_thesis: lim f is_measurable_on E
A5: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_f)_holds_
(lim_f)_._x_=_(lim_sup_f)_._x
let x be Element of X; ::_thesis: ( x in dom (lim f) implies (lim f) . x = (lim_sup f) . x )
assume A6: x in dom (lim f) ; ::_thesis: (lim f) . x = (lim_sup f) . x
then f # x is convergent by A2, A4;
hence (lim f) . x = (lim_sup f) . x by A6, Th15; ::_thesis: verum
end;
dom (lim_sup f) = E by A1, MESFUNC8:def_8;
hence lim f is_measurable_on E by A2, A3, A5, PARTFUN1:5; ::_thesis: verum
end;
theorem Th22: :: MESFUN7C:22
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,REAL
for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL
for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let g be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) implies g is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E and
A3: dom g = E and
A4: for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ; ::_thesis: g is_measurable_on E
A5: dom (lim f) = E by A1, MESFUNC8:def_9;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_f)_holds_
g_._x_=_(lim_f)_._x
let x be Element of X; ::_thesis: ( x in dom (lim f) implies g . x = (lim f) . x )
assume A6: x in dom (lim f) ; ::_thesis: g . x = (lim f) . x
then x in E by A1, MESFUNC8:def_9;
then f # x is convergent by A4;
then lim (f # x) = lim (R_EAL (f # x)) by RINFSUP2:14;
then g . x = lim (R_EAL (f # x)) by A4, A5, A6;
hence g . x = (lim f) . x by A6, Th14; ::_thesis: verum
end;
then A7: g = lim f by A3, A5, PARTFUN1:5;
for x being Element of X st x in E holds
f # x is convergent by A4;
hence g is_measurable_on E by A1, A2, A7, Th21; ::_thesis: verum
end;
begin
definition
let X be non empty set ;
let H be Functional_Sequence of X,COMPLEX;
let x be Element of X;
funcH # x -> Complex_Sequence means :Def9: :: MESFUN7C:def 9
for n being Nat holds it . n = (H . n) . x;
existence
ex b1 being Complex_Sequence st
for n being Nat holds b1 . n = (H . n) . x
proof
defpred S1[ Element of NAT , set ] means $2 = (H . $1) . x;
A1: for n being Element of NAT ex y being Element of COMPLEX st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of COMPLEX st S1[n,y]
(H . n) . x in COMPLEX by XCMPLX_0:def_2;
hence ex y being Element of COMPLEX st S1[n,y] ; ::_thesis: verum
end;
consider f being Function of NAT,COMPLEX such that
A2: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A1);
take f ; ::_thesis: for n being Nat holds f . n = (H . n) . x
let n be Nat; ::_thesis: f . n = (H . n) . x
n in NAT by ORDINAL1:def_12;
hence f . n = (H . n) . x by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Complex_Sequence st ( for n being Nat holds b1 . n = (H . n) . x ) & ( for n being Nat holds b2 . n = (H . n) . x ) holds
b1 = b2
proof
let S1, S2 be Complex_Sequence; ::_thesis: ( ( for n being Nat holds S1 . n = (H . n) . x ) & ( for n being Nat holds S2 . n = (H . n) . x ) implies S1 = S2 )
assume that
A3: for n being Nat holds S1 . n = (H . n) . x and
A4: for n being Nat holds S2 . n = (H . n) . x ; ::_thesis: S1 = S2
now__::_thesis:_for_n_being_Element_of_NAT_holds_S1_._n_=_S2_._n
let n be Element of NAT ; ::_thesis: S1 . n = S2 . n
S1 . n = (H . n) . x by A3;
hence S1 . n = S2 . n by A4; ::_thesis: verum
end;
hence S1 = S2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines # MESFUN7C:def_9_:_
for X being non empty set
for H being Functional_Sequence of X,COMPLEX
for x being Element of X
for b4 being Complex_Sequence holds
( b4 = H # x iff for n being Nat holds b4 . n = (H . n) . x );
definition
let X be non empty set ;
let f be Functional_Sequence of X,COMPLEX;
func lim f -> PartFunc of X,COMPLEX means :Def10: :: MESFUN7C:def 10
( dom it = dom (f . 0) & ( for x being Element of X st x in dom it holds
it . x = lim (f # x) ) );
existence
ex b1 being PartFunc of X,COMPLEX st
( dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = lim (f # x) ) )
proof
defpred S1[ set ] means $1 in dom (f . 0);
deffunc H1( Element of X) -> Element of COMPLEX = lim (f # $1);
consider g being PartFunc of X,COMPLEX such that
A1: ( ( for x being Element of X holds
( x in dom g iff S1[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from PARTFUN2:sch_2();
take g ; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim (f # x) ) )
A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_lim_(f_#_x)
let x be Element of X; ::_thesis: ( x in dom g implies g . x = lim (f # x) )
assume A3: x in dom g ; ::_thesis: g . x = lim (f # x)
then g /. x = lim (f # x) by A1;
hence g . x = lim (f # x) by A3, PARTFUN1:def_6; ::_thesis: verum
end;
for x being set holds
( x in dom g iff x in dom (f . 0) ) by A1;
hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim (f # x) ) ) by A2, TARSKI:1; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of X,COMPLEX st dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds
b1 . x = lim (f # x) ) & dom b2 = dom (f . 0) & ( for x being Element of X st x in dom b2 holds
b2 . x = lim (f # x) ) holds
b1 = b2
proof
let g, h be PartFunc of X,COMPLEX; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds
g . x = lim (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds
h . x = lim (f # x) ) implies g = h )
assume that
A4: dom g = dom (f . 0) and
A5: for x being Element of X st x in dom g holds
g . x = lim (f # x) ; ::_thesis: ( not dom h = dom (f . 0) or ex x being Element of X st
( x in dom h & not h . x = lim (f # x) ) or g = h )
assume that
A6: dom h = dom (f . 0) and
A7: for x being Element of X st x in dom h holds
h . x = lim (f # x) ; ::_thesis: g = h
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_h_._x
let x be Element of X; ::_thesis: ( x in dom g implies g . x = h . x )
assume A8: x in dom g ; ::_thesis: g . x = h . x
then g . x = lim (f # x) by A5;
hence g . x = h . x by A4, A6, A7, A8; ::_thesis: verum
end;
hence g = h by A4, A6, PARTFUN1:5; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines lim MESFUN7C:def_10_:_
for X being non empty set
for f being Functional_Sequence of X,COMPLEX
for b3 being PartFunc of X,COMPLEX holds
( b3 = lim f iff ( dom b3 = dom (f . 0) & ( for x being Element of X st x in dom b3 holds
b3 . x = lim (f # x) ) ) );
definition
let X be non empty set ;
let f be Functional_Sequence of X,COMPLEX;
func Re f -> Functional_Sequence of X,REAL means :Def11: :: MESFUN7C:def 11
for n being Nat holds
( dom (it . n) = dom (f . n) & ( for x being Element of X st x in dom (it . n) holds
(it . n) . x = (Re (f # x)) . n ) );
existence
ex b1 being Functional_Sequence of X,REAL st
for n being Nat holds
( dom (b1 . n) = dom (f . n) & ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (Re (f # x)) . n ) )
proof
defpred S1[ Element of NAT , Function] means ( dom $2 = dom (f . $1) & ( for x being Element of X st x in dom $2 holds
$2 . x = (Re (f # x)) . $1 ) );
A1: for n being Element of NAT ex y being Element of PFuncs (X,REAL) st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of PFuncs (X,REAL) st S1[n,y]
deffunc H1( Element of X) -> Element of REAL = (Re (f # $1)) . n;
defpred S2[ set ] means $1 in dom (f . n);
consider g being PartFunc of X,REAL such that
A2: ( ( for x being Element of X holds
( x in dom g iff S2[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from PARTFUN2:sch_2();
take g ; ::_thesis: ( g is Element of PFuncs (X,REAL) & S1[n,g] )
A3: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_(Re_(f_#_x))_._n
let x be Element of X; ::_thesis: ( x in dom g implies g . x = (Re (f # x)) . n )
assume A4: x in dom g ; ::_thesis: g . x = (Re (f # x)) . n
then g /. x = (Re (f # x)) . n by A2;
hence g . x = (Re (f # x)) . n by A4, PARTFUN1:def_6; ::_thesis: verum
end;
for x being set holds
( x in dom g iff x in dom (f . n) ) by A2;
hence ( g is Element of PFuncs (X,REAL) & S1[n,g] ) by A3, PARTFUN1:45, TARSKI:1; ::_thesis: verum
end;
consider g being Function of NAT,(PFuncs (X,REAL)) such that
A5: for n being Element of NAT holds S1[n,g . n] from FUNCT_2:sch_3(A1);
reconsider g = g as Functional_Sequence of X,REAL ;
take g ; ::_thesis: for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Re (f # x)) . n ) )
thus for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Re (f # x)) . n ) ) ::_thesis: verum
proof
let n be Nat; ::_thesis: ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Re (f # x)) . n ) )
n in NAT by ORDINAL1:def_12;
hence ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Re (f # x)) . n ) ) by A5; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being Functional_Sequence of X,REAL st ( for n being Nat holds
( dom (b1 . n) = dom (f . n) & ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (Re (f # x)) . n ) ) ) & ( for n being Nat holds
( dom (b2 . n) = dom (f . n) & ( for x being Element of X st x in dom (b2 . n) holds
(b2 . n) . x = (Re (f # x)) . n ) ) ) holds
b1 = b2
proof
let g, h be Functional_Sequence of X,REAL; ::_thesis: ( ( for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Re (f # x)) . n ) ) ) & ( for n being Nat holds
( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (Re (f # x)) . n ) ) ) implies g = h )
assume A6: for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Re (f # x)) . n ) ) ; ::_thesis: ( ex n being Nat st
( dom (h . n) = dom (f . n) implies ex x being Element of X st
( x in dom (h . n) & not (h . n) . x = (Re (f # x)) . n ) ) or g = h )
assume A7: for n being Nat holds
( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (Re (f # x)) . n ) ) ; ::_thesis: g = h
now__::_thesis:_for_n_being_Element_of_NAT_holds_g_._n_=_h_._n
let n be Element of NAT ; ::_thesis: g . n = h . n
A8: dom (g . n) = dom (f . n) by A6
.= dom (h . n) by A7 ;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(g_._n)_holds_
(g_._n)_._x_=_(h_._n)_._x
let x be Element of X; ::_thesis: ( x in dom (g . n) implies (g . n) . x = (h . n) . x )
assume A9: x in dom (g . n) ; ::_thesis: (g . n) . x = (h . n) . x
then (g . n) . x = (Re (f # x)) . n by A6;
hence (g . n) . x = (h . n) . x by A7, A8, A9; ::_thesis: verum
end;
hence g . n = h . n by A8, PARTFUN1:5; ::_thesis: verum
end;
hence g = h by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def11 defines Re MESFUN7C:def_11_:_
for X being non empty set
for f being Functional_Sequence of X,COMPLEX
for b3 being Functional_Sequence of X,REAL holds
( b3 = Re f iff for n being Nat holds
( dom (b3 . n) = dom (f . n) & ( for x being Element of X st x in dom (b3 . n) holds
(b3 . n) . x = (Re (f # x)) . n ) ) );
registration
let X be non empty set ;
let f be with_the_same_dom Functional_Sequence of X,COMPLEX;
cluster Re f -> with_the_same_dom ;
correctness
coherence
Re f is with_the_same_dom ;
proof
now__::_thesis:_for_k,_l_being_Nat_holds_dom_((Re_f)_._k)_=_dom_((Re_f)_._l)
let k, l be Nat; ::_thesis: dom ((Re f) . k) = dom ((Re f) . l)
dom ((Re f) . k) = dom (f . k) by Def11;
then dom ((Re f) . k) = dom (f . l) by MESFUNC8:def_2;
hence dom ((Re f) . k) = dom ((Re f) . l) by Def11; ::_thesis: verum
end;
hence Re f is with_the_same_dom by MESFUNC8:def_2; ::_thesis: verum
end;
end;
definition
let X be non empty set ;
let f be Functional_Sequence of X,COMPLEX;
func Im f -> Functional_Sequence of X,REAL means :Def12: :: MESFUN7C:def 12
for n being Nat holds
( dom (it . n) = dom (f . n) & ( for x being Element of X st x in dom (it . n) holds
(it . n) . x = (Im (f # x)) . n ) );
existence
ex b1 being Functional_Sequence of X,REAL st
for n being Nat holds
( dom (b1 . n) = dom (f . n) & ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (Im (f # x)) . n ) )
proof
defpred S1[ Element of NAT , Function] means ( dom $2 = dom (f . $1) & ( for x being Element of X st x in dom $2 holds
$2 . x = (Im (f # x)) . $1 ) );
A1: for n being Element of NAT ex y being Element of PFuncs (X,REAL) st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of PFuncs (X,REAL) st S1[n,y]
deffunc H1( Element of X) -> Element of REAL = (Im (f # $1)) . n;
defpred S2[ set ] means $1 in dom (f . n);
consider g being PartFunc of X,REAL such that
A2: ( ( for x being Element of X holds
( x in dom g iff S2[x] ) ) & ( for x being Element of X st x in dom g holds
g /. x = H1(x) ) ) from PARTFUN2:sch_2();
take g ; ::_thesis: ( g is Element of PFuncs (X,REAL) & S1[n,g] )
A3: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_
g_._x_=_(Im_(f_#_x))_._n
let x be Element of X; ::_thesis: ( x in dom g implies g . x = (Im (f # x)) . n )
assume A4: x in dom g ; ::_thesis: g . x = (Im (f # x)) . n
then g /. x = (Im (f # x)) . n by A2;
hence g . x = (Im (f # x)) . n by A4, PARTFUN1:def_6; ::_thesis: verum
end;
for x being set holds
( x in dom g iff x in dom (f . n) ) by A2;
hence ( g is Element of PFuncs (X,REAL) & S1[n,g] ) by A3, PARTFUN1:45, TARSKI:1; ::_thesis: verum
end;
consider g being Function of NAT,(PFuncs (X,REAL)) such that
A5: for n being Element of NAT holds S1[n,g . n] from FUNCT_2:sch_3(A1);
reconsider g = g as Functional_Sequence of X,REAL ;
take g ; ::_thesis: for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) )
thus for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) ) ::_thesis: verum
proof
let n be Nat; ::_thesis: ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) )
n in NAT by ORDINAL1:def_12;
hence ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) ) by A5; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being Functional_Sequence of X,REAL st ( for n being Nat holds
( dom (b1 . n) = dom (f . n) & ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (Im (f # x)) . n ) ) ) & ( for n being Nat holds
( dom (b2 . n) = dom (f . n) & ( for x being Element of X st x in dom (b2 . n) holds
(b2 . n) . x = (Im (f # x)) . n ) ) ) holds
b1 = b2
proof
let g, h be Functional_Sequence of X,REAL; ::_thesis: ( ( for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) ) ) & ( for n being Nat holds
( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (Im (f # x)) . n ) ) ) implies g = h )
assume A6: for n being Nat holds
( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (Im (f # x)) . n ) ) ; ::_thesis: ( ex n being Nat st
( dom (h . n) = dom (f . n) implies ex x being Element of X st
( x in dom (h . n) & not (h . n) . x = (Im (f # x)) . n ) ) or g = h )
assume A7: for n being Nat holds
( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (Im (f # x)) . n ) ) ; ::_thesis: g = h
now__::_thesis:_for_n_being_Element_of_NAT_holds_g_._n_=_h_._n
let n be Element of NAT ; ::_thesis: g . n = h . n
A8: dom (g . n) = dom (f . n) by A6
.= dom (h . n) by A7 ;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(g_._n)_holds_
(g_._n)_._x_=_(h_._n)_._x
let x be Element of X; ::_thesis: ( x in dom (g . n) implies (g . n) . x = (h . n) . x )
assume A9: x in dom (g . n) ; ::_thesis: (g . n) . x = (h . n) . x
then (g . n) . x = (Im (f # x)) . n by A6;
hence (g . n) . x = (h . n) . x by A7, A8, A9; ::_thesis: verum
end;
hence g . n = h . n by A8, PARTFUN1:5; ::_thesis: verum
end;
hence g = h by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines Im MESFUN7C:def_12_:_
for X being non empty set
for f being Functional_Sequence of X,COMPLEX
for b3 being Functional_Sequence of X,REAL holds
( b3 = Im f iff for n being Nat holds
( dom (b3 . n) = dom (f . n) & ( for x being Element of X st x in dom (b3 . n) holds
(b3 . n) . x = (Im (f # x)) . n ) ) );
registration
let X be non empty set ;
let f be with_the_same_dom Functional_Sequence of X,COMPLEX;
cluster Im f -> with_the_same_dom ;
correctness
coherence
Im f is with_the_same_dom ;
proof
now__::_thesis:_for_k,_l_being_Nat_holds_dom_((Im_f)_._k)_=_dom_((Im_f)_._l)
let k, l be Nat; ::_thesis: dom ((Im f) . k) = dom ((Im f) . l)
dom ((Im f) . k) = dom (f . k) by Def12;
then dom ((Im f) . k) = dom (f . l) by MESFUNC8:def_2;
hence dom ((Im f) . k) = dom ((Im f) . l) by Def12; ::_thesis: verum
end;
hence Im f is with_the_same_dom by MESFUNC8:def_2; ::_thesis: verum
end;
end;
theorem Th23: :: MESFUN7C:23
for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for x being Element of X st x in dom (f . 0) holds
( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) )
proof
let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for x being Element of X st x in dom (f . 0) holds
( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) )
let f be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: for x being Element of X st x in dom (f . 0) holds
( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) )
let x be Element of X; ::_thesis: ( x in dom (f . 0) implies ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) ) )
set F = Re f;
set G = Im f;
assume A1: x in dom (f . 0) ; ::_thesis: ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_((Re_f)_#_x)_._n_=_(Re_(f_#_x))_._n_&_((Im_f)_#_x)_._n_=_(Im_(f_#_x))_._n_)
let n be Element of NAT ; ::_thesis: ( ((Re f) # x) . n = (Re (f # x)) . n & ((Im f) # x) . n = (Im (f # x)) . n )
dom ((Re f) . n) = dom (f . n) by Def11;
then A2: dom ((Re f) . n) = dom (f . 0) by MESFUNC8:def_2;
dom ((Im f) . n) = dom (f . n) by Def12;
then A3: dom ((Im f) . n) = dom (f . 0) by MESFUNC8:def_2;
( ((Re f) # x) . n = ((Re f) . n) . x & ((Im f) # x) . n = ((Im f) . n) . x ) by SEQFUNC:def_10;
hence ( ((Re f) # x) . n = (Re (f # x)) . n & ((Im f) # x) . n = (Im (f # x)) . n ) by A1, A2, A3, Def11, Def12; ::_thesis: verum
end;
hence ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) ) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th24: :: MESFUN7C:24
for X being non empty set
for f being Functional_Sequence of X,COMPLEX
for n being Nat holds
( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )
proof
let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,COMPLEX
for n being Nat holds
( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )
let f be Functional_Sequence of X,COMPLEX; ::_thesis: for n being Nat holds
( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )
let n be Nat; ::_thesis: ( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )
A1: n in NAT by ORDINAL1:def_12;
dom ((Re f) . n) = dom (f . n) by Def11;
then A2: dom ((Re f) . n) = dom (Re (f . n)) by COMSEQ_3:def_3;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((Re_f)_._n)_holds_
((Re_f)_._n)_._x_=_(Re_(f_._n))_._x
let x be Element of X; ::_thesis: ( x in dom ((Re f) . n) implies ((Re f) . n) . x = (Re (f . n)) . x )
assume A3: x in dom ((Re f) . n) ; ::_thesis: ((Re f) . n) . x = (Re (f . n)) . x
then (Re (f . n)) . x = Re ((f . n) . x) by A2, COMSEQ_3:def_3;
then A4: (Re (f . n)) . x = Re ((f # x) . n) by Def9;
((Re f) . n) . x = (Re (f # x)) . n by A3, Def11;
hence ((Re f) . n) . x = (Re (f . n)) . x by A1, A4, COMSEQ_3:def_5; ::_thesis: verum
end;
hence (Re f) . n = Re (f . n) by A2, PARTFUN1:5; ::_thesis: (Im f) . n = Im (f . n)
dom ((Im f) . n) = dom (f . n) by Def12;
then A5: dom ((Im f) . n) = dom (Im (f . n)) by COMSEQ_3:def_4;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((Im_f)_._n)_holds_
((Im_f)_._n)_._x_=_(Im_(f_._n))_._x
let x be Element of X; ::_thesis: ( x in dom ((Im f) . n) implies ((Im f) . n) . x = (Im (f . n)) . x )
assume A6: x in dom ((Im f) . n) ; ::_thesis: ((Im f) . n) . x = (Im (f . n)) . x
then (Im (f . n)) . x = Im ((f . n) . x) by A5, COMSEQ_3:def_4;
then A7: (Im (f . n)) . x = Im ((f # x) . n) by Def9;
((Im f) . n) . x = (Im (f # x)) . n by A6, Def12;
hence ((Im f) . n) . x = (Im (f . n)) . x by A1, A7, COMSEQ_3:def_6; ::_thesis: verum
end;
hence (Im f) . n = Im (f . n) by A5, PARTFUN1:5; ::_thesis: verum
end;
theorem Th25: :: MESFUN7C:25
for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,COMPLEX st ( for x being Element of X st x in dom (f . 0) holds
f # x is convergent ) holds
( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) )
proof
let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,COMPLEX st ( for x being Element of X st x in dom (f . 0) holds
f # x is convergent ) holds
( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) )
let f be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: ( ( for x being Element of X st x in dom (f . 0) holds
f # x is convergent ) implies ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) ) )
dom (lim (Re f)) = dom ((Re f) . 0) by MESFUNC8:def_9;
then A1: dom (lim (Re f)) = dom (f . 0) by Def11;
A2: dom (Re (lim f)) = dom (lim f) by COMSEQ_3:def_3;
then A3: dom (lim (Re f)) = dom (Re (lim f)) by A1, Def10;
assume A4: for x being Element of X st x in dom (f . 0) holds
f # x is convergent ; ::_thesis: ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) )
A5: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_(Re_f))_holds_
(lim_(Re_f))_._x_=_(Re_(lim_f))_._x
let x be Element of X; ::_thesis: ( x in dom (lim (Re f)) implies (lim (Re f)) . x = (Re (lim f)) . x )
assume A6: x in dom (lim (Re f)) ; ::_thesis: (lim (Re f)) . x = (Re (lim f)) . x
then A7: f # x is convergent by A4, A1;
then Re (f # x) is convergent ;
then A8: (Re f) # x is convergent by A1, A6, Th23;
(lim (Re f)) . x = lim (R_EAL ((Re f) # x)) by A6, Th14
.= lim ((Re f) # x) by A8, RINFSUP2:14 ;
then (lim (Re f)) . x = lim (Re (f # x)) by A1, A6, Th23;
then A9: (lim (Re f)) . x = Re (lim (f # x)) by A7, COMSEQ_3:41;
(Re (lim f)) . x = Re ((lim f) . x) by A3, A6, COMSEQ_3:def_3;
hence (lim (Re f)) . x = (Re (lim f)) . x by A2, A3, A6, A9, Def10; ::_thesis: verum
end;
Re (lim f) is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:7;
hence lim (Re f) = Re (lim f) by A3, A5, PARTFUN1:5; ::_thesis: lim (Im f) = Im (lim f)
dom (lim (Im f)) = dom ((Im f) . 0) by MESFUNC8:def_9;
then A10: dom (lim (Im f)) = dom (f . 0) by Def12;
A11: dom (Im (lim f)) = dom (lim f) by COMSEQ_3:def_4;
then A12: dom (lim (Im f)) = dom (Im (lim f)) by A10, Def10;
A13: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_(Im_f))_holds_
(lim_(Im_f))_._x_=_(Im_(lim_f))_._x
let x be Element of X; ::_thesis: ( x in dom (lim (Im f)) implies (lim (Im f)) . x = (Im (lim f)) . x )
assume A14: x in dom (lim (Im f)) ; ::_thesis: (lim (Im f)) . x = (Im (lim f)) . x
then A15: f # x is convergent by A4, A10;
then Im (f # x) is convergent ;
then A16: (Im f) # x is convergent by A10, A14, Th23;
(lim (Im f)) . x = lim (R_EAL ((Im f) # x)) by A14, Th14
.= lim ((Im f) # x) by A16, RINFSUP2:14 ;
then (lim (Im f)) . x = lim (Im (f # x)) by A10, A14, Th23;
then A17: (lim (Im f)) . x = Im (lim (f # x)) by A15, COMSEQ_3:41;
(Im (lim f)) . x = Im ((lim f) . x) by A12, A14, COMSEQ_3:def_4;
hence (lim (Im f)) . x = (Im (lim f)) . x by A11, A12, A14, A17, Def10; ::_thesis: verum
end;
Im (lim f) is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:7;
hence lim (Im f) = Im (lim f) by A12, A13, PARTFUN1:5; ::_thesis: verum
end;
theorem :: MESFUN7C:26
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds
f # x is convergent ) implies lim f is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E and
A3: for x being Element of X st x in E holds
f # x is convergent ; ::_thesis: lim f is_measurable_on E
A4: lim (Im f) = R_EAL (Im (lim f)) by A1, A3, Th25;
A5: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_
(Im_f)_#_x_is_convergent
let x be Element of X; ::_thesis: ( x in E implies (Im f) # x is convergent )
assume A6: x in E ; ::_thesis: (Im f) # x is convergent
then f # x is convergent by A3;
then Im (f # x) is convergent ;
hence (Im f) # x is convergent by A1, A6, Th23; ::_thesis: verum
end;
A7: now__::_thesis:_for_n_being_Nat_holds_(Im_f)_._n_is_measurable_on_E
let n be Nat; ::_thesis: (Im f) . n is_measurable_on E
f . n is_measurable_on E by A2;
then Im (f . n) is_measurable_on E by MESFUN6C:def_1;
hence (Im f) . n is_measurable_on E by Th24; ::_thesis: verum
end;
dom ((Im f) . 0) = E by A1, Def12;
then lim (Im f) is_measurable_on E by A7, A5, Th21;
then A8: Im (lim f) is_measurable_on E by A4, MESFUNC6:def_1;
A9: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_
(Re_f)_#_x_is_convergent
let x be Element of X; ::_thesis: ( x in E implies (Re f) # x is convergent )
assume A10: x in E ; ::_thesis: (Re f) # x is convergent
then f # x is convergent by A3;
then Re (f # x) is convergent ;
hence (Re f) # x is convergent by A1, A10, Th23; ::_thesis: verum
end;
A11: now__::_thesis:_for_n_being_Nat_holds_(Re_f)_._n_is_measurable_on_E
let n be Nat; ::_thesis: (Re f) . n is_measurable_on E
f . n is_measurable_on E by A2;
then Re (f . n) is_measurable_on E by MESFUN6C:def_1;
hence (Re f) . n is_measurable_on E by Th24; ::_thesis: verum
end;
A12: lim (Re f) = R_EAL (Re (lim f)) by A1, A3, Th25;
dom ((Re f) . 0) = E by A1, Def11;
then lim (Re f) is_measurable_on E by A11, A9, Th21;
then Re (lim f) is_measurable_on E by A12, MESFUNC6:def_1;
hence lim f is_measurable_on E by A8, MESFUN6C:def_1; ::_thesis: verum
end;
theorem :: MESFUN7C:27
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for g being PartFunc of X,COMPLEX
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for g being PartFunc of X,COMPLEX
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,COMPLEX
for g being PartFunc of X,COMPLEX
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let f be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: for g being PartFunc of X,COMPLEX
for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let g be PartFunc of X,COMPLEX; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is_measurable_on E
let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) implies g is_measurable_on E )
assume that
A1: dom (f . 0) = E and
A2: for n being Nat holds f . n is_measurable_on E and
A3: dom g = E and
A4: for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ; ::_thesis: g is_measurable_on E
A5: now__::_thesis:_for_n_being_Nat_holds_(Im_f)_._n_is_measurable_on_E
let n be Nat; ::_thesis: (Im f) . n is_measurable_on E
f . n is_measurable_on E by A2;
then Im (f . n) is_measurable_on E by MESFUN6C:def_1;
hence (Im f) . n is_measurable_on E by Th24; ::_thesis: verum
end;
A6: dom (Im g) = E by A3, COMSEQ_3:def_4;
A7: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_
(_(Im_f)_#_x_is_convergent_&_(Im_g)_._x_=_lim_((Im_f)_#_x)_)
let x be Element of X; ::_thesis: ( x in E implies ( (Im f) # x is convergent & (Im g) . x = lim ((Im f) # x) ) )
assume A8: x in E ; ::_thesis: ( (Im f) # x is convergent & (Im g) . x = lim ((Im f) # x) )
then A9: f # x is convergent by A4;
then Im (f # x) is convergent ;
hence (Im f) # x is convergent by A1, A8, Th23; ::_thesis: (Im g) . x = lim ((Im f) # x)
g . x = lim (f # x) by A4, A8;
then Im (g . x) = lim (Im (f # x)) by A9, COMSEQ_3:41;
then Im (g . x) = lim ((Im f) # x) by A1, A8, Th23;
hence (Im g) . x = lim ((Im f) # x) by A6, A8, COMSEQ_3:def_4; ::_thesis: verum
end;
dom ((Im f) . 0) = E by A1, Def12;
then R_EAL (Im g) is_measurable_on E by A5, A6, A7, Th22;
then A10: Im g is_measurable_on E by MESFUNC6:def_1;
A11: now__::_thesis:_for_n_being_Nat_holds_(Re_f)_._n_is_measurable_on_E
let n be Nat; ::_thesis: (Re f) . n is_measurable_on E
f . n is_measurable_on E by A2;
then Re (f . n) is_measurable_on E by MESFUN6C:def_1;
hence (Re f) . n is_measurable_on E by Th24; ::_thesis: verum
end;
A12: dom (Re g) = E by A3, COMSEQ_3:def_3;
A13: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_
(_(Re_f)_#_x_is_convergent_&_(Re_g)_._x_=_lim_((Re_f)_#_x)_)
let x be Element of X; ::_thesis: ( x in E implies ( (Re f) # x is convergent & (Re g) . x = lim ((Re f) # x) ) )
assume A14: x in E ; ::_thesis: ( (Re f) # x is convergent & (Re g) . x = lim ((Re f) # x) )
then A15: f # x is convergent by A4;
then Re (f # x) is convergent ;
hence (Re f) # x is convergent by A1, A14, Th23; ::_thesis: (Re g) . x = lim ((Re f) # x)
g . x = lim (f # x) by A4, A14;
then Re (g . x) = lim (Re (f # x)) by A15, COMSEQ_3:41;
then Re (g . x) = lim ((Re f) # x) by A1, A14, Th23;
hence (Re g) . x = lim ((Re f) # x) by A12, A14, COMSEQ_3:def_3; ::_thesis: verum
end;
dom ((Re f) . 0) = E by A1, Def11;
then R_EAL (Re g) is_measurable_on E by A11, A12, A13, Th22;
then Re g is_measurable_on E by MESFUNC6:def_1;
hence g is_measurable_on E by A10, MESFUN6C:def_1; ::_thesis: verum
end;
begin
theorem :: MESFUN7C:28
for X being non empty set
for Y being set
for f being PartFunc of X,COMPLEX
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
proof
let X be non empty set ; ::_thesis: for Y being set
for f being PartFunc of X,COMPLEX
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let Y be set ; ::_thesis: for f being PartFunc of X,COMPLEX
for r being Real holds (r (#) f) | Y = r (#) (f | Y)
let f be PartFunc of X,COMPLEX; ::_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;
then dom ((r (#) f) | Y) = (dom f) /\ Y by VALUED_1:def_5;
then A2: dom ((r (#) f) | Y) = dom (f | Y) by RELAT_1:61;
then A3: dom ((r (#) f) | Y) = dom (r (#) (f | Y)) by VALUED_1:def_5;
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 A5: x in dom (r (#) f) by A1, XBOOLE_0:def_4;
thus ((r (#) f) | Y) . x = (r (#) f) . x by A4, FUNCT_1:47
.= r * (f . x) by A5, VALUED_1:def_5
.= r * ((f | Y) . x) by A2, A4, FUNCT_1:47
.= (r (#) (f | Y)) . x by A3, A4, VALUED_1:def_5 ; ::_thesis: verum
end;
hence (r (#) f) | Y = r (#) (f | Y) by A3, PARTFUN1:5; ::_thesis: verum
end;
Lm1: for X being non empty set
for f being PartFunc of X,COMPLEX holds |.f.| is nonnegative
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX holds |.f.| is nonnegative
let f be PartFunc of X,COMPLEX; ::_thesis: |.f.| is nonnegative
now__::_thesis:_for_x_being_set_st_x_in_dom_|.f.|_holds_
0_<=_|.f.|_._x
let x be set ; ::_thesis: ( x in dom |.f.| implies 0 <= |.f.| . x )
assume x in dom |.f.| ; ::_thesis: 0 <= |.f.| . x
then |.f.| . x = |.(f . x).| by VALUED_1:def_11;
hence 0 <= |.f.| . x by COMPLEX1:46; ::_thesis: verum
end;
hence |.f.| is nonnegative by MESFUNC6:52; ::_thesis: verum
end;
theorem :: MESFUN7C:29
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for k being real number
for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds
|.f.| to_power k is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for k being real number
for E being Element of S st 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 f being PartFunc of X,COMPLEX
for k being real number
for E being Element of S st 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,COMPLEX; ::_thesis: for k being real number
for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds
|.f.| to_power k is_measurable_on E
let k be real number ; ::_thesis: for E being Element of S st 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: ( 0 <= k & E c= dom f & f is_measurable_on E implies |.f.| to_power k is_measurable_on E )
assume that
A1: 0 <= k and
A2: E c= dom f and
A3: f is_measurable_on E ; ::_thesis: |.f.| to_power k is_measurable_on E
A4: |.f.| is nonnegative by Lm1;
E c= dom |.f.| by A2, VALUED_1:def_11;
hence |.f.| to_power k is_measurable_on E by A1, A2, A3, A4, MESFUN6C:29, MESFUN6C:30; ::_thesis: verum
end;
theorem Th30: :: MESFUN7C:30
for X being non empty set
for f, g being PartFunc of X,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g)
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g)
let f, g be PartFunc of X,REAL; ::_thesis: (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g)
A1: dom ((R_EAL f) (#) (R_EAL g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) by MESFUNC1:def_5;
A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((R_EAL_f)_(#)_(R_EAL_g))_holds_
((R_EAL_f)_(#)_(R_EAL_g))_._x_=_(R_EAL_(f_(#)_g))_._x
let x be Element of X; ::_thesis: ( x in dom ((R_EAL f) (#) (R_EAL g)) implies ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x )
assume A3: x in dom ((R_EAL f) (#) (R_EAL g)) ; ::_thesis: ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x
then x in dom (f (#) g) by A1, VALUED_1:def_4;
then A4: (f (#) g) . x = (f . x) * (g . x) by VALUED_1:def_4;
((R_EAL f) (#) (R_EAL g)) . x = ((R_EAL f) . x) * ((R_EAL g) . x) by A3, MESFUNC1:def_5;
hence ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x by A4, EXTREAL1:1; ::_thesis: verum
end;
dom ((R_EAL f) (#) (R_EAL g)) = dom (R_EAL (f (#) g)) by A1, VALUED_1:def_4;
hence (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) by A2, PARTFUN1:5; ::_thesis: verum
end;
theorem Th31: :: MESFUN7C:31
for X being non empty set
for S being SigmaField of X
for E being Element of S
for f, g being PartFunc of X,REAL st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for E being Element of S
for f, g being PartFunc of X,REAL st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let S be SigmaField of X; ::_thesis: for E being Element of S
for f, g being PartFunc of X,REAL st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let E be Element of S; ::_thesis: for f, g being PartFunc of X,REAL st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let f, g be PartFunc of X,REAL; ::_thesis: ( (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E implies f (#) g is_measurable_on E )
assume that
A1: (dom f) /\ (dom g) = E and
A2: ( f is_measurable_on E & g is_measurable_on E ) ; ::_thesis: f (#) g is_measurable_on E
( R_EAL f is_measurable_on E & R_EAL g is_measurable_on E ) by A2, MESFUNC6:def_1;
then (R_EAL f) (#) (R_EAL g) is_measurable_on E by A1, MESFUNC7:15;
then R_EAL (f (#) g) is_measurable_on E by Th30;
hence f (#) g is_measurable_on E by MESFUNC6:def_1; ::_thesis: verum
end;
theorem Th32: :: MESFUN7C:32
for X being non empty set
for f, g being PartFunc of X,COMPLEX holds
( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re 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) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) )
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) )
A1: dom ((Re f) (#) (Re g)) = (dom (Re f)) /\ (dom (Re g)) by VALUED_1:def_4;
A2: dom ((Im f) (#) (Im g)) = (dom (Im f)) /\ (dom (Im g)) by VALUED_1:def_4;
A3: dom (Re f) = dom f by COMSEQ_3:def_3;
A4: dom (Im g) = dom g by COMSEQ_3:def_4;
A5: dom (Re g) = dom g by COMSEQ_3:def_3;
A6: dom (Re (f (#) g)) = dom (f (#) g) by COMSEQ_3:def_3;
then A7: dom (Re (f (#) g)) = (dom f) /\ (dom g) by VALUED_1:def_4;
A8: dom (Im f) = dom f by COMSEQ_3:def_4;
A9: dom (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) = (dom ((Re f) (#) (Re g))) /\ (dom ((Im f) (#) (Im g))) by VALUED_1:12;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Re_(f_(#)_g))_holds_
(Re_(f_(#)_g))_._x_=_(((Re_f)_(#)_(Re_g))_-_((Im_f)_(#)_(Im_g)))_._x
let x be set ; ::_thesis: ( x in dom (Re (f (#) g)) implies (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x )
assume A10: x in dom (Re (f (#) g)) ; ::_thesis: (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im 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 A6, A10, VALUED_1:def_4;
then A11: (Re (f (#) g)) . x = ((Re (f . x)) * (Re (g . x))) - ((Im (f . x)) * (Im (g . x))) by COMPLEX1:9;
x in dom g by A7, A10, XBOOLE_0:def_4;
then A12: ( (Re g) . x = Re (g . x) & (Im g) . x = Im (g . x) ) by A5, A4, COMSEQ_3:def_3, COMSEQ_3:def_4;
x in dom f by A7, A10, XBOOLE_0:def_4;
then ( (Re f) . x = Re (f . x) & (Im f) . x = Im (f . x) ) by A3, A8, COMSEQ_3:def_3, COMSEQ_3:def_4;
then (Re (f (#) g)) . x = (((Re f) (#) (Re g)) . x) - (((Im f) . x) * ((Im g) . x)) by A7, A1, A3, A5, A10, A11, A12, VALUED_1:def_4;
then (Re (f (#) g)) . x = (((Re f) (#) (Re g)) . x) - (((Im f) (#) (Im g)) . x) by A7, A2, A8, A4, A10, VALUED_1:def_4;
hence (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x by A7, A9, A1, A2, A3, A8, A5, A4, A10, VALUED_1:13; ::_thesis: verum
end;
hence Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) by A7, A9, A1, A2, A3, A8, A5, A4, FUNCT_1:2; ::_thesis: Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g))
A13: dom ((Im f) (#) (Re g)) = (dom (Im f)) /\ (dom (Re g)) by VALUED_1:def_4;
A14: dom ((Re f) (#) (Im g)) = (dom (Re f)) /\ (dom (Im g)) by VALUED_1:def_4;
A15: dom (Im (f (#) g)) = dom (f (#) g) by COMSEQ_3:def_4;
then A16: dom (Im (f (#) g)) = (dom f) /\ (dom g) by VALUED_1:def_4;
A17: dom (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) = (dom ((Im f) (#) (Re g))) /\ (dom ((Re f) (#) (Im g))) by VALUED_1:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Im_(f_(#)_g))_holds_
(Im_(f_(#)_g))_._x_=_(((Im_f)_(#)_(Re_g))_+_((Re_f)_(#)_(Im_g)))_._x
let x be set ; ::_thesis: ( x in dom (Im (f (#) g)) implies (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x )
assume A18: x in dom (Im (f (#) g)) ; ::_thesis: (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re 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 A15, A18, VALUED_1:def_4;
then A19: (Im (f (#) g)) . x = ((Im (f . x)) * (Re (g . x))) + ((Re (f . x)) * (Im (g . x))) by COMPLEX1:9;
x in dom g by A16, A18, XBOOLE_0:def_4;
then A20: ( (Re g) . x = Re (g . x) & (Im g) . x = Im (g . x) ) by A5, A4, COMSEQ_3:def_3, COMSEQ_3:def_4;
x in dom f by A16, A18, XBOOLE_0:def_4;
then ( (Re f) . x = Re (f . x) & (Im f) . x = Im (f . x) ) by A3, A8, COMSEQ_3:def_3, COMSEQ_3:def_4;
then (Im (f (#) g)) . x = (((Im f) (#) (Re g)) . x) + (((Re f) . x) * ((Im g) . x)) by A16, A13, A8, A5, A18, A19, A20, VALUED_1:def_4;
then (Im (f (#) g)) . x = (((Im f) (#) (Re g)) . x) + (((Re f) (#) (Im g)) . x) by A16, A14, A3, A4, A18, VALUED_1:def_4;
hence (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x by A16, A17, A13, A14, A3, A8, A5, A4, A18, VALUED_1:def_1; ::_thesis: verum
end;
hence Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) by A16, A17, A13, A14, A3, A8, A5, A4, FUNCT_1:2; ::_thesis: verum
end;
theorem :: MESFUN7C:33
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX
for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX
for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,COMPLEX
for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let f, g be PartFunc of X,COMPLEX; ::_thesis: for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let E be Element of S; ::_thesis: ( (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E implies f (#) g is_measurable_on E )
assume that
A1: (dom f) /\ (dom g) = E and
A2: f is_measurable_on E and
A3: g is_measurable_on E ; ::_thesis: f (#) g is_measurable_on E
A4: dom (Im g) = dom g by COMSEQ_3:def_4;
A5: Im f is_measurable_on E by A2, MESFUN6C:def_1;
A6: dom (Im f) = dom f by COMSEQ_3:def_4;
then A7: dom ((Im f) (#) (Im g)) = E by A1, A4, VALUED_1:def_4;
A8: Im g is_measurable_on E by A3, MESFUN6C:def_1;
then A9: (Im f) (#) (Im g) is_measurable_on E by A1, A5, A6, A4, Th31;
A10: dom (Re f) = dom f by COMSEQ_3:def_3;
A11: dom (Re g) = dom g by COMSEQ_3:def_3;
A12: Re g is_measurable_on E by A3, MESFUN6C:def_1;
then A13: (Im f) (#) (Re g) is_measurable_on E by A1, A5, A6, A11, Th31;
A14: Re f is_measurable_on E by A2, MESFUN6C:def_1;
then (Re f) (#) (Im g) is_measurable_on E by A1, A8, A10, A4, Th31;
then ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) is_measurable_on E by A13, MESFUNC6:26;
then A15: Im (f (#) g) is_measurable_on E by Th32;
(Re f) (#) (Re g) is_measurable_on E by A1, A14, A12, A10, A11, Th31;
then ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) is_measurable_on E by A9, A7, MESFUNC6:29;
then Re (f (#) g) is_measurable_on E by Th32;
hence f (#) g is_measurable_on E by A15, MESFUN6C:def_1; ::_thesis: verum
end;
theorem Th34: :: MESFUN7C: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 ex E being Element of S st
( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds
g . x <= f . x ) holds
Integral (M,g) <= 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, g being PartFunc of X,REAL st ex E being Element of S st
( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds
g . x <= f . x ) holds
Integral (M,g) <= Integral (M,f)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st ex E being Element of S st
( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds
g . x <= f . x ) holds
Integral (M,g) <= Integral (M,f)
let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st ex E being Element of S st
( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds
g . x <= f . x ) holds
Integral (M,g) <= Integral (M,f)
let f, g be PartFunc of X,REAL; ::_thesis: ( ex E being Element of S st
( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds
g . x <= f . x ) implies Integral (M,g) <= Integral (M,f) )
assume that
A1: ex A being Element of S st
( A = dom f & A = dom g & f is_measurable_on A & g is_measurable_on A ) and
A2: ( f is nonnegative & g is nonnegative ) and
A3: for x being Element of X st x in dom g holds
g . x <= f . x ; ::_thesis: Integral (M,g) <= Integral (M,f)
A4: ( Integral (M,g) = integral+ (M,(R_EAL g)) & Integral (M,f) = integral+ (M,(R_EAL f)) ) by A1, A2, MESFUNC6:82;
consider A being Element of S such that
A5: ( A = dom f & A = dom g ) and
A6: ( f is_measurable_on A & g is_measurable_on A ) by A1;
( R_EAL f is_measurable_on A & R_EAL g is_measurable_on A ) by A6, MESFUNC6:def_1;
hence Integral (M,g) <= Integral (M,f) by A2, A3, A5, A4, MESFUNC5:85; ::_thesis: verum
end;
theorem Th35: :: MESFUN7C:35
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
( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & |.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 f is_integrable_on M holds
( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & |.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 f is_integrable_on M holds
( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & |.f.| is_integrable_on M )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & |.f.| is_integrable_on M )
let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M implies ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & |.f.| is_integrable_on M ) )
assume A1: f is_integrable_on M ; ::_thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & |.f.| is_integrable_on M )
then Re f is_integrable_on M by MESFUN6C:def_2;
then R_EAL (Re f) is_integrable_on M by MESFUNC6:def_4;
then consider A1 being Element of S such that
A2: A1 = dom (R_EAL (Re f)) and
A3: R_EAL (Re f) is_measurable_on A1 by MESFUNC5:def_17;
A4: Re f is_measurable_on A1 by A3, MESFUNC6:def_1;
Im f is_integrable_on M by A1, MESFUN6C:def_2;
then R_EAL (Im f) is_integrable_on M by MESFUNC6:def_4;
then consider A2 being Element of S such that
A5: A2 = dom (R_EAL (Im f)) and
A6: R_EAL (Im f) is_measurable_on A2 by MESFUNC5:def_17;
A7: A1 = dom f by A2, COMSEQ_3:def_3;
A2 = dom f by A5, COMSEQ_3:def_4;
then Im f is_measurable_on A1 by A6, A7, MESFUNC6:def_1;
then A8: f is_measurable_on A1 by A4, MESFUN6C:def_1;
hence ex A being Element of S st
( A = dom f & f is_measurable_on A ) by A7; ::_thesis: |.f.| is_integrable_on M
thus |.f.| is_integrable_on M by A1, A7, A8, MESFUN6C:31; ::_thesis: verum
end;
theorem :: MESFUN7C:36
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
ex F being Function of NAT,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
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
ex F being Function of NAT,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
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
ex F being Function of NAT,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
ex F being Function of NAT,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M implies ex F being Function of NAT,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) ) )
assume A1: f is_integrable_on M ; ::_thesis: ex F being Function of NAT,S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
then consider E being Element of S such that
A2: E = dom f and
A3: f is_measurable_on E by Th35;
defpred S1[ Element of NAT , set ] means $2 = E /\ (great_eq_dom (|.f.|,(1 / ($1 + 1))));
A4: dom |.f.| = E by A2, VALUED_1:def_11;
now__::_thesis:_for_x_being_set_st_x_in_E_\_(eq_dom_(|.f.|,0))_holds_
x_in_E_/\_(great_dom_(|.f.|,0))
let x be set ; ::_thesis: ( x in E \ (eq_dom (|.f.|,0)) implies x in E /\ (great_dom (|.f.|,0)) )
reconsider y = |.f.| . x as Real ;
assume A5: x in E \ (eq_dom (|.f.|,0)) ; ::_thesis: x in E /\ (great_dom (|.f.|,0))
then A6: x in E by XBOOLE_0:def_5;
then A7: x in dom |.f.| by A2, VALUED_1:def_11;
not x in eq_dom (|.f.|,0) by A5, XBOOLE_0:def_5;
then not y = 0 by A7, MESFUNC6:7;
then not |.(f . x).| = 0 by A7, VALUED_1:def_11;
then f . x <> 0 by COMPLEX1:5, SQUARE_1:17;
then 0 < |.(f . x).| by COMPLEX1:47;
then 0 < |.f.| . x by A7, VALUED_1:def_11;
then x in great_dom (|.f.|,0) by A7, MESFUNC1:def_13;
hence x in E /\ (great_dom (|.f.|,0)) by A6, XBOOLE_0:def_4; ::_thesis: verum
end;
then A8: E \ (eq_dom (|.f.|,0)) c= E /\ (great_dom (|.f.|,0)) by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_E_/\_(great_dom_(|.f.|,0))_holds_
x_in_E_\_(eq_dom_(|.f.|,0))
let x be set ; ::_thesis: ( x in E /\ (great_dom (|.f.|,0)) implies x in E \ (eq_dom (|.f.|,0)) )
assume A9: x in E /\ (great_dom (|.f.|,0)) ; ::_thesis: x in E \ (eq_dom (|.f.|,0))
then x in great_dom (|.f.|,0) by XBOOLE_0:def_4;
then 0 < |.f.| . x by MESFUNC1:def_13;
then A10: not x in eq_dom (|.f.|,0) by MESFUNC1:def_15;
x in E by A9, XBOOLE_0:def_4;
hence x in E \ (eq_dom (|.f.|,0)) by A10, XBOOLE_0:def_5; ::_thesis: verum
end;
then A11: E /\ (great_dom (|.f.|,0)) c= E \ (eq_dom (|.f.|,0)) by TARSKI:def_3;
A12: |.f.| is_measurable_on E by A2, A3, MESFUN6C:30;
A13: for n being Element of NAT ex Z being Element of S st S1[n,Z]
proof
let n be Element of NAT ; ::_thesis: ex Z being Element of S st S1[n,Z]
take E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ; ::_thesis: ( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S1[n,E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))] )
thus ( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S1[n,E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))] ) by A12, A4, MESFUNC6:13; ::_thesis: verum
end;
consider F being Function of NAT,S such that
A14: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A13);
A15: for n being Nat holds
( F . n in S & M . (F . n) < +infty )
proof
|.f.| is_integrable_on M by A1, Th35;
then A16: Integral (M,|.f.|) < +infty by MESFUNC6:90;
let n be Nat; ::_thesis: ( F . n in S & M . (F . n) < +infty )
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
set z = R_EAL (1 / (n + 1));
A17: F . n1 = E /\ (great_eq_dom (|.f.|,(1 / (n1 + 1)))) by A14;
then reconsider En = F . n as Element of S ;
set h = |.f.| | En;
consider nf being PartFunc of X,REAL such that
A18: nf is_simple_func_in S and
A19: dom nf = En and
A20: for x being set st x in En holds
nf . x = 1 / (n + 1) by MESFUNC6:75;
A21: dom (|.f.| | En) = En by A4, A17, RELAT_1:62, XBOOLE_1:17;
A22: F . n c= great_eq_dom (|.f.|,(1 / (n + 1))) by A17, XBOOLE_1:17;
A23: for x being Element of X st x in dom nf holds
nf . x <= (|.f.| | En) . x
proof
let x be Element of X; ::_thesis: ( x in dom nf implies nf . x <= (|.f.| | En) . x )
assume A24: x in dom nf ; ::_thesis: nf . x <= (|.f.| | En) . x
then (|.f.| | En) . x = |.f.| . x by A19, FUNCT_1:49;
then 1 / (n + 1) <= (|.f.| | En) . x by A22, A19, A24, MESFUNC1:def_14;
hence nf . x <= (|.f.| | En) . x by A19, A20, A24; ::_thesis: verum
end;
(dom |.f.|) /\ En = E /\ En by A2, VALUED_1:def_11;
then A25: (dom |.f.|) /\ En = En by A17, XBOOLE_1:17, XBOOLE_1:28;
|.f.| is_measurable_on En by A12, A17, MESFUNC6:16, XBOOLE_1:17;
then A26: |.f.| | En is_measurable_on En by A25, MESFUNC6:76;
A27: |.f.| | En is nonnegative by Lm1, MESFUNC6:55;
for x being set st x in dom nf holds
nf . x >= 0 by A19, A20;
then A28: nf is nonnegative by MESFUNC6:52;
( |.f.| is nonnegative & |.f.| | E = |.f.| ) by A4, Lm1, RELAT_1:69;
then A29: Integral (M,(|.f.| | En)) <= Integral (M,|.f.|) by A12, A4, A17, MESFUNC6:87, XBOOLE_1:17;
nf is_measurable_on En by A18, MESFUNC6:50;
then Integral (M,nf) <= Integral (M,(|.f.| | En)) by A21, A26, A27, A19, A28, A23, Th34;
then A30: Integral (M,nf) <= Integral (M,|.f.|) by A29, XXREAL_0:2;
A31: ( ((R_EAL (1 / (n + 1))) * (M . En)) / (R_EAL (1 / (n + 1))) = M . En & +infty / (R_EAL (1 / (n + 1))) = +infty ) by XXREAL_3:83, XXREAL_3:88;
Integral (M,nf) = (R_EAL (1 / (n + 1))) * (M . En) by A19, A20, MESFUNC6:97;
then (R_EAL (1 / (n + 1))) * (M . En) < +infty by A16, A30, XXREAL_0:2;
hence ( F . n in S & M . (F . n) < +infty ) by A31, XXREAL_3:80; ::_thesis: verum
end;
take F ; ::_thesis: ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) )
A32: for n being Nat holds F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))
proof
let n be Nat; ::_thesis: F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))
n in NAT by ORDINAL1:def_12;
hence F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) by A14; ::_thesis: verum
end;
then for n being Nat holds F . n = E /\ (great_eq_dom (|.f.|,(0 + (1 / (n + 1))))) ;
then E /\ (great_dom (|.f.|,0)) = union (rng F) by MESFUNC6:11;
hence ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) ) by A2, A32, A11, A8, A15, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th37: :: MESFUN7C:37
for X being non empty set
for f being PartFunc of X,COMPLEX
for A being set holds |.f.| | A = |.(f | A).|
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX
for A being set holds |.f.| | A = |.(f | A).|
let f be PartFunc of X,COMPLEX; ::_thesis: for A being set holds |.f.| | A = |.(f | A).|
let A be set ; ::_thesis: |.f.| | A = |.(f | A).|
dom (|.f.| | A) = (dom |.f.|) /\ A by RELAT_1:61;
then A1: dom (|.f.| | A) = (dom f) /\ A by VALUED_1:def_11;
A2: dom (f | A) = (dom f) /\ A by RELAT_1:61;
then A3: dom |.(f | A).| = (dom f) /\ A by VALUED_1:def_11;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(|.f.|_|_A)_holds_
(|.f.|_|_A)_._x_=_|.(f_|_A).|_._x
let x be Element of X; ::_thesis: ( x in dom (|.f.| | A) implies (|.f.| | A) . x = |.(f | A).| . x )
assume A4: x in dom (|.f.| | A) ; ::_thesis: (|.f.| | A) . x = |.(f | A).| . x
then |.(f | A).| . x = |.((f | A) . x).| by A1, A3, VALUED_1:def_11;
then A5: |.(f | A).| . x = |.(f . x).| by A2, A1, A4, FUNCT_1:47;
x in dom f by A1, A4, XBOOLE_0:def_4;
then A6: x in dom |.f.| by VALUED_1:def_11;
(|.f.| | A) . x = |.f.| . x by A4, FUNCT_1:47;
hence (|.f.| | A) . x = |.(f | A).| . x by A6, A5, VALUED_1:def_11; ::_thesis: verum
end;
hence |.f.| | A = |.(f | A).| by A1, A3, PARTFUN1:5; ::_thesis: verum
end;
theorem Th38: :: MESFUN7C:38
for X being non empty set
for f, g being PartFunc of X,COMPLEX holds
( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,COMPLEX holds
( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
let f, g be PartFunc of X,COMPLEX; ::_thesis: ( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )
dom (|.f.| + |.g.|) = (dom |.f.|) /\ (dom |.g.|) by VALUED_1:def_1;
then dom (|.f.| + |.g.|) = (dom f) /\ (dom |.g.|) by VALUED_1:def_11;
hence dom (|.f.| + |.g.|) = (dom f) /\ (dom g) by VALUED_1:def_11; ::_thesis: dom |.(f + g).| c= dom |.f.|
dom |.(f + g).| = dom (f + g) by VALUED_1:def_11
.= (dom f) /\ (dom g) by VALUED_1:def_1 ;
then dom |.(f + g).| c= dom f by XBOOLE_1:17;
hence dom |.(f + g).| c= dom |.f.| by VALUED_1:def_11; ::_thesis: verum
end;
theorem Th39: :: MESFUN7C:39
for X being non empty set
for f, g being PartFunc of X,COMPLEX holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,COMPLEX holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
let f, g be PartFunc of X,COMPLEX; ::_thesis: (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)
A1: dom |.(f + g).| c= dom |.g.| by Th38;
then A2: dom |.(f + g).| c= dom g by VALUED_1:def_11;
dom (g | (dom |.(f + g).|)) = (dom g) /\ (dom |.(f + g).|) by RELAT_1:61;
then A3: dom (g | (dom |.(f + g).|)) = dom |.(f + g).| by A2, XBOOLE_1:28;
then A4: dom |.(g | (dom |.(f + g).|)).| = dom |.(f + g).| by VALUED_1:def_11;
A5: dom |.(f + g).| c= dom |.f.| by Th38;
then A6: dom |.(f + g).| c= dom f by VALUED_1:def_11;
then (dom |.(f + g).|) /\ (dom |.(f + g).|) c= (dom f) /\ (dom g) by A2, XBOOLE_1:27;
then A7: dom |.(f + g).| c= dom (|.f.| + |.g.|) by Th38;
then A8: dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) = dom |.(f + g).| by RELAT_1:62;
dom (f | (dom |.(f + g).|)) = (dom f) /\ (dom |.(f + g).|) by RELAT_1:61;
then A9: dom (f | (dom |.(f + g).|)) = dom |.(f + g).| by A6, XBOOLE_1:28;
A10: ( |.f.| | (dom |.(f + g).|) = |.(f | (dom |.(f + g).|)).| & |.g.| | (dom |.(f + g).|) = |.(g | (dom |.(f + g).|)).| ) by Th37;
then A11: dom ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) = (dom (f | (dom |.(f + g).|))) /\ (dom (g | (dom |.(f + g).|))) by Th38
.= dom |.(f + g).| by A9, A3 ;
A12: dom |.(f | (dom |.(f + g).|)).| = dom |.(f + g).| by A9, VALUED_1:def_11;
now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((|.f.|_+_|.g.|)_|_(dom_|.(f_+_g).|))_holds_
((|.f.|_+_|.g.|)_|_(dom_|.(f_+_g).|))_._x_=_((|.f.|_|_(dom_|.(f_+_g).|))_+_(|.g.|_|_(dom_|.(f_+_g).|)))_._x
let x be Element of X; ::_thesis: ( x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) implies ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x )
assume A13: x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) ; ::_thesis: ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x
then A14: ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = (|.f.| + |.g.|) . x by FUNCT_1:47
.= (|.f.| . x) + (|.g.| . x) by A7, A8, A13, VALUED_1:def_1
.= |.(f . x).| + (|.g.| . x) by A5, A8, A13, VALUED_1:def_11 ;
A15: x in dom |.(f + g).| by A7, A13, RELAT_1:62;
then ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x = ((|.f.| | (dom |.(f + g).|)) . x) + ((|.g.| | (dom |.(f + g).|)) . x) by A11, VALUED_1:def_1
.= |.((f | (dom |.(f + g).|)) . x).| + (|.(g | (dom |.(f + g).|)).| . x) by A12, A10, A15, VALUED_1:def_11
.= |.((f | (dom |.(f + g).|)) . x).| + |.((g | (dom |.(f + g).|)) . x).| by A4, A15, VALUED_1:def_11
.= |.(f . x).| + |.((g | (dom |.(f + g).|)) . x).| by A15, FUNCT_1:49
.= |.(f . x).| + |.(g . x).| by A15, FUNCT_1:49 ;
hence ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x by A1, A8, A13, A14, VALUED_1:def_11; ::_thesis: verum
end;
hence (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|) by A11, A7, PARTFUN1:5, RELAT_1:62; ::_thesis: verum
end;
theorem Th40: :: MESFUN7C:40
for X being non empty set
for f, g being PartFunc of X,COMPLEX
for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,COMPLEX
for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
let f, g be PartFunc of X,COMPLEX; ::_thesis: for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x
let x be set ; ::_thesis: ( x in dom |.(f + g).| implies |.(f + g).| . x <= (|.f.| + |.g.|) . x )
A1: |.((f . x) + (g . x)).| <= |.(f . x).| + |.(g . x).| by COMPLEX1:56;
assume A2: x in dom |.(f + g).| ; ::_thesis: |.(f + g).| . x <= (|.f.| + |.g.|) . x
then x in dom (f + g) by VALUED_1:def_11;
then A3: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by A1, VALUED_1:def_1;
A4: dom |.(f + g).| c= dom |.g.| by Th38;
then A5: |.(g . x).| = |.g.| . x by A2, VALUED_1:def_11;
x in dom |.g.| by A2, A4;
then A6: x in dom g by VALUED_1:def_11;
A7: dom |.(f + g).| c= dom |.f.| by Th38;
then x in dom |.f.| by A2;
then x in dom f by VALUED_1:def_11;
then x in (dom f) /\ (dom g) by A6, XBOOLE_0:def_4;
then A8: x in dom (|.f.| + |.g.|) by Th38;
|.(f . x).| = |.f.| . x by A2, A7, VALUED_1:def_11;
then |.(f . x).| + |.(g . x).| = (|.f.| + |.g.|) . x by A5, A8, VALUED_1:def_1;
hence |.(f + g).| . x <= (|.f.| + |.g.|) . x by A2, A3, VALUED_1:def_11; ::_thesis: verum
end;
theorem Th41: :: MESFUN7C:41
for X being non empty set
for f, g being PartFunc of X,REAL st ( for x being set st x in dom f holds
f . x <= g . x ) holds
g - f is nonnegative
proof
let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL st ( for x being set st x in dom f holds
f . x <= g . x ) holds
g - f is nonnegative
let f, g be PartFunc of X,REAL; ::_thesis: ( ( for x being set st x in dom f holds
f . x <= g . x ) implies g - f is nonnegative )
assume A1: for x being set st x in dom f holds
f . x <= g . x ; ::_thesis: g - f is nonnegative
now__::_thesis:_for_x_being_set_st_x_in_dom_(g_-_f)_holds_
0_<=_(g_-_f)_._x
let x be set ; ::_thesis: ( x in dom (g - f) implies 0 <= (g - f) . x )
assume A2: x in dom (g - f) ; ::_thesis: 0 <= (g - f) . x
then x in (dom g) /\ (dom f) by VALUED_1:12;
then x in dom f by XBOOLE_0:def_4;
then 0 <= (g . x) - (f . x) by A1, XREAL_1:48;
hence 0 <= (g - f) . x by A2, VALUED_1:13; ::_thesis: verum
end;
hence g - f is nonnegative by MESFUNC6:52; ::_thesis: verum
end;
theorem :: MESFUN7C:42
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (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 + g) & Integral (M,(|.(f + g).| | E)) <= (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 + g) & Integral (M,(|.(f + g).| | E)) <= (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 + g) & Integral (M,(|.(f + g).| | E)) <= (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 + g) & Integral (M,(|.(f + g).| | E)) <= (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 + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
( |.f.| is_integrable_on M & |.g.| is_integrable_on M ) by A1, A2, Th35;
then A3: |.f.| + |.g.| is_integrable_on M by MESFUNC6:100;
Im g is_integrable_on M by A2, MESFUN6C:def_2;
then R_EAL (Im g) is_integrable_on M by MESFUNC6:def_4;
then consider B2 being Element of S such that
A4: ( B2 = dom (R_EAL (Im g)) & R_EAL (Im g) is_measurable_on B2 ) by MESFUNC5:def_17;
Im f is_integrable_on M by A1, MESFUN6C:def_2;
then R_EAL (Im f) is_integrable_on M by MESFUNC6:def_4;
then consider A2 being Element of S such that
A5: ( A2 = dom (R_EAL (Im f)) & R_EAL (Im f) is_measurable_on A2 ) by MESFUNC5:def_17;
Re g is_integrable_on M by A2, MESFUN6C:def_2;
then R_EAL (Re g) is_integrable_on M by MESFUNC6:def_4;
then consider B1 being Element of S such that
A6: B1 = dom (R_EAL (Re g)) and
A7: R_EAL (Re g) is_measurable_on B1 by MESFUNC5:def_17;
A8: B1 = dom g by A6, COMSEQ_3:def_3;
f + g is_integrable_on M by A1, A2, MESFUN6C:33;
then A9: |.(f + g).| is_integrable_on M by Th35;
set G = |.g.|;
set F = |.f.|;
for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x by Th40;
then A10: (|.f.| + |.g.|) - |.(f + g).| is nonnegative by Th41;
Re f is_integrable_on M by A1, MESFUN6C:def_2;
then R_EAL (Re f) is_integrable_on M by MESFUNC6:def_4;
then consider A1 being Element of S such that
A11: A1 = dom (R_EAL (Re f)) and
A12: R_EAL (Re f) is_measurable_on A1 by MESFUNC5:def_17;
A13: A1 = dom f by A11, COMSEQ_3:def_3;
reconsider A = A1 /\ B1 as Element of S ;
Re f is_measurable_on A1 by A12, MESFUNC6:def_1;
then A14: Re f is_measurable_on A by MESFUNC6:16, XBOOLE_1:17;
A15: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1;
then A16: dom |.(f + g).| = A by A13, A8, VALUED_1:def_11;
Re g is_measurable_on B1 by A7, MESFUNC6:def_1;
then A17: Re g is_measurable_on A by MESFUNC6:16, XBOOLE_1:17;
( B2 = dom g & Im g is_measurable_on B2 ) by A4, COMSEQ_3:def_4, MESFUNC6:def_1;
then Im g is_measurable_on A by A8, MESFUNC6:16, XBOOLE_1:17;
then A18: g is_measurable_on A by A17, MESFUN6C:def_1;
then A19: |.g.| is_measurable_on A by A8, MESFUN6C:30, XBOOLE_1:17;
( A2 = dom f & Im f is_measurable_on A2 ) by A5, COMSEQ_3:def_4, MESFUNC6:def_1;
then Im f is_measurable_on A by A13, MESFUNC6:16, XBOOLE_1:17;
then A20: f is_measurable_on A by A14, MESFUN6C:def_1;
then |.f.| is_measurable_on A by A13, MESFUN6C:30, XBOOLE_1:17;
then A21: |.f.| + |.g.| is_measurable_on A by A19, MESFUNC6:26;
A c= A1 by XBOOLE_1:17;
then A22: A c= dom |.f.| by A13, VALUED_1:def_11;
A c= B1 by XBOOLE_1:17;
then A23: A c= dom |.g.| by A8, VALUED_1:def_11;
A24: dom (|.f.| + |.g.|) = (dom |.f.|) /\ (dom |.g.|) by VALUED_1:def_1;
then A25: (dom |.(f + g).|) /\ (dom (|.f.| + |.g.|)) = A by A22, A23, A16, XBOOLE_1:19, XBOOLE_1:28;
|.(f + g).| is_measurable_on A by A13, A8, A20, A18, A15, MESFUN6C:11, MESFUN6C:30;
then consider E being Element of S such that
A26: E = (dom (|.f.| + |.g.|)) /\ (dom |.(f + g).|) and
A27: Integral (M,(|.(f + g).| | E)) <= Integral (M,((|.f.| + |.g.|) | E)) by A21, A3, A25, A9, A10, MESFUN6C:42;
A28: dom (|.g.| | E) = E by A23, A25, A26, RELAT_1:62;
take E ; ::_thesis: ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
thus E = dom (f + g) by A13, A8, A15, A24, A22, A23, A16, A26, XBOOLE_1:19, XBOOLE_1:28; ::_thesis: Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E)))
( |.f.| | E is_integrable_on M & |.g.| | E is_integrable_on M ) by A1, A2, Th35, MESFUNC6:91;
then consider E1 being Element of S such that
A29: E1 = (dom (|.f.| | E)) /\ (dom (|.g.| | E)) and
A30: Integral (M,((|.f.| | E) + (|.g.| | E))) = (Integral (M,((|.f.| | E) | E1))) + (Integral (M,((|.g.| | E) | E1))) by MESFUNC6:101;
dom (|.f.| | E) = E by A22, A25, A26, RELAT_1:62;
then ( (|.f.| | E) | E1 = |.f.| | E & (|.g.| | E) | E1 = |.g.| | E ) by A29, A28, FUNCT_1:51;
hence Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) by A16, A25, A26, A27, A30, Th39; ::_thesis: verum
end;
begin
definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,COMPLEX;
predf is_simple_func_in S means :Def13: :: MESFUN7C:def 13
ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) & ( for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) );
end;
:: deftheorem Def13 defines is_simple_func_in MESFUN7C:def_13_:_
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) & ( for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) ) );
definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,REAL;
let F be Finite_Sep_Sequence of S;
let a be FinSequence of REAL ;
predF,a are_Re-presentation_of f means :Def14: :: MESFUN7C:def 14
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) );
end;
:: deftheorem Def14 defines are_Re-presentation_of MESFUN7C:def_14_:_
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of REAL holds
( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) ) );
definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,COMPLEX;
let F be Finite_Sep_Sequence of S;
let a be FinSequence of COMPLEX ;
predF,a are_Re-presentation_of f means :Def15: :: MESFUN7C:def 15
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) );
end;
:: deftheorem Def15 defines are_Re-presentation_of MESFUN7C:def_15_:_
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for F being Finite_Sep_Sequence of S
for a being FinSequence of COMPLEX holds
( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) ) );
theorem :: MESFUN7C:43
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )
let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )
hereby ::_thesis: ( Re f is_simple_func_in S & Im f is_simple_func_in S implies f is_simple_func_in S )
assume f is_simple_func_in S ; ::_thesis: ( Re f is_simple_func_in S & Im f is_simple_func_in S )
then consider F being Finite_Sep_Sequence of S such that
A1: dom f = union (rng F) and
A2: for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y by Def13;
A3: dom (Im f) = union (rng F) by A1, COMSEQ_3:def_4;
A4: for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
(Im f) . x = (Im f) . y
proof
let n be Nat; ::_thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
(Im f) . x = (Im f) . y
let x, y be Element of X; ::_thesis: ( n in dom F & x in F . n & y in F . n implies (Im f) . x = (Im f) . y )
assume that
A5: n in dom F and
A6: ( x in F . n & y in F . n ) ; ::_thesis: (Im f) . x = (Im f) . y
F . n c= union (rng F) by A5, MESFUNC3:7;
then ( (Im f) . x = Im (f . x) & (Im f) . y = Im (f . y) ) by A3, A6, COMSEQ_3:def_4;
hence (Im f) . x = (Im f) . y by A2, A5, A6; ::_thesis: verum
end;
A7: dom (Re f) = union (rng F) by A1, COMSEQ_3:def_3;
for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
(Re f) . x = (Re f) . y
proof
let n be Nat; ::_thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
(Re f) . x = (Re f) . y
let x, y be Element of X; ::_thesis: ( n in dom F & x in F . n & y in F . n implies (Re f) . x = (Re f) . y )
assume that
A8: n in dom F and
A9: ( x in F . n & y in F . n ) ; ::_thesis: (Re f) . x = (Re f) . y
F . n c= union (rng F) by A8, MESFUNC3:7;
then ( (Re f) . x = Re (f . x) & (Re f) . y = Re (f . y) ) by A7, A9, COMSEQ_3:def_3;
hence (Re f) . x = (Re f) . y by A2, A8, A9; ::_thesis: verum
end;
hence ( Re f is_simple_func_in S & Im f is_simple_func_in S ) by A7, A3, A4, MESFUNC6:def_2; ::_thesis: verum
end;
assume that
A10: Re f is_simple_func_in S and
A11: Im f is_simple_func_in S ; ::_thesis: f is_simple_func_in S
consider F being Finite_Sep_Sequence of S such that
A12: dom (Re f) = union (rng F) and
A13: for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
(Re f) . x = (Re f) . y by A10, MESFUNC6:def_2;
set la = len F;
A14: dom f = union (rng F) by A12, COMSEQ_3:def_3;
consider G being Finite_Sep_Sequence of S such that
A15: dom (Im f) = union (rng G) and
A16: for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(Im f) . x = (Im f) . y by A11, MESFUNC6:def_2;
set lb = len G;
deffunc H1( Nat) -> set = (F . ((($1 -' 1) div (len G)) + 1)) /\ (G . ((($1 -' 1) mod (len G)) + 1));
consider FG being FinSequence such that
A17: len FG = (len F) * (len G) and
A18: for k being Nat st k in dom FG holds
FG . k = H1(k) from FINSEQ_1:sch_2();
A19: dom FG = Seg ((len F) * (len G)) by A17, FINSEQ_1:def_3;
now__::_thesis:_for_k_being_Nat_st_k_in_dom_FG_holds_
FG_._k_in_S
let k be Nat; ::_thesis: ( k in dom FG implies FG . k in S )
A20: len G divides (len F) * (len G) by NAT_D:def_3;
set j = ((k -' 1) mod (len G)) + 1;
set i = ((k -' 1) div (len G)) + 1;
assume A21: k in dom FG ; ::_thesis: FG . k in S
then A22: 1 <= k by FINSEQ_3:25;
then A23: len G > 0 by A17, A21, FINSEQ_3:25;
A24: k <= (len F) * (len G) by A17, A21, FINSEQ_3:25;
then k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;
then A25: (k -' 1) div (len G) <= (((len F) * (len G)) -' 1) div (len G) by NAT_2:24;
A26: 1 <= (len F) * (len G) by A22, A24, XXREAL_0:2;
1 <= len G by A23, NAT_1:14;
then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A26, A20, NAT_2:15;
then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by A25, XREAL_1:19;
then ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A23, NAT_1:14, NAT_D:18;
then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_3:25;
then A27: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:3;
(k -' 1) mod (len G) < len G by A23, NAT_D:1;
then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14;
then ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25;
then G . (((k -' 1) mod (len G)) + 1) in rng G by FUNCT_1:3;
then (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) in S by A27, MEASURE1:34;
hence FG . k in S by A18, A21; ::_thesis: verum
end;
then reconsider FG = FG as FinSequence of S by FINSEQ_2:12;
for k, l being Nat st k in dom FG & l in dom FG & k <> l holds
FG . k misses FG . l
proof
let k, l be Nat; ::_thesis: ( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l )
assume that
A28: k in dom FG and
A29: l in dom FG and
A30: k <> l ; ::_thesis: FG . k misses FG . l
set m = ((l -' 1) mod (len G)) + 1;
set n = ((l -' 1) div (len G)) + 1;
A31: 1 <= k by A28, FINSEQ_3:25;
then A32: len G > 0 by A17, A28, FINSEQ_3:25;
then A33: (l -' 1) + 1 = ((((((l -' 1) div (len G)) + 1) - 1) * (len G)) + ((((l -' 1) mod (len G)) + 1) - 1)) + 1 by NAT_D:2;
A34: k <= (len F) * (len G) by A17, A28, FINSEQ_3:25;
then A35: ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A31, NAT_1:14, NAT_D:def_3;
1 <= len G by A32, NAT_1:14;
then A36: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A35, NAT_2:15;
set j = ((k -' 1) mod (len G)) + 1;
set i = ((k -' 1) div (len G)) + 1;
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A18, A28;
then A37: (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A18, A29
.= (F . (((k -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16
.= (F . (((k -' 1) div (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16
.= ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by XBOOLE_1:16 ;
l <= (len F) * (len G) by A17, A29, FINSEQ_3:25;
then l -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;
then (l -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A36, NAT_2:24;
then ((l -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
then ( ((l -' 1) div (len G)) + 1 >= 1 & ((l -' 1) div (len G)) + 1 <= len F ) by A32, NAT_1:14, NAT_D:18;
then ((l -' 1) div (len G)) + 1 in Seg (len F) ;
then A38: ((l -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3;
1 <= l by A29, FINSEQ_3:25;
then A39: (l - 1) + 1 = (((((l -' 1) div (len G)) + 1) - 1) * (len G)) + (((l -' 1) mod (len G)) + 1) by A33, XREAL_1:233;
(l -' 1) mod (len G) < len G by A32, NAT_D:1;
then ( ((l -' 1) mod (len G)) + 1 >= 1 & ((l -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14;
then ((l -' 1) mod (len G)) + 1 in Seg (len G) ;
then A40: ((l -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def_3;
k -' 1 <= ((len F) * (len G)) -' 1 by A34, NAT_D:42;
then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A36, NAT_2:24;
then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
then ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A32, NAT_1:11, NAT_D:18;
then ((k -' 1) div (len G)) + 1 in Seg (len F) ;
then A41: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3;
(k -' 1) + 1 = ((((((k -' 1) div (len G)) + 1) - 1) * (len G)) + ((((k -' 1) mod (len G)) + 1) - 1)) + 1 by A32, NAT_D:2;
then A42: (k - 1) + 1 = (((((k -' 1) div (len G)) + 1) - 1) * (len G)) + (((k -' 1) mod (len G)) + 1) by A31, XREAL_1:233;
(k -' 1) mod (len G) < len G by A32, NAT_D:1;
then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:11, NAT_1:13;
then ((k -' 1) mod (len G)) + 1 in Seg (len G) ;
then A43: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def_3;
percases ( ((k -' 1) div (len G)) + 1 <> ((l -' 1) div (len G)) + 1 or ((k -' 1) mod (len G)) + 1 <> ((l -' 1) mod (len G)) + 1 ) by A30, A42, A39;
suppose ((k -' 1) div (len G)) + 1 <> ((l -' 1) div (len G)) + 1 ; ::_thesis: FG . k misses FG . l
then F . (((k -' 1) div (len G)) + 1) misses F . (((l -' 1) div (len G)) + 1) by A41, A38, MESFUNC3:4;
then (FG . k) /\ (FG . l) = {} /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A37, XBOOLE_0:def_7;
hence FG . k misses FG . l by XBOOLE_0:def_7; ::_thesis: verum
end;
suppose ((k -' 1) mod (len G)) + 1 <> ((l -' 1) mod (len G)) + 1 ; ::_thesis: FG . k misses FG . l
then G . (((k -' 1) mod (len G)) + 1) misses G . (((l -' 1) mod (len G)) + 1) by A43, A40, MESFUNC3:4;
then (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ {} by A37, XBOOLE_0:def_7;
hence FG . k misses FG . l by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
A44: dom f = union (rng G) by A15, COMSEQ_3:def_4;
A45: dom f = union (rng FG)
proof
thus dom f c= union (rng FG) :: according to XBOOLE_0:def_10 ::_thesis: union (rng FG) c= dom f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom f or z in union (rng FG) )
assume A46: z in dom f ; ::_thesis: z in union (rng FG)
then consider Y being set such that
A47: z in Y and
A48: Y in rng F by A14, TARSKI:def_4;
consider Z being set such that
A49: z in Z and
A50: Z in rng G by A44, A46, TARSKI:def_4;
consider j being Nat such that
A51: j in dom G and
A52: Z = G . j by A50, FINSEQ_2:10;
consider i being Nat such that
A53: i in dom F and
A54: F . i = Y by A48, FINSEQ_2:10;
1 <= i by A53, FINSEQ_3:25;
then consider i9 being Nat such that
A55: i = 1 + i9 by NAT_1:10;
set k = ((i - 1) * (len G)) + j;
reconsider k = ((i - 1) * (len G)) + j as Nat by A55;
i <= len F by A53, FINSEQ_3:25;
then i - 1 <= (len F) - 1 by XREAL_1:9;
then (i - 1) * (len G) <= ((len F) - 1) * (len G) by XREAL_1:64;
then A56: k <= (((len F) - 1) * (len G)) + j by XREAL_1:6;
A57: j <= len G by A51, FINSEQ_3:25;
then (((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G) by XREAL_1:6;
then A58: k <= (len F) * (len G) by A56, XXREAL_0:2;
A59: 1 <= j by A51, FINSEQ_3:25;
then consider j9 being Nat such that
A60: j = 1 + j9 by NAT_1:10;
A61: j9 < len G by A57, A60, NAT_1:13;
A62: k >= j by A55, NAT_1:11;
then A63: k -' 1 = k - 1 by A59, XREAL_1:233, XXREAL_0:2
.= (i9 * (len G)) + j9 by A55, A60 ;
then A64: i = ((k -' 1) div (len G)) + 1 by A55, A61, NAT_D:def_1;
A65: k >= 1 by A59, A62, XXREAL_0:2;
then A66: k in Seg ((len F) * (len G)) by A58, FINSEQ_1:1;
A67: j = ((k -' 1) mod (len G)) + 1 by A60, A63, A61, NAT_D:def_2;
k in dom FG by A17, A65, A58, FINSEQ_3:25;
then A68: FG . k in rng FG by FUNCT_1:def_3;
z in (F . i) /\ (G . j) by A47, A54, A49, A52, XBOOLE_0:def_4;
then z in FG . k by A18, A19, A64, A67, A66;
hence z in union (rng FG) by A68, TARSKI:def_4; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union (rng FG) or z in dom f )
assume z in union (rng FG) ; ::_thesis: z in dom f
then consider Y being set such that
A69: z in Y and
A70: Y in rng FG by TARSKI:def_4;
consider k being Nat such that
A71: k in dom FG and
A72: FG . k = Y by A70, FINSEQ_2:10;
A73: 1 <= k by A71, FINSEQ_3:25;
then A74: len G > 0 by A17, A71, FINSEQ_3:25;
then A75: 1 <= len G by NAT_1:14;
A76: k <= (len F) * (len G) by A17, A71, FINSEQ_3:25;
then ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A73, NAT_1:14, NAT_D:def_3;
then A77: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A75, NAT_2:15;
set j = ((k -' 1) mod (len G)) + 1;
set i = ((k -' 1) div (len G)) + 1;
k -' 1 <= ((len F) * (len G)) -' 1 by A76, NAT_D:42;
then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A77, NAT_2:24;
then A78: ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) ) by NAT_1:14, XREAL_1:19;
((len F) * (len G)) div (len G) = len F by A74, NAT_D:18;
then ((k -' 1) div (len G)) + 1 in dom F by A78, FINSEQ_3:25;
then A79: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:def_3;
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A18, A71;
then z in F . (((k -' 1) div (len G)) + 1) by A69, A72, XBOOLE_0:def_4;
hence z in dom f by A14, A79, TARSKI:def_4; ::_thesis: verum
end;
for k being Nat
for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds
f . x = f . y
proof
let k be Nat; ::_thesis: for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds
f . x = f . y
let x, y be Element of X; ::_thesis: ( k in dom FG & x in FG . k & y in FG . k implies f . x = f . y )
set i = ((k -' 1) div (len G)) + 1;
set j = ((k -' 1) mod (len G)) + 1;
assume that
A80: k in dom FG and
A81: ( x in FG . k & y in FG . k ) ; ::_thesis: f . x = f . y
A82: FG . k c= union (rng FG) by A80, MESFUNC3:7;
then FG . k c= dom (Im f) by A45, COMSEQ_3:def_4;
then A83: ( (Im f) . x = Im (f . x) & (Im f) . y = Im (f . y) ) by A81, COMSEQ_3:def_4;
A84: 1 <= k by A80, FINSEQ_3:25;
then A85: len G > 0 by A17, A80, FINSEQ_3:25;
then (k -' 1) mod (len G) < len G by NAT_D:1;
then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14;
then A86: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25;
FG . k c= dom (Re f) by A45, A82, COMSEQ_3:def_3;
then A87: ( (Re f) . x = Re (f . x) & (Re f) . y = Re (f . y) ) by A81, COMSEQ_3:def_3;
A88: k <= (len F) * (len G) by A17, A80, FINSEQ_3:25;
then A89: k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;
A90: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A18, A80;
then ( x in G . (((k -' 1) mod (len G)) + 1) & y in G . (((k -' 1) mod (len G)) + 1) ) by A81, XBOOLE_0:def_4;
then A91: Im (f . x) = Im (f . y) by A16, A86, A83;
A92: ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A84, A88, NAT_1:14, NAT_D:def_3;
1 <= len G by A85, NAT_1:14;
then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A92, NAT_2:15;
then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A89, NAT_2:24;
then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19;
then ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A85, NAT_1:14, NAT_D:18;
then A93: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_3:25;
( x in F . (((k -' 1) div (len G)) + 1) & y in F . (((k -' 1) div (len G)) + 1) ) by A81, A90, XBOOLE_0:def_4;
then Re (f . x) = Re (f . y) by A13, A93, A87;
hence f . x = f . y by A91, COMPLEX1:def_3; ::_thesis: verum
end;
hence f is_simple_func_in S by A45, Def13; ::_thesis: verum
end;
theorem Th44: :: MESFUN7C:44
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) )
let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_simple_func_in S implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) ) )
assume f is_simple_func_in S ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) )
then consider F being Finite_Sep_Sequence of S such that
A1: dom f = union (rng F) and
A2: for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y by Def13;
defpred S1[ set , set ] means for x being set st x in F . $1 holds
$2 = f . x;
A3: for k being Nat st k in Seg (len F) holds
ex y being Element of COMPLEX st S1[k,y]
proof
let k be Nat; ::_thesis: ( k in Seg (len F) implies ex y being Element of COMPLEX st S1[k,y] )
assume k in Seg (len F) ; ::_thesis: ex y being Element of COMPLEX st S1[k,y]
then A4: k in dom F by FINSEQ_1:def_3;
then A5: F . k in rng F by FUNCT_1:3;
percases ( F . k = {} or F . k <> {} ) ;
supposeA6: F . k = {} ; ::_thesis: ex y being Element of COMPLEX st S1[k,y]
reconsider y = 0 as Element of COMPLEX by NUMBERS:11, TARSKI:def_3;
take y ; ::_thesis: S1[k,y]
thus S1[k,y] by A6; ::_thesis: verum
end;
suppose F . k <> {} ; ::_thesis: ex y being Element of COMPLEX st S1[k,y]
then consider x1 being set such that
A7: x1 in F . k by XBOOLE_0:def_1;
x1 in dom f by A1, A5, A7, TARSKI:def_4;
then f . x1 in rng f by FUNCT_1:3;
then reconsider y = f . x1 as Element of COMPLEX ;
take y ; ::_thesis: S1[k,y]
hereby ::_thesis: verum
let x be set ; ::_thesis: ( x in F . k implies y = f . x )
A8: rng F c= bool X by XBOOLE_1:1;
assume x in F . k ; ::_thesis: y = f . x
hence y = f . x by A2, A4, A5, A7, A8; ::_thesis: verum
end;
end;
end;
end;
consider a being FinSequence of COMPLEX such that
A9: ( dom a = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S1[k,a . k] ) ) from FINSEQ_1:sch_5(A3);
take F ; ::_thesis: ex a being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) )
take a ; ::_thesis: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) )
now__::_thesis:_for_n_being_Nat_st_n_in_dom_F_holds_
for_x_being_set_st_x_in_F_._n_holds_
a_._n_=_f_._x
let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds
a . n = f . x )
assume n in dom F ; ::_thesis: for x being set st x in F . n holds
a . n = f . x
then n in Seg (len F) by FINSEQ_1:def_3;
hence for x being set st x in F . n holds
a . n = f . x by A9; ::_thesis: verum
end;
hence ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) ) by A1, A9, FINSEQ_1:def_3; ::_thesis: verum
end;
theorem Th45: :: MESFUN7C:45
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f )
let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f )
hereby ::_thesis: ( ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f implies f is_simple_func_in S )
assume f is_simple_func_in S ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f
then consider F being Finite_Sep_Sequence of S, a being FinSequence of COMPLEX such that
A1: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) ) by Th44;
take F = F; ::_thesis: ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f
take a = a; ::_thesis: F,a are_Re-presentation_of f
thus F,a are_Re-presentation_of f by A1, Def15; ::_thesis: verum
end;
given F being Finite_Sep_Sequence of S, a being FinSequence of COMPLEX such that A2: F,a are_Re-presentation_of f ; ::_thesis: f is_simple_func_in S
A3: for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y
proof
let n be Nat; ::_thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y
let x, y be Element of X; ::_thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y )
assume that
A4: n in dom F and
A5: x in F . n and
A6: y in F . n ; ::_thesis: f . x = f . y
f . x = a . n by A2, A4, A5, Def15;
hence f . x = f . y by A2, A4, A6, Def15; ::_thesis: verum
end;
dom f = union (rng F) by A2, Def15;
hence f is_simple_func_in S by A3, Def13; ::_thesis: verum
end;
theorem Th46: :: MESFUN7C:46
for c being FinSequence of COMPLEX
for n being Nat st n in dom (Re c) holds
(Re c) . n = Re (c . n)
proof
let c be FinSequence of COMPLEX ; ::_thesis: for n being Nat st n in dom (Re c) holds
(Re c) . n = Re (c . n)
let n be Nat; ::_thesis: ( n in dom (Re c) implies (Re c) . n = Re (c . n) )
A1: ((1 / 2) * (c *')) . n = (1 / 2) * ((c *') . n) by COMPLSP2:16;
( len ((1 / 2) * c) = len c & len ((1 / 2) * (c *')) = len (c *') ) by COMPLSP2:3;
then A2: len ((1 / 2) * c) = len ((1 / 2) * (c *')) by COMPLSP2:def_1;
len (c *') = len c by COMPLSP2:def_1;
then ( n in NAT & (1 / 2) * (c + (c *')) = ((1 / 2) * c) + ((1 / 2) * (c *')) ) by COMPLSP2:30, ORDINAL1:def_12;
then A3: (Re c) . n = (((1 / 2) * c) . n) + (((1 / 2) * (c *')) . n) by A2, COMPLSP2:26;
assume A4: n in dom (Re c) ; ::_thesis: (Re c) . n = Re (c . n)
then n <= len (Re c) by FINSEQ_3:25;
then A5: n <= len c by COMPLSP2:48;
1 <= n by A4, FINSEQ_3:25;
then ((1 / 2) * (c *')) . n = (1 / 2) * ((c . n) *') by A5, A1, COMPLSP2:def_1;
then A6: (Re c) . n = ((1 / 2) * (c . n)) + ((1 / 2) * ((c . n) *')) by A3, COMPLSP2:16;
c . n = (Re (c . n)) + ((Im (c . n)) * *) by COMPLEX1:13;
hence (Re c) . n = Re (c . n) by A6; ::_thesis: verum
end;
theorem Th47: :: MESFUN7C:47
for c being FinSequence of COMPLEX
for n being Nat st n in dom (Im c) holds
(Im c) . n = Im (c . n)
proof
let c be FinSequence of COMPLEX ; ::_thesis: for n being Nat st n in dom (Im c) holds
(Im c) . n = Im (c . n)
let n be Nat; ::_thesis: ( n in dom (Im c) implies (Im c) . n = Im (c . n) )
assume A1: n in dom (Im c) ; ::_thesis: (Im c) . n = Im (c . n)
then A2: 1 <= n by FINSEQ_3:25;
n <= len (Im c) by A1, FINSEQ_3:25;
then A3: n <= len c by COMPLSP2:48;
A4: ((- ((1 / 2) * **)) * (c *')) . n = (- ((1 / 2) * **)) * ((c *') . n) by COMPLSP2:16
.= (- ((1 / 2) * **)) * ((c . n) *') by A2, A3, COMPLSP2:def_1 ;
( len ((- ((1 / 2) * **)) * c) = len c & len ((- ((1 / 2) * **)) * (c *')) = len (c *') ) by COMPLSP2:3;
then A5: len ((- ((1 / 2) * **)) * c) = len ((- ((1 / 2) * **)) * (c *')) by COMPLSP2:def_1;
len (c *') = len c by COMPLSP2:def_1;
then ( n in NAT & (- ((1 / 2) * **)) * (c - (c *')) = ((- ((1 / 2) * **)) * c) - ((- ((1 / 2) * **)) * (c *')) ) by COMPLSP2:43, ORDINAL1:def_12;
then (Im c) . n = (((- ((1 / 2) * **)) * c) . n) - (((- ((1 / 2) * **)) * (c *')) . n) by A5, COMPLSP2:25;
then A6: (Im c) . n = ((- ((1 / 2) * **)) * (c . n)) - ((- ((1 / 2) * **)) * ((c . n) *')) by A4, COMPLSP2:16;
(c . n) - ((c . n) *') = ((Re (c . n)) + ((Im (c . n)) * **)) - ((Re (c . n)) - ((Im (c . n)) * **)) by COMPLEX1:13;
hence (Im c) . n = Im (c . n) by A6; ::_thesis: verum
end;
theorem Th48: :: MESFUN7C:48
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for F being Finite_Sep_Sequence of S
for a being FinSequence of COMPLEX holds
( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for F being Finite_Sep_Sequence of S
for a being FinSequence of COMPLEX holds
( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX
for F being Finite_Sep_Sequence of S
for a being FinSequence of COMPLEX holds
( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) )
let f be PartFunc of X,COMPLEX; ::_thesis: for F being Finite_Sep_Sequence of S
for a being FinSequence of COMPLEX holds
( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) )
let F be Finite_Sep_Sequence of S; ::_thesis: for a being FinSequence of COMPLEX holds
( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) )
let a be FinSequence of COMPLEX ; ::_thesis: ( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) )
hereby ::_thesis: ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f implies F,a are_Re-presentation_of f )
assume A1: F,a are_Re-presentation_of f ; ::_thesis: ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f )
len (Im a) = len a by COMPLSP2:48;
then dom (Im a) = Seg (len a) by FINSEQ_1:def_3;
then dom (Im a) = dom a by FINSEQ_1:def_3;
then A2: dom F = dom (Im a) by A1, Def15;
dom (Im f) = dom f by COMSEQ_3:def_4;
then A3: dom (Im f) = union (rng F) by A1, Def15;
A4: for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im a) . n
proof
let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds
(Im f) . x = (Im a) . n )
assume A5: n in dom F ; ::_thesis: for x being set st x in F . n holds
(Im f) . x = (Im a) . n
let x be set ; ::_thesis: ( x in F . n implies (Im f) . x = (Im a) . n )
assume A6: x in F . n ; ::_thesis: (Im f) . x = (Im a) . n
F . n c= union (rng F) by A5, MESFUNC3:7;
then x in dom (Im f) by A3, A6;
then A7: (Im f) . x = Im (f . x) by COMSEQ_3:def_4;
Im (f . x) = Im (a . n) by A1, A5, A6, Def15;
hence (Im f) . x = (Im a) . n by A2, A5, A7, Th47; ::_thesis: verum
end;
len (Re a) = len a by COMPLSP2:48;
then dom (Re a) = Seg (len a) by FINSEQ_1:def_3;
then dom (Re a) = dom a by FINSEQ_1:def_3;
then A8: dom F = dom (Re a) by A1, Def15;
dom (Re f) = dom f by COMSEQ_3:def_3;
then A9: dom (Re f) = union (rng F) by A1, Def15;
for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re a) . n
proof
let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds
(Re f) . x = (Re a) . n )
assume A10: n in dom F ; ::_thesis: for x being set st x in F . n holds
(Re f) . x = (Re a) . n
let x be set ; ::_thesis: ( x in F . n implies (Re f) . x = (Re a) . n )
assume A11: x in F . n ; ::_thesis: (Re f) . x = (Re a) . n
F . n c= union (rng F) by A10, MESFUNC3:7;
then x in dom (Re f) by A9, A11;
then A12: (Re f) . x = Re (f . x) by COMSEQ_3:def_3;
Re (f . x) = Re (a . n) by A1, A10, A11, Def15;
hence (Re f) . x = (Re a) . n by A8, A10, A12, Th46; ::_thesis: verum
end;
hence ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) by A9, A3, A8, A2, A4, Def14; ::_thesis: verum
end;
assume that
A13: F, Re a are_Re-presentation_of Re f and
A14: F, Im a are_Re-presentation_of Im f ; ::_thesis: F,a are_Re-presentation_of f
A15: dom F = dom (Re a) by A13, Def14;
A16: dom (Re f) = union (rng F) by A13, Def14;
then A17: dom f = union (rng F) by COMSEQ_3:def_3;
A18: dom F = dom (Im a) by A14, Def14;
A19: dom (Im f) = union (rng F) by A14, Def14;
A20: for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n
proof
let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds
f . x = a . n )
assume A21: n in dom F ; ::_thesis: for x being set st x in F . n holds
f . x = a . n
let x be set ; ::_thesis: ( x in F . n implies f . x = a . n )
assume A22: x in F . n ; ::_thesis: f . x = a . n
A23: F . n c= union (rng F) by A21, MESFUNC3:7;
then x in dom (Im f) by A19, A22;
then A24: (Im f) . x = Im (f . x) by COMSEQ_3:def_4;
x in dom (Re f) by A16, A22, A23;
then A25: (Re f) . x = Re (f . x) by COMSEQ_3:def_3;
(Im f) . x = (Im a) . n by A14, A21, A22, Def14;
then A26: Im (f . x) = Im (a . n) by A18, A21, A24, Th47;
(Re f) . x = (Re a) . n by A13, A21, A22, Def14;
then Re (f . x) = Re (a . n) by A15, A21, A25, Th46;
hence f . x = a . n by A26, COMPLEX1:def_3; ::_thesis: verum
end;
len (Re a) = len a by COMPLSP2:48;
then dom (Re a) = Seg (len a) by FINSEQ_1:def_3;
then dom F = dom a by A15, FINSEQ_1:def_3;
hence F,a are_Re-presentation_of f by A17, A20, Def15; ::_thesis: verum
end;
theorem :: MESFUN7C:49
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n ) ) )
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n ) ) )
let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n ) ) )
let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n ) ) )
hereby ::_thesis: ( ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n ) ) implies f is_simple_func_in S )
assume f is_simple_func_in S ; ::_thesis: ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n ) )
then consider F being Finite_Sep_Sequence of S, c being FinSequence of COMPLEX such that
A1: F,c are_Re-presentation_of f by Th45;
F, Im c are_Re-presentation_of Im f by A1, Th48;
then A2: for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n by Def14;
F, Re c are_Re-presentation_of Re f by A1, Th48;
then A3: for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n by Def14;
( dom f = union (rng F) & dom F = dom c ) by A1, Def15;
hence ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n ) ) by A3, A2; ::_thesis: verum
end;
given F being Finite_Sep_Sequence of S, c being FinSequence of COMPLEX such that A4: dom f = union (rng F) and
A5: dom F = dom c and
A6: for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n and
A7: for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n ; ::_thesis: f is_simple_func_in S
A8: dom (Im f) = union (rng F) by A4, COMSEQ_3:def_4;
len (Im c) = len c by COMPLSP2:48;
then dom (Im c) = Seg (len c) by FINSEQ_1:def_3;
then A9: dom F = dom (Im c) by A5, FINSEQ_1:def_3;
len (Re c) = len c by COMPLSP2:48;
then dom (Re c) = Seg (len c) by FINSEQ_1:def_3;
then A10: dom F = dom (Re c) by A5, FINSEQ_1:def_3;
A11: dom (Re f) = union (rng F) by A4, COMSEQ_3:def_3;
for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = c . n
proof
let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds
f . x = c . n )
assume A12: n in dom F ; ::_thesis: for x being set st x in F . n holds
f . x = c . n
let x be set ; ::_thesis: ( x in F . n implies f . x = c . n )
assume A13: x in F . n ; ::_thesis: f . x = c . n
A14: F . n c= union (rng F) by A12, MESFUNC3:7;
then x in dom (Im f) by A8, A13;
then A15: (Im f) . x = Im (f . x) by COMSEQ_3:def_4;
x in dom (Re f) by A11, A13, A14;
then A16: (Re f) . x = Re (f . x) by COMSEQ_3:def_3;
(Im f) . x = (Im c) . n by A7, A12, A13;
then A17: Im (f . x) = Im (c . n) by A9, A12, A15, Th47;
(Re f) . x = (Re c) . n by A6, A12, A13;
then Re (f . x) = Re (c . n) by A10, A12, A16, Th46;
hence f . x = c . n by A17, COMPLEX1:def_3; ::_thesis: verum
end;
then F,c are_Re-presentation_of f by A4, A5, Def15;
hence f is_simple_func_in S by Th45; ::_thesis: verum
end;
*