:: INTEGR15 semantic presentation
begin
definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL;
let D be Division of A;
mode middle_volume of f,D -> FinSequence of REAL means :Def1: :: INTEGR15:def 1
( len it = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & it . i = r * (vol (divset (D,i))) ) ) );
correctness
existence
ex b1 being FinSequence of REAL st
( len b1 = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & b1 . i = r * (vol (divset (D,i))) ) ) );
proof
defpred S1[ Nat, Element of REAL ] means ex r being Element of REAL st
( r in rng (f | (divset (D,$1))) & $2 = r * (vol (divset (D,$1))) );
A1: Seg (len D) = dom D by FINSEQ_1:def_3;
A2: for k being Nat st k in Seg (len D) holds
ex x being Element of REAL st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len D) implies ex x being Element of REAL st S1[k,x] )
assume k in Seg (len D) ; ::_thesis: ex x being Element of REAL st S1[k,x]
then A3: k in dom D by FINSEQ_1:def_3;
dom f = A by FUNCT_2:def_1;
then dom (f | (divset (D,k))) = divset (D,k) by A3, INTEGRA1:8, RELAT_1:62;
then not rng (f | (divset (D,k))) is empty by RELAT_1:42;
then consider r being set such that
A4: r in rng (f | (divset (D,k))) by XBOOLE_0:def_1;
reconsider r = r as Element of REAL by A4;
r * (vol (divset (D,k))) is Element of REAL ;
hence ex x being Element of REAL st S1[k,x] by A4; ::_thesis: verum
end;
consider p being FinSequence of REAL such that
A5: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds
S1[k,p . k] ) ) from FINSEQ_1:sch_5(A2);
len p = len D by A5, FINSEQ_1:def_3;
hence ex b1 being FinSequence of REAL st
( len b1 = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & b1 . i = r * (vol (divset (D,i))) ) ) ) by A5, A1; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines middle_volume INTEGR15:def_1_:_
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for b4 being FinSequence of REAL holds
( b4 is middle_volume of f,D iff ( len b4 = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & b4 . i = r * (vol (divset (D,i))) ) ) ) );
Lm1: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_below & i in dom D holds
(lower_volume (f,D)) . i <= F . i
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_below & i in dom D holds
(lower_volume (f,D)) . i <= F . i
let f be Function of A,REAL; ::_thesis: for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_below & i in dom D holds
(lower_volume (f,D)) . i <= F . i
let D be Division of A; ::_thesis: for F being middle_volume of f,D
for i being Nat st f | A is bounded_below & i in dom D holds
(lower_volume (f,D)) . i <= F . i
let F be middle_volume of f,D; ::_thesis: for i being Nat st f | A is bounded_below & i in dom D holds
(lower_volume (f,D)) . i <= F . i
let i be Nat; ::_thesis: ( f | A is bounded_below & i in dom D implies (lower_volume (f,D)) . i <= F . i )
assume that
A1: f | A is bounded_below and
A2: i in dom D ; ::_thesis: (lower_volume (f,D)) . i <= F . i
A3: (lower_volume (f,D)) . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A2, INTEGRA1:def_7;
consider r being Element of REAL such that
A4: r in rng (f | (divset (D,i))) and
A5: F . i = r * (vol (divset (D,i))) by A2, Def1;
rng f is bounded_below by A1, INTEGRA1:11;
then rng (f | (divset (D,i))) is bounded_below by RELAT_1:70, XXREAL_2:44;
then ( 0 <= vol (divset (D,i)) & lower_bound (rng (f | (divset (D,i)))) <= r ) by A4, INTEGRA1:9, SEQ_4:def_2;
hence (lower_volume (f,D)) . i <= F . i by A5, A3, XREAL_1:64; ::_thesis: verum
end;
Lm2: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )
let f be Function of A,REAL; ::_thesis: for D being Division of A
for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )
let D be Division of A; ::_thesis: for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )
let e be Real; ::_thesis: ( f | A is bounded_below & 0 < e implies ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) )
assume that
A1: f | A is bounded_below and
A2: 0 < e ; ::_thesis: ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )
defpred S1[ Nat, Element of REAL ] means ex r being Element of REAL st
( r in rng (f | (divset (D,$1))) & $2 = r * (vol (divset (D,$1))) & (lower_volume (f,D)) . $1 <= $2 & $2 < ((lower_volume (f,D)) . $1) + e );
A3: for k being Nat st k in Seg (len D) holds
ex x being Element of REAL st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len D) implies ex x being Element of REAL st S1[k,x] )
assume k in Seg (len D) ; ::_thesis: ex x being Element of REAL st S1[k,x]
then A4: k in dom D by FINSEQ_1:def_3;
dom f = A by FUNCT_2:def_1;
then dom (f | (divset (D,k))) = divset (D,k) by A4, INTEGRA1:8, RELAT_1:62;
then A5: not rng (f | (divset (D,k))) is empty by RELAT_1:42;
rng f is bounded_below by A1, INTEGRA1:11;
then A6: rng (f | (divset (D,k))) is bounded_below by RELAT_1:70, XXREAL_2:44;
percases ( vol (divset (D,k)) = 0 or vol (divset (D,k)) <> 0 ) ;
supposeA7: vol (divset (D,k)) = 0 ; ::_thesis: ex x being Element of REAL st S1[k,x]
consider r being set such that
A8: r in rng (f | (divset (D,k))) by A5, XBOOLE_0:def_1;
reconsider r = r as Element of REAL by A8;
reconsider x = r * (vol (divset (D,k))) as Element of REAL ;
A9: (lower_volume (f,D)) . k = (lower_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k))) by A4, INTEGRA1:def_7
.= 0 by A7 ;
then x < ((lower_volume (f,D)) . k) + e by A2, A7;
hence ex x being Element of REAL st S1[k,x] by A7, A8, A9; ::_thesis: verum
end;
supposeA10: vol (divset (D,k)) <> 0 ; ::_thesis: ex x being Element of REAL st S1[k,x]
set l = lower_bound (rng (f | (divset (D,k))));
set e1 = e / (vol (divset (D,k)));
A11: 0 < vol (divset (D,k)) by A10, INTEGRA1:9;
then 0 < e / (vol (divset (D,k))) by A2, XREAL_1:139;
then consider r being real number such that
A12: r in rng (f | (divset (D,k))) and
A13: r < (lower_bound (rng (f | (divset (D,k))))) + (e / (vol (divset (D,k)))) by A6, A5, SEQ_4:def_2;
A14: (lower_volume (f,D)) . k = (lower_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k))) by A4, INTEGRA1:def_7;
reconsider x = r * (vol (divset (D,k))) as Element of REAL ;
x < ((lower_bound (rng (f | (divset (D,k))))) + (e / (vol (divset (D,k))))) * (vol (divset (D,k))) by A11, A13, XREAL_1:68;
then x < ((lower_volume (f,D)) . k) + ((e / (vol (divset (D,k)))) * (vol (divset (D,k)))) by A14;
then A15: x < ((lower_volume (f,D)) . k) + e by A10, XCMPLX_1:87;
lower_bound (rng (f | (divset (D,k)))) <= r by A6, A12, SEQ_4:def_2;
then (lower_volume (f,D)) . k <= x by A11, A14, XREAL_1:64;
hence ex x being Element of REAL st S1[k,x] by A12, A15; ::_thesis: verum
end;
end;
end;
consider p being FinSequence of REAL such that
A16: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds
S1[k,p . k] ) ) from FINSEQ_1:sch_5(A3);
A17: now__::_thesis:_for_i_being_Nat_st_i_in_dom_D_holds_
ex_r_being_Element_of_REAL_st_
(_r_in_rng_(f_|_(divset_(D,i)))_&_p_._i_=_r_*_(vol_(divset_(D,i)))_)
let i be Nat; ::_thesis: ( i in dom D implies ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) )
assume i in dom D ; ::_thesis: ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) )
then i in Seg (len D) by FINSEQ_1:def_3;
then consider r being Element of REAL such that
A18: ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) and
(lower_volume (f,D)) . i <= p . i and
p . i < ((lower_volume (f,D)) . i) + e by A16;
take r = r; ::_thesis: ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) )
thus ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) by A18; ::_thesis: verum
end;
len p = len D by A16, FINSEQ_1:def_3;
then reconsider p = p as middle_volume of f,D by A17, Def1;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_D_holds_
(_(lower_volume_(f,D))_._i_<=_p_._i_&_p_._i_<_((lower_volume_(f,D))_._i)_+_e_)
let i be Nat; ::_thesis: ( i in dom D implies ( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e ) )
assume i in dom D ; ::_thesis: ( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e )
then i in Seg (len D) by FINSEQ_1:def_3;
then ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) & (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e ) by A16;
hence ( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e ) ; ::_thesis: verum
end;
hence ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) ; ::_thesis: verum
end;
Lm3: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i )
let f be Function of A,REAL; ::_thesis: for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i )
let D be Division of A; ::_thesis: for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i )
let e be Real; ::_thesis: ( f | A is bounded_above & 0 < e implies ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i ) )
assume that
A1: f | A is bounded_above and
A2: 0 < e ; ::_thesis: ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i )
defpred S1[ Nat, Element of REAL ] means ex r being Element of REAL st
( r in rng (f | (divset (D,$1))) & $2 = r * (vol (divset (D,$1))) & $2 <= (upper_volume (f,D)) . $1 & ((upper_volume (f,D)) . $1) - e < $2 );
A3: for k being Nat st k in Seg (len D) holds
ex x being Element of REAL st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len D) implies ex x being Element of REAL st S1[k,x] )
assume k in Seg (len D) ; ::_thesis: ex x being Element of REAL st S1[k,x]
then A4: k in dom D by FINSEQ_1:def_3;
dom f = A by FUNCT_2:def_1;
then dom (f | (divset (D,k))) = divset (D,k) by A4, INTEGRA1:8, RELAT_1:62;
then A5: not rng (f | (divset (D,k))) is empty by RELAT_1:42;
rng f is bounded_above by A1, INTEGRA1:13;
then A6: rng (f | (divset (D,k))) is bounded_above by RELAT_1:70, XXREAL_2:43;
percases ( vol (divset (D,k)) = 0 or vol (divset (D,k)) <> 0 ) ;
supposeA7: vol (divset (D,k)) = 0 ; ::_thesis: ex x being Element of REAL st S1[k,x]
consider r being set such that
A8: r in rng (f | (divset (D,k))) by A5, XBOOLE_0:def_1;
reconsider r = r as Element of REAL by A8;
reconsider x = r * (vol (divset (D,k))) as Element of REAL ;
A9: (upper_volume (f,D)) . k = (upper_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k))) by A4, INTEGRA1:def_6
.= 0 by A7 ;
then ((upper_volume (f,D)) . k) - e < x by A2, A7;
hence ex x being Element of REAL st S1[k,x] by A7, A8, A9; ::_thesis: verum
end;
supposeA10: vol (divset (D,k)) <> 0 ; ::_thesis: ex x being Element of REAL st S1[k,x]
set l = upper_bound (rng (f | (divset (D,k))));
set e1 = e / (vol (divset (D,k)));
A11: 0 < vol (divset (D,k)) by A10, INTEGRA1:9;
then 0 < e / (vol (divset (D,k))) by A2, XREAL_1:139;
then consider r being real number such that
A12: r in rng (f | (divset (D,k))) and
A13: (upper_bound (rng (f | (divset (D,k))))) - (e / (vol (divset (D,k)))) < r by A6, A5, SEQ_4:def_1;
A14: (upper_volume (f,D)) . k = (upper_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k))) by A4, INTEGRA1:def_6;
reconsider x = r * (vol (divset (D,k))) as Element of REAL ;
((upper_bound (rng (f | (divset (D,k))))) - (e / (vol (divset (D,k))))) * (vol (divset (D,k))) < x by A11, A13, XREAL_1:68;
then ((upper_volume (f,D)) . k) - ((e / (vol (divset (D,k)))) * (vol (divset (D,k)))) < x by A14;
then A15: ((upper_volume (f,D)) . k) - e < x by A10, XCMPLX_1:87;
r <= upper_bound (rng (f | (divset (D,k)))) by A6, A12, SEQ_4:def_1;
then x <= (upper_volume (f,D)) . k by A11, A14, XREAL_1:64;
hence ex x being Element of REAL st S1[k,x] by A12, A15; ::_thesis: verum
end;
end;
end;
consider p being FinSequence of REAL such that
A16: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds
S1[k,p . k] ) ) from FINSEQ_1:sch_5(A3);
A17: now__::_thesis:_for_i_being_Nat_st_i_in_dom_D_holds_
ex_r_being_Element_of_REAL_st_
(_r_in_rng_(f_|_(divset_(D,i)))_&_p_._i_=_r_*_(vol_(divset_(D,i)))_)
let i be Nat; ::_thesis: ( i in dom D implies ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) )
assume i in dom D ; ::_thesis: ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) )
then i in Seg (len D) by FINSEQ_1:def_3;
then consider r being Element of REAL such that
A18: ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) and
p . i <= (upper_volume (f,D)) . i and
((upper_volume (f,D)) . i) - e < p . i by A16;
take r = r; ::_thesis: ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) )
thus ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) by A18; ::_thesis: verum
end;
len p = len D by A16, FINSEQ_1:def_3;
then reconsider p = p as middle_volume of f,D by A17, Def1;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_D_holds_
(_p_._i_<=_(upper_volume_(f,D))_._i_&_((upper_volume_(f,D))_._i)_-_e_<_p_._i_)
let i be Nat; ::_thesis: ( i in dom D implies ( p . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < p . i ) )
assume i in dom D ; ::_thesis: ( p . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < p . i )
then i in Seg (len D) by FINSEQ_1:def_3;
then ex r being Element of REAL st
( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) & p . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < p . i ) by A16;
hence ( p . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < p . i ) ; ::_thesis: verum
end;
hence ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e < F . i ) ; ::_thesis: verum
end;
Lm4: for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_above & i in dom D holds
F . i <= (upper_volume (f,D)) . i
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_above & i in dom D holds
F . i <= (upper_volume (f,D)) . i
let f be Function of A,REAL; ::_thesis: for D being Division of A
for F being middle_volume of f,D
for i being Nat st f | A is bounded_above & i in dom D holds
F . i <= (upper_volume (f,D)) . i
let D be Division of A; ::_thesis: for F being middle_volume of f,D
for i being Nat st f | A is bounded_above & i in dom D holds
F . i <= (upper_volume (f,D)) . i
let F be middle_volume of f,D; ::_thesis: for i being Nat st f | A is bounded_above & i in dom D holds
F . i <= (upper_volume (f,D)) . i
let i be Nat; ::_thesis: ( f | A is bounded_above & i in dom D implies F . i <= (upper_volume (f,D)) . i )
assume that
A1: f | A is bounded_above and
A2: i in dom D ; ::_thesis: F . i <= (upper_volume (f,D)) . i
A3: (upper_volume (f,D)) . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A2, INTEGRA1:def_6;
consider r being Element of REAL such that
A4: r in rng (f | (divset (D,i))) and
A5: F . i = r * (vol (divset (D,i))) by A2, Def1;
rng f is bounded_above by A1, INTEGRA1:13;
then rng (f | (divset (D,i))) is bounded_above by RELAT_1:70, XXREAL_2:43;
then ( 0 <= vol (divset (D,i)) & r <= upper_bound (rng (f | (divset (D,i)))) ) by A4, INTEGRA1:9, SEQ_4:def_1;
hence F . i <= (upper_volume (f,D)) . i by A5, A3, XREAL_1:64; ::_thesis: verum
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL;
let D be Division of A;
let F be middle_volume of f,D;
func middle_sum (f,F) -> Real equals :: INTEGR15:def 2
Sum F;
correctness
coherence
Sum F is Real;
;
end;
:: deftheorem defines middle_sum INTEGR15:def_2_:_
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D holds middle_sum (f,F) = Sum F;
theorem Th1: :: INTEGR15:1
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D st f | A is bounded_below holds
lower_sum (f,D) <= middle_sum (f,F)
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D st f | A is bounded_below holds
lower_sum (f,D) <= middle_sum (f,F)
let f be Function of A,REAL; ::_thesis: for D being Division of A
for F being middle_volume of f,D st f | A is bounded_below holds
lower_sum (f,D) <= middle_sum (f,F)
let D be Division of A; ::_thesis: for F being middle_volume of f,D st f | A is bounded_below holds
lower_sum (f,D) <= middle_sum (f,F)
let F be middle_volume of f,D; ::_thesis: ( f | A is bounded_below implies lower_sum (f,D) <= middle_sum (f,F) )
len (lower_volume (f,D)) = len D by INTEGRA1:def_7;
then reconsider p = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
len F = len D by Def1;
then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
assume A1: f | A is bounded_below ; ::_thesis: lower_sum (f,D) <= middle_sum (f,F)
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_D)_holds_
p_._i_<=_q_._i
let i be Nat; ::_thesis: ( i in Seg (len D) implies p . i <= q . i )
assume i in Seg (len D) ; ::_thesis: p . i <= q . i
then i in dom D by FINSEQ_1:def_3;
hence p . i <= q . i by A1, Lm1; ::_thesis: verum
end;
hence lower_sum (f,D) <= middle_sum (f,F) by RVSUM_1:82; ::_thesis: verum
end;
theorem Th2: :: INTEGR15:2
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D st f | A is bounded_above holds
middle_sum (f,F) <= upper_sum (f,D)
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D st f | A is bounded_above holds
middle_sum (f,F) <= upper_sum (f,D)
let f be Function of A,REAL; ::_thesis: for D being Division of A
for F being middle_volume of f,D st f | A is bounded_above holds
middle_sum (f,F) <= upper_sum (f,D)
let D be Division of A; ::_thesis: for F being middle_volume of f,D st f | A is bounded_above holds
middle_sum (f,F) <= upper_sum (f,D)
let F be middle_volume of f,D; ::_thesis: ( f | A is bounded_above implies middle_sum (f,F) <= upper_sum (f,D) )
len (upper_volume (f,D)) = len D by INTEGRA1:def_6;
then reconsider p = upper_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
len F = len D by Def1;
then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
assume A1: f | A is bounded_above ; ::_thesis: middle_sum (f,F) <= upper_sum (f,D)
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_D)_holds_
q_._i_<=_p_._i
let i be Nat; ::_thesis: ( i in Seg (len D) implies q . i <= p . i )
assume i in Seg (len D) ; ::_thesis: q . i <= p . i
then i in dom D by FINSEQ_1:def_3;
hence q . i <= p . i by A1, Lm4; ::_thesis: verum
end;
hence middle_sum (f,F) <= upper_sum (f,D) by RVSUM_1:82; ::_thesis: verum
end;
theorem Th3: :: INTEGR15:3
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e
let f be Function of A,REAL; ::_thesis: for D being Division of A
for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e
let D be Division of A; ::_thesis: for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e
let e be Real; ::_thesis: ( f | A is bounded_below & 0 < e implies ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e )
len (lower_volume (f,D)) = len D by INTEGRA1:def_7;
then reconsider p = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
set e1 = e / (len D);
assume ( f | A is bounded_below & 0 < e ) ; ::_thesis: ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e
then consider F being middle_volume of f,D such that
A1: for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + (e / (len D)) ) by Lm2, XREAL_1:139;
set s = (len D) |-> (e / (len D));
reconsider t = p + ((len D) |-> (e / (len D))) as Element of (len D) -tuples_on REAL ;
take F ; ::_thesis: middle_sum (f,F) <= (lower_sum (f,D)) + e
len F = len D by Def1;
then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_D)_holds_
q_._i_<=_t_._i
let i be Nat; ::_thesis: ( i in Seg (len D) implies q . i <= t . i )
assume A2: i in Seg (len D) ; ::_thesis: q . i <= t . i
then i in dom D by FINSEQ_1:def_3;
then q . i <= (p . i) + (e / (len D)) by A1;
then q . i <= (p . i) + (((len D) |-> (e / (len D))) . i) by A2, FINSEQ_2:57;
hence q . i <= t . i by RVSUM_1:11; ::_thesis: verum
end;
then Sum q <= Sum t by RVSUM_1:82;
then Sum q <= (Sum p) + (Sum ((len D) |-> (e / (len D)))) by RVSUM_1:89;
then Sum q <= (Sum p) + ((len D) * (e / (len D))) by RVSUM_1:80;
hence middle_sum (f,F) <= (lower_sum (f,D)) + e by XCMPLX_1:87; ::_thesis: verum
end;
theorem Th4: :: INTEGR15:4
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F)
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F)
let f be Function of A,REAL; ::_thesis: for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F)
let D be Division of A; ::_thesis: for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F)
let e be Real; ::_thesis: ( f | A is bounded_above & 0 < e implies ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F) )
len (upper_volume (f,D)) = len D by INTEGRA1:def_6;
then reconsider p = upper_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
set e1 = e / (len D);
assume ( f | A is bounded_above & 0 < e ) ; ::_thesis: ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F)
then consider F being middle_volume of f,D such that
A1: for i being Nat st i in dom D holds
( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - (e / (len D)) < F . i ) by Lm3, XREAL_1:139;
set s = (len D) |-> (e / (len D));
reconsider t = p - ((len D) |-> (e / (len D))) as Element of (len D) -tuples_on REAL ;
take F ; ::_thesis: (upper_sum (f,D)) - e <= middle_sum (f,F)
len F = len D by Def1;
then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(len_D)_holds_
t_._i_<=_q_._i
let i be Nat; ::_thesis: ( i in Seg (len D) implies t . i <= q . i )
assume A2: i in Seg (len D) ; ::_thesis: t . i <= q . i
then i in dom D by FINSEQ_1:def_3;
then (p . i) - (e / (len D)) <= q . i by A1;
then (p . i) - (((len D) |-> (e / (len D))) . i) <= q . i by A2, FINSEQ_2:57;
hence t . i <= q . i by RVSUM_1:27; ::_thesis: verum
end;
then Sum t <= Sum q by RVSUM_1:82;
then (Sum p) - (Sum ((len D) |-> (e / (len D)))) <= Sum q by RVSUM_1:90;
then (Sum p) - ((len D) * (e / (len D))) <= Sum q by RVSUM_1:80;
hence (upper_sum (f,D)) - e <= middle_sum (f,F) by XCMPLX_1:87; ::_thesis: verum
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL;
let T be DivSequence of A;
mode middle_volume_Sequence of f,T -> Function of NAT,(REAL *) means :Def3: :: INTEGR15:def 3
for k being Element of NAT holds it . k is middle_volume of f,T . k;
correctness
existence
ex b1 being Function of NAT,(REAL *) st
for k being Element of NAT holds b1 . k is middle_volume of f,T . k;
proof
defpred S1[ Element of NAT , set ] means $2 is middle_volume of f,T . $1;
A1: for x being Element of NAT ex y being Element of REAL * st S1[x,y]
proof
let x be Element of NAT ; ::_thesis: ex y being Element of REAL * st S1[x,y]
set y = the middle_volume of f,T . x;
reconsider y = the middle_volume of f,T . x as Element of REAL * by FINSEQ_1:def_11;
y is middle_volume of f,T . x ;
hence ex y being Element of REAL * st S1[x,y] ; ::_thesis: verum
end;
ex f being Function of NAT,(REAL *) st
for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A1);
hence ex b1 being Function of NAT,(REAL *) st
for k being Element of NAT holds b1 . k is middle_volume of f,T . k ; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines middle_volume_Sequence INTEGR15:def_3_:_
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for b4 being Function of NAT,(REAL *) holds
( b4 is middle_volume_Sequence of f,T iff for k being Element of NAT holds b4 . k is middle_volume of f,T . k );
definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
let k be Element of NAT ;
:: original: .
redefine funcS . k -> middle_volume of f,T . k;
coherence
S . k is middle_volume of f,T . k by Def3;
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be Function of A,REAL;
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
func middle_sum (f,S) -> Real_Sequence means :Def4: :: INTEGR15:def 4
for i being Element of NAT holds it . i = middle_sum (f,(S . i));
existence
ex b1 being Real_Sequence st
for i being Element of NAT holds b1 . i = middle_sum (f,(S . i))
proof
deffunc H1( Element of NAT ) -> Real = middle_sum (f,(S . $1));
thus ex IT being Real_Sequence st
for i being Element of NAT holds IT . i = H1(i) from SEQ_1:sch_1(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Real_Sequence st ( for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b2 . i = middle_sum (f,(S . i)) ) holds
b1 = b2
proof
let F1, F2 be Real_Sequence; ::_thesis: ( ( for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ) implies F1 = F2 )
assume that
A1: for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) and
A2: for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ; ::_thesis: F1 = F2
for i being Element of NAT holds F1 . i = F2 . i
proof
let i be Element of NAT ; ::_thesis: F1 . i = F2 . i
F1 . i = middle_sum (f,(S . i)) by A1
.= F2 . i by A2 ;
hence F1 . i = F2 . i ; ::_thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines middle_sum INTEGR15:def_4_:_
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for b5 being Real_Sequence holds
( b5 = middle_sum (f,S) iff for i being Element of NAT holds b5 . i = middle_sum (f,(S . i)) );
theorem Th5: :: INTEGR15:5
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for i being Element of NAT st f | A is bounded_below holds
(lower_sum (f,T)) . i <= (middle_sum (f,S)) . i
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for i being Element of NAT st f | A is bounded_below holds
(lower_sum (f,T)) . i <= (middle_sum (f,S)) . i
let f be Function of A,REAL; ::_thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for i being Element of NAT st f | A is bounded_below holds
(lower_sum (f,T)) . i <= (middle_sum (f,S)) . i
let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of f,T
for i being Element of NAT st f | A is bounded_below holds
(lower_sum (f,T)) . i <= (middle_sum (f,S)) . i
let S be middle_volume_Sequence of f,T; ::_thesis: for i being Element of NAT st f | A is bounded_below holds
(lower_sum (f,T)) . i <= (middle_sum (f,S)) . i
let i be Element of NAT ; ::_thesis: ( f | A is bounded_below implies (lower_sum (f,T)) . i <= (middle_sum (f,S)) . i )
assume A1: f | A is bounded_below ; ::_thesis: (lower_sum (f,T)) . i <= (middle_sum (f,S)) . i
( (middle_sum (f,S)) . i = middle_sum (f,(S . i)) & (lower_sum (f,T)) . i = lower_sum (f,(T . i)) ) by Def4, INTEGRA2:def_3;
hence (lower_sum (f,T)) . i <= (middle_sum (f,S)) . i by A1, Th1; ::_thesis: verum
end;
theorem Th6: :: INTEGR15:6
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for i being Element of NAT st f | A is bounded_above holds
(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for i being Element of NAT st f | A is bounded_above holds
(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i
let f be Function of A,REAL; ::_thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for i being Element of NAT st f | A is bounded_above holds
(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i
let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of f,T
for i being Element of NAT st f | A is bounded_above holds
(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i
let S be middle_volume_Sequence of f,T; ::_thesis: for i being Element of NAT st f | A is bounded_above holds
(middle_sum (f,S)) . i <= (upper_sum (f,T)) . i
let i be Element of NAT ; ::_thesis: ( f | A is bounded_above implies (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i )
assume A1: f | A is bounded_above ; ::_thesis: (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i
( (middle_sum (f,S)) . i = middle_sum (f,(S . i)) & (upper_sum (f,T)) . i = upper_sum (f,(T . i)) ) by Def4, INTEGRA2:def_2;
hence (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i by A1, Th2; ::_thesis: verum
end;
theorem Th7: :: INTEGR15:7
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for e being Element of REAL st 0 < e & f | A is bounded_below holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for T being DivSequence of A
for e being Element of REAL st 0 < e & f | A is bounded_below holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e
let f be Function of A,REAL; ::_thesis: for T being DivSequence of A
for e being Element of REAL st 0 < e & f | A is bounded_below holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e
let T be DivSequence of A; ::_thesis: for e being Element of REAL st 0 < e & f | A is bounded_below holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e
let e be Element of REAL ; ::_thesis: ( 0 < e & f | A is bounded_below implies ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e )
defpred S1[ Element of NAT , set ] means ( $2 is middle_volume of f,T . $1 & ex z being middle_volume of f,T . $1 st
( z = $2 & middle_sum (f,z) <= (lower_sum (f,(T . $1))) + e ) );
assume A1: ( 0 < e & f | A is bounded_below ) ; ::_thesis: ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e
A2: for x being Element of NAT ex y being Element of REAL * st S1[x,y]
proof
let x be Element of NAT ; ::_thesis: ex y being Element of REAL * st S1[x,y]
consider z being middle_volume of f,T . x such that
A3: middle_sum (f,z) <= (lower_sum (f,(T . x))) + e by A1, Th3;
reconsider y = z as Element of REAL * by FINSEQ_1:def_11;
take y ; ::_thesis: S1[x,y]
thus S1[x,y] by A3; ::_thesis: verum
end;
consider F being Function of NAT,(REAL *) such that
A4: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A2);
reconsider F = F as middle_volume_Sequence of f,T by A4, Def3;
now__::_thesis:_for_x_being_Element_of_NAT_holds_(middle_sum_(f,F))_._x_<=_((lower_sum_(f,T))_._x)_+_e
let x be Element of NAT ; ::_thesis: (middle_sum (f,F)) . x <= ((lower_sum (f,T)) . x) + e
ex z being middle_volume of f,T . x st
( z = F . x & middle_sum (f,z) <= (lower_sum (f,(T . x))) + e ) by A4;
then (middle_sum (f,F)) . x <= (lower_sum (f,(T . x))) + e by Def4;
hence (middle_sum (f,F)) . x <= ((lower_sum (f,T)) . x) + e by INTEGRA2:def_3; ::_thesis: verum
end;
hence ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e ; ::_thesis: verum
end;
theorem Th8: :: INTEGR15:8
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for e being Element of REAL st 0 < e & f | A is bounded_above holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for T being DivSequence of A
for e being Element of REAL st 0 < e & f | A is bounded_above holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i
let f be Function of A,REAL; ::_thesis: for T being DivSequence of A
for e being Element of REAL st 0 < e & f | A is bounded_above holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i
let T be DivSequence of A; ::_thesis: for e being Element of REAL st 0 < e & f | A is bounded_above holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i
let e be Element of REAL ; ::_thesis: ( 0 < e & f | A is bounded_above implies ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i )
defpred S1[ Element of NAT , set ] means ( $2 is middle_volume of f,T . $1 & ex z being middle_volume of f,T . $1 st
( z = $2 & (upper_sum (f,(T . $1))) - e <= middle_sum (f,z) ) );
assume A1: ( 0 < e & f | A is bounded_above ) ; ::_thesis: ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i
A2: for x being Element of NAT ex y being Element of REAL * st S1[x,y]
proof
let x be Element of NAT ; ::_thesis: ex y being Element of REAL * st S1[x,y]
consider z being middle_volume of f,T . x such that
A3: (upper_sum (f,(T . x))) - e <= middle_sum (f,z) by A1, Th4;
reconsider y = z as Element of REAL * by FINSEQ_1:def_11;
take y ; ::_thesis: S1[x,y]
thus S1[x,y] by A3; ::_thesis: verum
end;
consider F being Function of NAT,(REAL *) such that
A4: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A2);
reconsider F = F as middle_volume_Sequence of f,T by A4, Def3;
now__::_thesis:_for_x_being_Element_of_NAT_holds_((upper_sum_(f,T))_._x)_-_e_<=_(middle_sum_(f,F))_._x
let x be Element of NAT ; ::_thesis: ((upper_sum (f,T)) . x) - e <= (middle_sum (f,F)) . x
ex z being middle_volume of f,T . x st
( z = F . x & (upper_sum (f,(T . x))) - e <= middle_sum (f,z) ) by A4;
then (upper_sum (f,(T . x))) - e <= (middle_sum (f,F)) . x by Def4;
hence ((upper_sum (f,T)) . x) - e <= (middle_sum (f,F)) . x by INTEGRA2:def_2; ::_thesis: verum
end;
hence ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i ; ::_thesis: verum
end;
Lm5: for p, q, r being Real_Sequence st p is convergent & r is convergent & lim p = lim r & ( for i being Element of NAT holds p . i <= q . i ) & ( for i being Element of NAT holds q . i <= r . i ) holds
( q is convergent & lim p = lim q & lim r = lim q )
proof
let p, q, r be Real_Sequence; ::_thesis: ( p is convergent & r is convergent & lim p = lim r & ( for i being Element of NAT holds p . i <= q . i ) & ( for i being Element of NAT holds q . i <= r . i ) implies ( q is convergent & lim p = lim q & lim r = lim q ) )
assume that
A1: p is convergent and
A2: r is convergent and
A3: lim p = lim r and
A4: for i being Element of NAT holds p . i <= q . i and
A5: for i being Element of NAT holds q . i <= r . i ; ::_thesis: ( q is convergent & lim p = lim q & lim r = lim q )
A6: now__::_thesis:_for_e_being_real_number_st_0_<_e_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((q_._m)_-_(lim_p))_<_e
let e be real number ; ::_thesis: ( 0 < e implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((q . m) - (lim p)) < e )
assume A7: 0 < e ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((q . m) - (lim p)) < e
then consider n1 being Element of NAT such that
A8: for m being Element of NAT st n1 <= m holds
abs ((p . m) - (lim p)) < e by A1, SEQ_2:def_7;
consider n2 being Element of NAT such that
A9: for m being Element of NAT st n2 <= m holds
abs ((r . m) - (lim r)) < e by A2, A7, SEQ_2:def_7;
reconsider n = max (n1,n2) as Element of NAT by ORDINAL1:def_12;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
abs ((q . m) - (lim p)) < e
thus for m being Element of NAT st n <= m holds
abs ((q . m) - (lim p)) < e ::_thesis: verum
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((q . m) - (lim p)) < e )
assume A10: n <= m ; ::_thesis: abs ((q . m) - (lim p)) < e
n1 <= n by XXREAL_0:25;
then n1 <= m by A10, XXREAL_0:2;
then abs ((p . m) - (lim p)) < e by A8;
then p . m in ].((lim p) - e),((lim p) + e).[ by RCOMP_1:1;
then p . m in { z where z is Real : ( (lim p) - e < z & z < (lim p) + e ) } by RCOMP_1:def_2;
then A11: ex z being Real st
( z = p . m & (lim p) - e < z & z < (lim p) + e ) ;
p . m <= q . m by A4;
then A12: (lim p) - e < q . m by A11, XXREAL_0:2;
n2 <= n by XXREAL_0:25;
then n2 <= m by A10, XXREAL_0:2;
then abs ((r . m) - (lim r)) < e by A9;
then r . m in ].((lim r) - e),((lim r) + e).[ by RCOMP_1:1;
then r . m in { z where z is Real : ( (lim r) - e < z & z < (lim r) + e ) } by RCOMP_1:def_2;
then A13: ex z being Real st
( z = r . m & (lim r) - e < z & z < (lim r) + e ) ;
q . m <= r . m by A5;
then q . m < (lim p) + e by A3, A13, XXREAL_0:2;
then q . m in { z where z is Real : ( (lim p) - e < z & z < (lim p) + e ) } by A12;
then q . m in ].((lim p) - e),((lim p) + e).[ by RCOMP_1:def_2;
hence abs ((q . m) - (lim p)) < e by RCOMP_1:1; ::_thesis: verum
end;
end;
hence q is convergent by SEQ_2:def_6; ::_thesis: ( lim p = lim q & lim r = lim q )
hence ( lim q = lim p & lim q = lim r ) by A3, A6, SEQ_2:def_7; ::_thesis: verum
end;
theorem Th9: :: INTEGR15:9
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
let f be Function of A,REAL; ::_thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
let S be middle_volume_Sequence of f,T; ::_thesis: ( f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 implies ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) )
assume that
A1: f is bounded and
A2: f is integrable and
A3: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
A4: dom f = A by FUNCT_2:def_1;
then f | A is bounded_below by A1, RELAT_1:69;
then A5: for i being Element of NAT holds (lower_sum (f,T)) . i <= (middle_sum (f,S)) . i by Th5;
A6: f | A = f by A4, RELAT_1:69;
then A7: ( lower_sum (f,T) is convergent & upper_sum (f,T) is convergent ) by A1, A3, INTEGRA4:8, INTEGRA4:9;
f | A is bounded_above by A1, A4, RELAT_1:69;
then A8: for i being Element of NAT holds (middle_sum (f,S)) . i <= (upper_sum (f,T)) . i by Th6;
A9: (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 by A1, A2, A3, A6, INTEGRA4:12;
then lim (lower_sum (f,T)) = integral f by A1, A3, A6, INTEGRA4:9;
hence ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) by A7, A9, A5, A8, Lm5; ::_thesis: verum
end;
theorem Th10: :: INTEGR15:10
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL st f is bounded holds
( f is integrable iff ex I being Real st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f is bounded holds
( f is integrable iff ex I being Real st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
let f be Function of A,REAL; ::_thesis: ( f is bounded implies ( f is integrable iff ex I being Real st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) )
assume A1: f is bounded ; ::_thesis: ( f is integrable iff ex I being Real st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
hereby ::_thesis: ( ex I being Real st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable )
assume A2: f is integrable ; ::_thesis: ex I being Element of REAL st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )
take I = integral f; ::_thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )
thus for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A1, A2, Th9; ::_thesis: verum
end;
dom f = A by FUNCT_2:def_1;
then A3: f | A is bounded by A1, RELAT_1:69;
now__::_thesis:_(_ex_I_being_Real_st_
for_T_being_DivSequence_of_A
for_S_being_middle_volume_Sequence_of_f,T_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_
(_middle_sum_(f,S)_is_convergent_&_lim_(middle_sum_(f,S))_=_I_)_implies_f_is_integrable_)
assume ex I being Real st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ; ::_thesis: f is integrable
then consider I being Real such that
A4: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ;
A5: for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
lim (upper_sum (f,T)) = I
proof
let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies lim (upper_sum (f,T)) = I )
set S = the middle_volume_Sequence of f,T;
A6: now__::_thesis:_for_i_being_Element_of_NAT_holds_0_<=_((upper_sum_(f,T))_-_(middle_sum_(f,_the_middle_volume_Sequence_of_f,T)))_._i
let i be Element of NAT ; ::_thesis: 0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . i
(middle_sum (f, the middle_volume_Sequence of f,T)) . i <= (upper_sum (f,T)) . i by A3, Th6;
then ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) - ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) <= ((upper_sum (f,T)) . i) - ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) by XREAL_1:9;
hence 0 <= ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) . i by VALUED_1:15; ::_thesis: verum
end;
assume A7: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: lim (upper_sum (f,T)) = I
then A8: upper_sum (f,T) is convergent by A3, INTEGRA4:9;
A9: now__::_thesis:_for_e1_being_real_number_st_0_<_e1_holds_
(lim_(upper_sum_(f,T)))_-_I_<=_e1
let e1 be real number ; ::_thesis: ( 0 < e1 implies (lim (upper_sum (f,T))) - I <= e1 )
reconsider e = e1 as Real by XREAL_0:def_1;
assume 0 < e1 ; ::_thesis: (lim (upper_sum (f,T))) - I <= e1
then consider S being middle_volume_Sequence of f,T such that
A10: for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i by A3, Th8;
A11: now__::_thesis:_for_i_being_Element_of_NAT_holds_((upper_sum_(f,T))_-_(middle_sum_(f,S)))_._i_<=_e
let i be Element of NAT ; ::_thesis: ((upper_sum (f,T)) - (middle_sum (f,S))) . i <= e
((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i by A10;
then (((upper_sum (f,T)) . i) - e) + e <= ((middle_sum (f,S)) . i) + e by XREAL_1:6;
then ((upper_sum (f,T)) . i) - ((middle_sum (f,S)) . i) <= (((middle_sum (f,S)) . i) + e) - ((middle_sum (f,S)) . i) by XREAL_1:9;
hence ((upper_sum (f,T)) - (middle_sum (f,S))) . i <= e by VALUED_1:15; ::_thesis: verum
end;
A12: middle_sum (f,S) is convergent by A4, A7;
then A13: (upper_sum (f,T)) - (middle_sum (f,S)) is convergent by A8;
lim ((upper_sum (f,T)) - (middle_sum (f,S))) = (lim (upper_sum (f,T))) - (lim (middle_sum (f,S))) by A8, A12, SEQ_2:12
.= (lim (upper_sum (f,T))) - I by A4, A7 ;
hence (lim (upper_sum (f,T))) - I <= e1 by A11, A13, PREPOWER:2; ::_thesis: verum
end;
A14: middle_sum (f, the middle_volume_Sequence of f,T) is convergent by A4, A7;
then A15: (upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T)) is convergent by A8;
lim ((upper_sum (f,T)) - (middle_sum (f, the middle_volume_Sequence of f,T))) = (lim (upper_sum (f,T))) - (lim (middle_sum (f, the middle_volume_Sequence of f,T))) by A8, A14, SEQ_2:12
.= (lim (upper_sum (f,T))) - I by A4, A7 ;
then 0 <= (lim (upper_sum (f,T))) - I by A6, A15, SEQ_2:17;
then (lim (upper_sum (f,T))) - I = 0 by A9, XREAL_1:5;
hence lim (upper_sum (f,T)) = I ; ::_thesis: verum
end;
A16: for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
I = lim (lower_sum (f,T))
proof
let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies I = lim (lower_sum (f,T)) )
set S = the middle_volume_Sequence of f,T;
A17: now__::_thesis:_for_i_being_Element_of_NAT_holds_0_<=_((middle_sum_(f,_the_middle_volume_Sequence_of_f,T))_-_(lower_sum_(f,T)))_._i
let i be Element of NAT ; ::_thesis: 0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . i
(lower_sum (f,T)) . i <= (middle_sum (f, the middle_volume_Sequence of f,T)) . i by A3, Th5;
then ((lower_sum (f,T)) . i) - ((lower_sum (f,T)) . i) <= ((middle_sum (f, the middle_volume_Sequence of f,T)) . i) - ((lower_sum (f,T)) . i) by XREAL_1:9;
hence 0 <= ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) . i by VALUED_1:15; ::_thesis: verum
end;
assume A18: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: I = lim (lower_sum (f,T))
then A19: lower_sum (f,T) is convergent by A3, INTEGRA4:8;
A20: now__::_thesis:_for_e1_being_real_number_st_0_<_e1_holds_
I_-_(lim_(lower_sum_(f,T)))_<=_e1
let e1 be real number ; ::_thesis: ( 0 < e1 implies I - (lim (lower_sum (f,T))) <= e1 )
reconsider e = e1 as Real by XREAL_0:def_1;
assume 0 < e1 ; ::_thesis: I - (lim (lower_sum (f,T))) <= e1
then consider S being middle_volume_Sequence of f,T such that
A21: for i being Element of NAT holds (middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e by A3, Th7;
A22: now__::_thesis:_for_i_being_Element_of_NAT_holds_((middle_sum_(f,S))_-_(lower_sum_(f,T)))_._i_<=_e
let i be Element of NAT ; ::_thesis: ((middle_sum (f,S)) - (lower_sum (f,T))) . i <= e
(middle_sum (f,S)) . i <= ((lower_sum (f,T)) . i) + e by A21;
then ((middle_sum (f,S)) . i) - ((lower_sum (f,T)) . i) <= (((lower_sum (f,T)) . i) + e) - ((lower_sum (f,T)) . i) by XREAL_1:9;
hence ((middle_sum (f,S)) - (lower_sum (f,T))) . i <= e by VALUED_1:15; ::_thesis: verum
end;
A23: middle_sum (f,S) is convergent by A4, A18;
then A24: (middle_sum (f,S)) - (lower_sum (f,T)) is convergent by A19;
lim ((middle_sum (f,S)) - (lower_sum (f,T))) = (lim (middle_sum (f,S))) - (lim (lower_sum (f,T))) by A19, A23, SEQ_2:12
.= I - (lim (lower_sum (f,T))) by A4, A18 ;
hence I - (lim (lower_sum (f,T))) <= e1 by A22, A24, PREPOWER:2; ::_thesis: verum
end;
A25: middle_sum (f, the middle_volume_Sequence of f,T) is convergent by A4, A18;
then A26: (middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T)) is convergent by A19;
lim ((middle_sum (f, the middle_volume_Sequence of f,T)) - (lower_sum (f,T))) = (lim (middle_sum (f, the middle_volume_Sequence of f,T))) - (lim (lower_sum (f,T))) by A19, A25, SEQ_2:12
.= I - (lim (lower_sum (f,T))) by A4, A18 ;
then 0 <= I - (lim (lower_sum (f,T))) by A17, A26, SEQ_2:17;
then I - (lim (lower_sum (f,T))) = 0 by A20, XREAL_1:5;
hence I = lim (lower_sum (f,T)) ; ::_thesis: verum
end;
now__::_thesis:_for_T_being_DivSequence_of_A_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_
(lim_(upper_sum_(f,T)))_-_(lim_(lower_sum_(f,T)))_=_0
let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0 )
assume A27: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = 0
hence (lim (upper_sum (f,T))) - (lim (lower_sum (f,T))) = (lim (upper_sum (f,T))) - I by A16
.= I - I by A5, A27
.= 0 ;
::_thesis: verum
end;
hence f is integrable by A3, INTEGRA4:12; ::_thesis: verum
end;
hence ( ex I being Real st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable ) ; ::_thesis: verum
end;
definition
let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);
let D be Division of A;
mode middle_volume of f,D -> FinSequence of REAL n means :Def5: :: INTEGR15:def 5
( len it = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL n st
( r in rng (f | (divset (D,i))) & it . i = (vol (divset (D,i))) * r ) ) );
correctness
existence
ex b1 being FinSequence of REAL n st
( len b1 = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL n st
( r in rng (f | (divset (D,i))) & b1 . i = (vol (divset (D,i))) * r ) ) );
proof
defpred S1[ Nat, set ] means ex r being Element of REAL n st
( r in rng (f | (divset (D,$1))) & $2 = (vol (divset (D,$1))) * r );
A1: Seg (len D) = dom D by FINSEQ_1:def_3;
A2: for k being Nat st k in Seg (len D) holds
ex x being Element of REAL n st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len D) implies ex x being Element of REAL n st S1[k,x] )
assume k in Seg (len D) ; ::_thesis: ex x being Element of REAL n st S1[k,x]
then A3: k in dom D by FINSEQ_1:def_3;
dom f = A by FUNCT_2:def_1;
then dom (f | (divset (D,k))) = divset (D,k) by A3, INTEGRA1:8, RELAT_1:62;
then not rng (f | (divset (D,k))) is empty by RELAT_1:42;
then consider r being set such that
A4: r in rng (f | (divset (D,k))) by XBOOLE_0:def_1;
reconsider r = r as Element of REAL n by A4;
(vol (divset (D,k))) * r is Element of REAL n ;
hence ex x being Element of REAL n st S1[k,x] by A4; ::_thesis: verum
end;
consider p being FinSequence of REAL n such that
A5: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds
S1[k,p . k] ) ) from FINSEQ_1:sch_5(A2);
len p = len D by A5, FINSEQ_1:def_3;
hence ex b1 being FinSequence of REAL n st
( len b1 = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL n st
( r in rng (f | (divset (D,i))) & b1 . i = (vol (divset (D,i))) * r ) ) ) by A5, A1; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines middle_volume INTEGR15:def_5_:_
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for D being Division of A
for b5 being FinSequence of REAL n holds
( b5 is middle_volume of f,D iff ( len b5 = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL n st
( r in rng (f | (divset (D,i))) & b5 . i = (vol (divset (D,i))) * r ) ) ) );
definition
let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);
let D be Division of A;
let F be middle_volume of f,D;
func middle_sum (f,F) -> Element of REAL n means :Def6: :: INTEGR15:def 6
for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & it . i = Sum Fi );
existence
ex b1 being Element of REAL n st
for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & b1 . i = Sum Fi )
proof
defpred S1[ Nat, Element of REAL ] means ex i being Element of NAT ex Fi being FinSequence of REAL st
( $1 = i & Fi = (proj (i,n)) * F & $2 = Sum Fi );
A1: for i being Nat st i in Seg n holds
ex x being Element of REAL st S1[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg n implies ex x being Element of REAL st S1[i,x] )
assume i in Seg n ; ::_thesis: ex x being Element of REAL st S1[i,x]
then reconsider ii = i as Element of NAT ;
reconsider Fi = (proj (ii,n)) * F as FinSequence of REAL ;
reconsider x = Sum Fi as Element of REAL ;
take x ; ::_thesis: S1[i,x]
thus ex ii being Element of NAT ex Fi being FinSequence of REAL st
( i = ii & Fi = (proj (ii,n)) * F & x = Sum Fi ) ; ::_thesis: verum
end;
consider p being FinSequence of REAL such that
A2: ( dom p = Seg n & ( for i being Nat st i in Seg n holds
S1[i,p . i] ) ) from FINSEQ_1:sch_5(A1);
take p ; ::_thesis: ( p is Element of REAL n & ( for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & p . i = Sum Fi ) ) )
A3: for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & p . i = Sum Fi )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & p . i = Sum Fi ) )
reconsider k = i as Nat ;
assume i in Seg n ; ::_thesis: ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & p . i = Sum Fi )
then S1[k,p . k] by A2;
hence ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & p . i = Sum Fi ) ; ::_thesis: verum
end;
len p = n by A2, FINSEQ_1:def_3;
hence ( p is Element of REAL n & ( for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & p . i = Sum Fi ) ) ) by A3, FINSEQ_2:92; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of REAL n st ( for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & b1 . i = Sum Fi ) ) & ( for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & b2 . i = Sum Fi ) ) holds
b1 = b2
proof
let x1, x2 be Element of REAL n; ::_thesis: ( ( for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & x1 . i = Sum Fi ) ) & ( for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & x2 . i = Sum Fi ) ) implies x1 = x2 )
assume A4: ( ( for i being Element of NAT st i in Seg n holds
ex Fi1 being FinSequence of REAL st
( Fi1 = (proj (i,n)) * F & x1 . i = Sum Fi1 ) ) & ( for i being Element of NAT st i in Seg n holds
ex Fi2 being FinSequence of REAL st
( Fi2 = (proj (i,n)) * F & x2 . i = Sum Fi2 ) ) ) ; ::_thesis: x1 = x2
A5: for k0 being Nat st k0 in dom x1 holds
x1 . k0 = x2 . k0
proof
let k0 be Nat; ::_thesis: ( k0 in dom x1 implies x1 . k0 = x2 . k0 )
assume A6: k0 in dom x1 ; ::_thesis: x1 . k0 = x2 . k0
then reconsider k = k0 as Element of NAT ;
len x1 = n by CARD_1:def_7;
then k0 in Seg n by A6, FINSEQ_1:def_3;
then ( ex Fi1 being FinSequence of REAL st
( Fi1 = (proj (k,n)) * F & x1 . k = Sum Fi1 ) & ex Fi2 being FinSequence of REAL st
( Fi2 = (proj (k,n)) * F & x2 . k = Sum Fi2 ) ) by A4;
hence x1 . k0 = x2 . k0 ; ::_thesis: verum
end;
A7: len x2 = n by CARD_1:def_7;
len x1 = n by CARD_1:def_7;
then dom x1 = Seg n by FINSEQ_1:def_3
.= dom x2 by A7, FINSEQ_1:def_3 ;
hence x1 = x2 by A5, FINSEQ_1:13; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines middle_sum INTEGR15:def_6_:_
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for D being Division of A
for F being middle_volume of f,D
for b6 being Element of REAL n holds
( b6 = middle_sum (f,F) iff for i being Element of NAT st i in Seg n holds
ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * F & b6 . i = Sum Fi ) );
definition
let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);
let T be DivSequence of A;
mode middle_volume_Sequence of f,T -> Function of NAT,((REAL n) *) means :Def7: :: INTEGR15:def 7
for k being Element of NAT holds it . k is middle_volume of f,T . k;
correctness
existence
ex b1 being Function of NAT,((REAL n) *) st
for k being Element of NAT holds b1 . k is middle_volume of f,T . k;
proof
defpred S1[ Element of NAT , set ] means $2 is middle_volume of f,T . $1;
A1: for x being Element of NAT ex y being Element of (REAL n) * st S1[x,y]
proof
let x be Element of NAT ; ::_thesis: ex y being Element of (REAL n) * st S1[x,y]
set y = the middle_volume of f,T . x;
reconsider y = the middle_volume of f,T . x as Element of (REAL n) * by FINSEQ_1:def_11;
y is middle_volume of f,T . x ;
hence ex y being Element of (REAL n) * st S1[x,y] ; ::_thesis: verum
end;
ex f being Function of NAT,((REAL n) *) st
for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A1);
hence ex b1 being Function of NAT,((REAL n) *) st
for k being Element of NAT holds b1 . k is middle_volume of f,T . k ; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines middle_volume_Sequence INTEGR15:def_7_:_
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for T being DivSequence of A
for b5 being Function of NAT,((REAL n) *) holds
( b5 is middle_volume_Sequence of f,T iff for k being Element of NAT holds b5 . k is middle_volume of f,T . k );
definition
let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
let k be Element of NAT ;
:: original: .
redefine funcS . k -> middle_volume of f,T . k;
coherence
S . k is middle_volume of f,T . k by Def7;
end;
definition
let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);
let T be DivSequence of A;
let S be middle_volume_Sequence of f,T;
func middle_sum (f,S) -> sequence of (REAL-NS n) means :Def8: :: INTEGR15:def 8
for i being Element of NAT holds it . i = middle_sum (f,(S . i));
existence
ex b1 being sequence of (REAL-NS n) st
for i being Element of NAT holds b1 . i = middle_sum (f,(S . i))
proof
deffunc H1( Element of NAT ) -> Element of REAL n = middle_sum (f,(S . $1));
A1: REAL n = the carrier of (REAL-NS n) by REAL_NS1:def_4;
ex IT being sequence of (REAL n) st
for i being Element of NAT holds IT . i = H1(i) from FUNCT_2:sch_4();
hence ex b1 being sequence of (REAL-NS n) st
for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being sequence of (REAL-NS n) st ( for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b2 . i = middle_sum (f,(S . i)) ) holds
b1 = b2
proof
let F1, F2 be sequence of (REAL-NS n); ::_thesis: ( ( for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ) implies F1 = F2 )
assume that
A2: for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) and
A3: for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ; ::_thesis: F1 = F2
for i being Element of NAT holds F1 . i = F2 . i
proof
let i be Element of NAT ; ::_thesis: F1 . i = F2 . i
thus F1 . i = middle_sum (f,(S . i)) by A2
.= F2 . i by A3 ; ::_thesis: verum
end;
hence F1 = F2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines middle_sum INTEGR15:def_8_:_
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for b6 being sequence of (REAL-NS n) holds
( b6 = middle_sum (f,S) iff for i being Element of NAT holds b6 . i = middle_sum (f,(S . i)) );
definition
let n be Nat;
let Z be set ;
let f, g be PartFunc of Z,(REAL n);
funcf + g -> PartFunc of Z,(REAL n) equals :: INTEGR15:def 9
f <++> g;
coherence
f <++> g is PartFunc of Z,(REAL n)
proof
set F = f <++> g;
rng (f <++> g) c= REAL n
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f <++> g) or y in REAL n )
assume y in rng (f <++> g) ; ::_thesis: y in REAL n
then consider x being set such that
A1: x in dom (f <++> g) and
A2: (f <++> g) . x = y by FUNCT_1:def_3;
dom (f <++> g) = (dom f) /\ (dom g) by VALUED_2:def_45;
then ( x in dom f & x in dom g ) by A1, XBOOLE_0:def_4;
then A3: ( f . x = f /. x & g . x = g /. x ) by PARTFUN1:def_6;
(f /. x) + (g /. x) in REAL n ;
hence y in REAL n by A2, A3, A1, VALUED_2:def_45; ::_thesis: verum
end;
hence f <++> g is PartFunc of Z,(REAL n) by RELSET_1:6; ::_thesis: verum
end;
funcf - g -> PartFunc of Z,(REAL n) equals :: INTEGR15:def 10
f <--> g;
coherence
f <--> g is PartFunc of Z,(REAL n)
proof
set F = f <--> g;
rng (f <--> g) c= REAL n
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f <--> g) or y in REAL n )
assume y in rng (f <--> g) ; ::_thesis: y in REAL n
then consider x being set such that
A4: x in dom (f <--> g) and
A5: (f <--> g) . x = y by FUNCT_1:def_3;
dom (f <--> g) = (dom f) /\ (dom g) by VALUED_2:def_46;
then ( x in dom f & x in dom g ) by A4, XBOOLE_0:def_4;
then A6: ( f . x = f /. x & g . x = g /. x ) by PARTFUN1:def_6;
(f /. x) - (g /. x) in REAL n ;
hence y in REAL n by A5, A6, A4, VALUED_2:def_46; ::_thesis: verum
end;
hence f <--> g is PartFunc of Z,(REAL n) by RELSET_1:6; ::_thesis: verum
end;
end;
:: deftheorem defines + INTEGR15:def_9_:_
for n being Nat
for Z being set
for f, g being PartFunc of Z,(REAL n) holds f + g = f <++> g;
:: deftheorem defines - INTEGR15:def_10_:_
for n being Nat
for Z being set
for f, g being PartFunc of Z,(REAL n) holds f - g = f <--> g;
definition
let n be Nat;
let r be real number ;
let Z be set ;
let f be PartFunc of Z,(REAL n);
funcr (#) f -> PartFunc of Z,(REAL n) equals :: INTEGR15:def 11
f [#] r;
coherence
f [#] r is PartFunc of Z,(REAL n)
proof
set F = f [#] r;
rng (f [#] r) c= REAL n
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (f [#] r) or y in REAL n )
assume y in rng (f [#] r) ; ::_thesis: y in REAL n
then consider x being set such that
A1: x in dom (f [#] r) and
A2: (f [#] r) . x = y by FUNCT_1:def_3;
dom (f [#] r) = dom f by VALUED_2:def_39;
then A3: f . x = f /. x by A1, PARTFUN1:def_6;
r * (f /. x) in REAL n ;
hence y in REAL n by A2, A3, A1, VALUED_2:def_39; ::_thesis: verum
end;
hence f [#] r is PartFunc of Z,(REAL n) by RELSET_1:6; ::_thesis: verum
end;
end;
:: deftheorem defines (#) INTEGR15:def_11_:_
for n being Nat
for r being real number
for Z being set
for f being PartFunc of Z,(REAL n) holds r (#) f = f [#] r;
begin
definition
let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);
attrf is bounded means :Def12: :: INTEGR15:def 12
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is bounded ;
end;
:: deftheorem Def12 defines bounded INTEGR15:def_12_:_
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n) holds
( f is bounded iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is bounded );
Lm6: for n, i being Element of NAT
for f being PartFunc of REAL,(REAL n)
for i being Element of NAT
for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A
proof
let n, i be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for i being Element of NAT
for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A
let f be PartFunc of REAL,(REAL n); ::_thesis: for i being Element of NAT
for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A
let i be Element of NAT ; ::_thesis: for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A
let A be Subset of REAL; ::_thesis: (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A
A1: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then A2: rng f c= dom (proj (i,n)) ;
A3: rng (f | A) c= dom (proj (i,n)) by A1;
A4: now__::_thesis:_for_c_being_set_st_c_in_dom_(((proj_(i,n))_*_f)_|_A)_holds_
(((proj_(i,n))_*_f)_|_A)_._c_=_((proj_(i,n))_*_(f_|_A))_._c
let c be set ; ::_thesis: ( c in dom (((proj (i,n)) * f) | A) implies (((proj (i,n)) * f) | A) . c = ((proj (i,n)) * (f | A)) . c )
assume A5: c in dom (((proj (i,n)) * f) | A) ; ::_thesis: (((proj (i,n)) * f) | A) . c = ((proj (i,n)) * (f | A)) . c
then A6: c in (dom ((proj (i,n)) * f)) /\ A by RELAT_1:61;
then A7: c in A by XBOOLE_0:def_4;
A8: c in dom ((proj (i,n)) * f) by A6, XBOOLE_0:def_4;
then c in dom f by A2, RELAT_1:27;
then c in (dom f) /\ A by A7, XBOOLE_0:def_4;
then A9: c in dom (f | A) by RELAT_1:61;
then c in dom ((proj (i,n)) * (f | A)) by A3, RELAT_1:27;
then ((proj (i,n)) * (f | A)) . c = (proj (i,n)) . ((f | A) . c) by FUNCT_1:12
.= (proj (i,n)) . (f . c) by A9, FUNCT_1:47
.= ((proj (i,n)) * f) . c by A8, FUNCT_1:12 ;
hence (((proj (i,n)) * f) | A) . c = ((proj (i,n)) * (f | A)) . c by A5, FUNCT_1:47; ::_thesis: verum
end;
dom (((proj (i,n)) * f) | A) = (dom ((proj (i,n)) * f)) /\ A by RELAT_1:61
.= (dom f) /\ A by A2, RELAT_1:27
.= dom (f | A) by RELAT_1:61
.= dom ((proj (i,n)) * (f | A)) by A3, RELAT_1:27 ;
hence (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A by A4, FUNCT_1:2; ::_thesis: verum
end;
definition
let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);
attrf is integrable means :Def13: :: INTEGR15:def 13
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is integrable ;
end;
:: deftheorem Def13 defines integrable INTEGR15:def_13_:_
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n) holds
( f is integrable iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is integrable );
definition
let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be Function of A,(REAL n);
func integral f -> Element of REAL n means :Def14: :: INTEGR15:def 14
( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds
it . i = integral ((proj (i,n)) * f) ) );
existence
ex b1 being Element of REAL n st
( dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral ((proj (i,n)) * f) ) )
proof
defpred S1[ Nat, Element of REAL ] means ex i being Element of NAT st
( $1 = i & $2 = integral ((proj (i,n)) * f) );
A1: for i being Nat st i in Seg n holds
ex x being Element of REAL st S1[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg n implies ex x being Element of REAL st S1[i,x] )
assume i in Seg n ; ::_thesis: ex x being Element of REAL st S1[i,x]
then reconsider ii = i as Element of NAT ;
consider x being Element of REAL such that
A2: x = integral ((proj (ii,n)) * f) ;
take x ; ::_thesis: S1[i,x]
thus S1[i,x] by A2; ::_thesis: verum
end;
consider p being FinSequence of REAL such that
A3: ( dom p = Seg n & ( for i being Nat st i in Seg n holds
S1[i,p . i] ) ) from FINSEQ_1:sch_5(A1);
take p ; ::_thesis: ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds
p . i = integral ((proj (i,n)) * f) ) )
A4: for i being Element of NAT st i in Seg n holds
p . i = integral ((proj (i,n)) * f)
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies p . i = integral ((proj (i,n)) * f) )
assume i in Seg n ; ::_thesis: p . i = integral ((proj (i,n)) * f)
then S1[i,p . i] by A3;
hence p . i = integral ((proj (i,n)) * f) ; ::_thesis: verum
end;
len p = n by A3, FINSEQ_1:def_3;
hence ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds
p . i = integral ((proj (i,n)) * f) ) ) by A3, A4, FINSEQ_2:92; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of REAL n st dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral ((proj (i,n)) * f) ) & dom b2 = Seg n & ( for i being Element of NAT st i in Seg n holds
b2 . i = integral ((proj (i,n)) * f) ) holds
b1 = b2
proof
let x1, x2 be Element of REAL n; ::_thesis: ( dom x1 = Seg n & ( for i being Element of NAT st i in Seg n holds
x1 . i = integral ((proj (i,n)) * f) ) & dom x2 = Seg n & ( for i being Element of NAT st i in Seg n holds
x2 . i = integral ((proj (i,n)) * f) ) implies x1 = x2 )
assume that
A5: dom x1 = Seg n and
A6: for i being Element of NAT st i in Seg n holds
x1 . i = integral ((proj (i,n)) * f) and
A7: dom x2 = Seg n and
A8: for i being Element of NAT st i in Seg n holds
x2 . i = integral ((proj (i,n)) * f) ; ::_thesis: x1 = x2
now__::_thesis:_for_k_being_Nat_st_k_in_dom_x1_holds_
x1_._k_=_x2_._k
let k be Nat; ::_thesis: ( k in dom x1 implies x1 . k = x2 . k )
assume A9: k in dom x1 ; ::_thesis: x1 . k = x2 . k
then reconsider i = k as Element of NAT ;
x1 . i = integral ((proj (i,n)) * f) by A5, A6, A9
.= x2 . i by A5, A8, A9 ;
hence x1 . k = x2 . k ; ::_thesis: verum
end;
hence x1 = x2 by A5, A7, FINSEQ_1:13; ::_thesis: verum
end;
end;
:: deftheorem Def14 defines integral INTEGR15:def_14_:_
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for b4 being Element of REAL n holds
( b4 = integral f iff ( dom b4 = Seg n & ( for i being Element of NAT st i in Seg n holds
b4 . i = integral ((proj (i,n)) * f) ) ) );
theorem Th11: :: INTEGR15:11
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n)
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
let f be Function of A,(REAL n); ::_thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
let S be middle_volume_Sequence of f,T; ::_thesis: ( f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 implies ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) )
assume that
A1: ( f is bounded & f is integrable ) and
A2: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f )
set seq = middle_sum (f,S);
set xs = integral f;
REAL n = the carrier of (REAL-NS n) by REAL_NS1:def_4;
then reconsider xseq = middle_sum (f,S) as Function of NAT,(REAL n) ;
A3: for i being Element of NAT st i in Seg n holds
ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi ) )
reconsider pjinf = (proj (i,n)) * f as Function of A,REAL ;
defpred S1[ Element of NAT , set ] means $2 = (proj (i,n)) * (S . $1);
A4: for x being Element of NAT ex y being Element of REAL * st S1[x,y]
proof
let x be Element of NAT ; ::_thesis: ex y being Element of REAL * st S1[x,y]
(proj (i,n)) * (S . x) is Element of REAL * by FINSEQ_1:def_11;
hence ex y being Element of REAL * st S1[x,y] ; ::_thesis: verum
end;
consider F being Function of NAT,(REAL *) such that
A5: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A4);
A6: for x being Element of NAT holds
( (proj (i,n)) * (S . x) is FinSequence of REAL & dom ((proj (i,n)) * (S . x)) = Seg (len (S . x)) & rng ((proj (i,n)) * (S . x)) c= REAL )
proof
let x be Element of NAT ; ::_thesis: ( (proj (i,n)) * (S . x) is FinSequence of REAL & dom ((proj (i,n)) * (S . x)) = Seg (len (S . x)) & rng ((proj (i,n)) * (S . x)) c= REAL )
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng (S . x) c= dom (proj (i,n)) ;
then dom ((proj (i,n)) * (S . x)) = dom (S . x) by RELAT_1:27
.= Seg (len (S . x)) by FINSEQ_1:def_3 ;
hence ( (proj (i,n)) * (S . x) is FinSequence of REAL & dom ((proj (i,n)) * (S . x)) = Seg (len (S . x)) & rng ((proj (i,n)) * (S . x)) c= REAL ) ; ::_thesis: verum
end;
for k being Element of NAT holds F . k is middle_volume of pjinf,T . k
proof
let k be Element of NAT ; ::_thesis: F . k is middle_volume of pjinf,T . k
reconsider Tk = T . k as FinSequence ;
reconsider Fk = F . k as FinSequence of REAL by FINSEQ_1:def_11;
A7: F . k = (proj (i,n)) * (S . k) by A5;
then A8: dom Fk = Seg (len (S . k)) by A6
.= Seg (len Tk) by Def5 ;
then A9: dom Fk = dom Tk by FINSEQ_1:def_3;
A10: now__::_thesis:_for_j_being_Nat_st_j_in_dom_Tk_holds_
ex_v_being_Element_of_REAL_st_
(_v_in_rng_(pjinf_|_(divset_((T_._k),j)))_&_Fk_._j_=_v_*_(vol_(divset_((T_._k),j)))_)
let j be Nat; ::_thesis: ( j in dom Tk implies ex v being Element of REAL st
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) ) )
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then A11: rng f c= dom (proj (i,n)) ;
assume A12: j in dom Tk ; ::_thesis: ex v being Element of REAL st
( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )
then consider r being Element of REAL n such that
A13: r in rng (f | (divset ((T . k),j))) and
A14: (S . k) . j = (vol (divset ((T . k),j))) * r by Def5;
reconsider v = (proj (i,n)) . r as Element of REAL ;
take v = v; ::_thesis: ( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) )
consider t being set such that
A15: t in dom (f | (divset ((T . k),j))) and
A16: r = (f | (divset ((T . k),j))) . t by A13, FUNCT_1:def_3;
t in (dom f) /\ (divset ((T . k),j)) by A15, RELAT_1:61;
then t in dom f by XBOOLE_0:def_4;
then A17: t in dom ((proj (i,n)) * f) by A11, RELAT_1:27;
A18: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61
.= (dom pjinf) /\ (divset ((T . k),j)) by A11, RELAT_1:27
.= dom (pjinf | (divset ((T . k),j))) by RELAT_1:61 ;
(proj (i,n)) . r = (proj (i,n)) . (f . t) by A15, A16, FUNCT_1:47
.= ((proj (i,n)) * f) . t by A17, FUNCT_1:12
.= (pjinf | (divset ((T . k),j))) . t by A15, A18, FUNCT_1:47 ;
hence v in rng (pjinf | (divset ((T . k),j))) by A15, A18, FUNCT_1:3; ::_thesis: Fk . j = v * (vol (divset ((T . k),j)))
thus Fk . j = (proj (i,n)) . ((S . k) . j) by A7, A9, A12, FUNCT_1:12
.= ((vol (divset ((T . k),j))) * r) . i by A14, PDIFF_1:def_1
.= (vol (divset ((T . k),j))) * (r . i) by RVSUM_1:44
.= v * (vol (divset ((T . k),j))) by PDIFF_1:def_1 ; ::_thesis: verum
end;
len Fk = len Tk by A8, FINSEQ_1:def_3;
hence F . k is middle_volume of pjinf,T . k by A10, Def1; ::_thesis: verum
end;
then reconsider pjis = F as middle_volume_Sequence of pjinf,T by Def3;
reconsider rseqi = middle_sum (pjinf,pjis) as Real_Sequence ;
assume A19: i in Seg n ; ::_thesis: ex rseqi being Real_Sequence st
for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi )
A20: for k being Element of NAT holds rseqi . k = (xseq . k) . i
proof
let k be Element of NAT ; ::_thesis: rseqi . k = (xseq . k) . i
A21: ex Fi being FinSequence of REAL st
( Fi = (proj (i,n)) * (S . k) & (middle_sum (f,(S . k))) . i = Sum Fi ) by A19, Def6;
thus rseqi . k = middle_sum (pjinf,(pjis . k)) by Def4
.= (middle_sum (f,(S . k))) . i by A5, A21
.= (xseq . k) . i by Def8 ; ::_thesis: verum
end;
take rseqi ; ::_thesis: for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi )
A22: ( (proj (i,n)) * f is bounded & pjinf is integrable ) by A1, A19, Def12, Def13;
then lim (middle_sum (pjinf,pjis)) = integral pjinf by A2, Th9;
hence for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & (integral f) . i = lim rseqi ) by A2, A19, A22, A20, Def14, Th9; ::_thesis: verum
end;
reconsider x = integral f as Point of (REAL-NS n) by REAL_NS1:def_4;
integral f = x ;
hence ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) by A3, REAL_NS1:11; ::_thesis: verum
end;
theorem :: INTEGR15:12
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n) st f is bounded holds
( f is integrable iff ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n) st f is bounded holds
( f is integrable iff ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,(REAL n) st f is bounded holds
( f is integrable iff ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
let f be Function of A,(REAL n); ::_thesis: ( f is bounded implies ( f is integrable iff ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) )
assume A1: f is bounded ; ::_thesis: ( f is integrable iff ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )
hereby ::_thesis: ( ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable )
reconsider I = integral f as Element of REAL n ;
assume A2: f is integrable ; ::_thesis: ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )
take I = I; ::_thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I )
thus for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A1, A2, Th11; ::_thesis: verum
end;
now__::_thesis:_(_ex_I_being_Element_of_REAL_n_st_
for_T_being_DivSequence_of_A
for_S_being_middle_volume_Sequence_of_f,T_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_
(_middle_sum_(f,S)_is_convergent_&_lim_(middle_sum_(f,S))_=_I_)_implies_f_is_integrable_)
assume ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ; ::_thesis: f is integrable
then consider I being Element of REAL n such that
A3: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ;
now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_
(proj_(i,n))_*_f_is_integrable
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * f is integrable )
reconsider Ii = I . i as Element of REAL ;
assume A4: i in Seg n ; ::_thesis: (proj (i,n)) * f is integrable
A5: now__::_thesis:_for_T_being_DivSequence_of_A
for_Si_being_middle_volume_Sequence_of_(proj_(i,n))_*_f,T_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_
(_middle_sum_(((proj_(i,n))_*_f),Si)_is_convergent_&_lim_(middle_sum_(((proj_(i,n))_*_f),Si))_=_Ii_)
set x = I;
let T be DivSequence of A; ::_thesis: for Si being middle_volume_Sequence of (proj (i,n)) * f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii )
let Si be middle_volume_Sequence of (proj (i,n)) * f,T; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii ) )
defpred S1[ Element of NAT , set ] means ex H, z being FinSequence st
( H = T . $1 & z = $2 & len z = len H & ( for j being Element of NAT st j in dom H holds
ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . $1),j))) & (Si . $1) . j = (vol (divset ((T . $1),j))) * ((((proj (i,n)) * f) | (divset ((T . $1),j))) . tji) & rji = (f | (divset ((T . $1),j))) . tji & z . j = (vol (divset ((T . $1),j))) * rji ) ) );
reconsider xs = I as Element of REAL n ;
A6: for k being Element of NAT ex y being Element of (REAL n) * st S1[k,y]
proof
let k be Element of NAT ; ::_thesis: ex y being Element of (REAL n) * st S1[k,y]
reconsider Tk = T . k as FinSequence ;
defpred S2[ Nat, set ] means ex j being Element of NAT st
( $1 = j & ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & $2 = (vol (divset ((T . k),j))) * rji ) );
A7: for j being Nat st j in Seg (len Tk) holds
ex x being Element of REAL n st S2[j,x]
proof
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then A8: rng f c= dom (proj (i,n)) ;
let j0 be Nat; ::_thesis: ( j0 in Seg (len Tk) implies ex x being Element of REAL n st S2[j0,x] )
assume A9: j0 in Seg (len Tk) ; ::_thesis: ex x being Element of REAL n st S2[j0,x]
then reconsider j = j0 as Element of NAT ;
j in dom Tk by A9, FINSEQ_1:def_3;
then consider r being Element of REAL such that
A10: r in rng (((proj (i,n)) * f) | (divset ((T . k),j))) and
A11: (Si . k) . j = r * (vol (divset ((T . k),j))) by Def1;
consider tji being set such that
A12: tji in dom (((proj (i,n)) * f) | (divset ((T . k),j))) and
A13: r = (((proj (i,n)) * f) | (divset ((T . k),j))) . tji by A10, FUNCT_1:def_3;
tji in (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j)) by A12, RELAT_1:61;
then reconsider tji = tji as Element of REAL ;
A14: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61
.= (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j)) by A8, RELAT_1:27
.= dom (((proj (i,n)) * f) | (divset ((T . k),j))) by RELAT_1:61 ;
then (f | (divset ((T . k),j))) . tji in rng (f | (divset ((T . k),j))) by A12, FUNCT_1:3;
then reconsider rji = (f | (divset ((T . k),j))) . tji as Element of REAL n ;
reconsider x = (vol (divset ((T . k),j))) * rji as Element of REAL n ;
take x ; ::_thesis: S2[j0,x]
thus S2[j0,x] by A11, A12, A13, A14; ::_thesis: verum
end;
consider p being FinSequence of REAL n such that
A15: ( dom p = Seg (len Tk) & ( for j being Nat st j in Seg (len Tk) holds
S2[j,p . j] ) ) from FINSEQ_1:sch_5(A7);
reconsider x = p as Element of (REAL n) * by FINSEQ_1:def_11;
take x ; ::_thesis: S1[k,x]
A16: now__::_thesis:_for_jj0_being_Element_of_NAT_st_jj0_in_dom_Tk_holds_
ex_rji_being_Element_of_REAL_n_ex_tji_being_Element_of_REAL_st_
(_tji_in_dom_(f_|_(divset_((T_._k),jj0)))_&_(Si_._k)_._jj0_=_(vol_(divset_((T_._k),jj0)))_*_((((proj_(i,n))_*_f)_|_(divset_((T_._k),jj0)))_._tji)_&_rji_=_(f_|_(divset_((T_._k),jj0)))_._tji_&_p_._jj0_=_(vol_(divset_((T_._k),jj0)))_*_rji_)
let jj0 be Element of NAT ; ::_thesis: ( jj0 in dom Tk implies ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * ((((proj (i,n)) * f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji ) )
reconsider j0 = jj0 as Nat ;
A17: dom Tk = Seg (len Tk) by FINSEQ_1:def_3;
assume jj0 in dom Tk ; ::_thesis: ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * ((((proj (i,n)) * f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji )
then S2[j0,p . j0] by A15, A17;
hence ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * ((((proj (i,n)) * f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji ) ; ::_thesis: verum
end;
len p = len Tk by A15, FINSEQ_1:def_3;
hence S1[k,x] by A16; ::_thesis: verum
end;
consider S being Function of NAT,((REAL n) *) such that
A18: for x being Element of NAT holds S1[x,S . x] from FUNCT_2:sch_3(A6);
for k being Element of NAT holds S . k is middle_volume of f,T . k
proof
let k be Element of NAT ; ::_thesis: S . k is middle_volume of f,T . k
consider H, z being FinSequence such that
A19: ( H = T . k & z = S . k & len H = len z ) and
A20: for j being Element of NAT st j in dom H holds
ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A18;
A21: now__::_thesis:_for_x_being_Nat_st_x_in_dom_H_holds_
ex_rji_being_Element_of_REAL_n_st_
(_rji_in_rng_(f_|_(divset_((T_._k),x)))_&_z_._x_=_(vol_(divset_((T_._k),x)))_*_rji_)
let x be Nat; ::_thesis: ( x in dom H implies ex rji being Element of REAL n st
( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji ) )
assume A22: x in dom H ; ::_thesis: ex rji being Element of REAL n st
( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji )
then reconsider j = x as Element of NAT ;
consider rji being Element of REAL n, tji being Element of REAL such that
A23: tji in dom (f | (divset ((T . k),j))) and
(Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) and
A24: rji = (f | (divset ((T . k),j))) . tji and
A25: z . j = (vol (divset ((T . k),j))) * rji by A20, A22;
take rji = rji; ::_thesis: ( rji in rng (f | (divset ((T . k),x))) & z . x = (vol (divset ((T . k),x))) * rji )
thus rji in rng (f | (divset ((T . k),x))) by A23, A24, FUNCT_1:3; ::_thesis: z . x = (vol (divset ((T . k),x))) * rji
thus z . x = (vol (divset ((T . k),x))) * rji by A25; ::_thesis: verum
end;
S . k is FinSequence of REAL n by FINSEQ_1:def_11;
hence S . k is middle_volume of f,T . k by A19, A21, Def5; ::_thesis: verum
end;
then reconsider S = S as middle_volume_Sequence of f,T by Def7;
set seq = middle_sum (f,S);
REAL n = the carrier of (REAL-NS n) by REAL_NS1:def_4;
then reconsider xseq = middle_sum (f,S) as Function of NAT,(REAL n) ;
assume ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii )
then ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A3;
then consider rseqi being Real_Sequence such that
A26: for k being Element of NAT holds
( rseqi . k = (xseq . k) . i & rseqi is convergent & xs . i = lim rseqi ) by A4, REAL_NS1:11;
for k being Element of NAT holds rseqi . k = (middle_sum (((proj (i,n)) * f),Si)) . k
proof
let k be Element of NAT ; ::_thesis: rseqi . k = (middle_sum (((proj (i,n)) * f),Si)) . k
consider H, z being FinSequence such that
A27: H = T . k and
A28: z = S . k and
A29: len H = len z and
A30: for j being Element of NAT st j in dom H holds
ex rji being Element of REAL n ex tji being Element of REAL st
( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A18;
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng (S . k) c= dom (proj (i,n)) ;
then A31: dom ((proj (i,n)) * (S . k)) = dom (S . k) by RELAT_1:27
.= Seg (len H) by A28, A29, FINSEQ_1:def_3
.= Seg (len (Si . k)) by A27, Def1
.= dom (Si . k) by FINSEQ_1:def_3 ;
A32: for j being Nat st j in dom ((proj (i,n)) * (S . k)) holds
((proj (i,n)) * (S . k)) . j = (Si . k) . j
proof
let j0 be Nat; ::_thesis: ( j0 in dom ((proj (i,n)) * (S . k)) implies ((proj (i,n)) * (S . k)) . j0 = (Si . k) . j0 )
reconsider j = j0 as Element of NAT by ORDINAL1:def_12;
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then A33: rng f c= dom (proj (i,n)) ;
assume A34: j0 in dom ((proj (i,n)) * (S . k)) ; ::_thesis: ((proj (i,n)) * (S . k)) . j0 = (Si . k) . j0
then j0 in Seg (len (Si . k)) by A31, FINSEQ_1:def_3;
then j0 in Seg (len H) by A27, Def1;
then j in dom H by FINSEQ_1:def_3;
then consider rji being Element of REAL n, tji being Element of REAL such that
A35: tji in dom (f | (divset ((T . k),j))) and
A36: (Si . k) . j = (vol (divset ((T . k),j))) * ((((proj (i,n)) * f) | (divset ((T . k),j))) . tji) and
A37: rji = (f | (divset ((T . k),j))) . tji and
A38: z . j = (vol (divset ((T . k),j))) * rji by A30;
A39: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61
.= (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j)) by A33, RELAT_1:27
.= dom (((proj (i,n)) * f) | (divset ((T . k),j))) by RELAT_1:61 ;
then tji in (dom ((proj (i,n)) * f)) /\ (divset ((T . k),j)) by A35, RELAT_1:61;
then A40: tji in dom ((proj (i,n)) * f) by XBOOLE_0:def_4;
A41: (((proj (i,n)) * f) | (divset ((T . k),j))) . tji = ((proj (i,n)) * f) . tji by A35, A39, FUNCT_1:47
.= (proj (i,n)) . (f . tji) by A40, FUNCT_1:12
.= (proj (i,n)) . rji by A35, A37, FUNCT_1:47 ;
((proj (i,n)) * (S . k)) . j = (proj (i,n)) . ((S . k) . j) by A34, FUNCT_1:12
.= ((vol (divset ((T . k),j))) * rji) . i by A28, A38, PDIFF_1:def_1
.= (vol (divset ((T . k),j))) * (rji . i) by RVSUM_1:44
.= (Si . k) . j by A36, A41, PDIFF_1:def_1 ;
hence ((proj (i,n)) * (S . k)) . j0 = (Si . k) . j0 ; ::_thesis: verum
end;
consider Fi being FinSequence of REAL such that
A42: Fi = (proj (i,n)) * (S . k) and
A43: (middle_sum (f,(S . k))) . i = Sum Fi by A4, Def6;
thus rseqi . k = (xseq . k) . i by A26
.= Sum Fi by A43, Def8
.= middle_sum (((proj (i,n)) * f),(Si . k)) by A31, A32, A42, FINSEQ_1:13
.= (middle_sum (((proj (i,n)) * f),Si)) . k by Def4 ; ::_thesis: verum
end;
hence ( middle_sum (((proj (i,n)) * f),Si) is convergent & lim (middle_sum (((proj (i,n)) * f),Si)) = Ii ) by A26, FUNCT_2:63; ::_thesis: verum
end;
(proj (i,n)) * f is bounded by A1, A4, Def12;
hence (proj (i,n)) * f is integrable by A5, Th10; ::_thesis: verum
end;
hence f is integrable by Def13; ::_thesis: verum
end;
hence ( ex I being Element of REAL n st
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable ) ; ::_thesis: verum
end;
definition
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
attrf is bounded means :Def15: :: INTEGR15:def 15
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is bounded ;
end;
:: deftheorem Def15 defines bounded INTEGR15:def_15_:_
for n being Element of NAT
for f being PartFunc of REAL,(REAL n) holds
( f is bounded iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is bounded );
definition
let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,(REAL n);
predf is_integrable_on A means :Def16: :: INTEGR15:def 16
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is_integrable_on A;
end;
:: deftheorem Def16 defines is_integrable_on INTEGR15:def_16_:_
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n) holds
( f is_integrable_on A iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is_integrable_on A );
definition
let n be Element of NAT ;
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,(REAL n);
func integral (f,A) -> Element of REAL n means :Def17: :: INTEGR15:def 17
( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds
it . i = integral (((proj (i,n)) * f),A) ) );
existence
ex b1 being Element of REAL n st
( dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral (((proj (i,n)) * f),A) ) )
proof
defpred S1[ Nat, Element of REAL ] means ex i being Element of NAT st
( $1 = i & $2 = integral (((proj (i,n)) * f),A) );
A1: for i being Nat st i in Seg n holds
ex x being Element of REAL st S1[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg n implies ex x being Element of REAL st S1[i,x] )
assume i in Seg n ; ::_thesis: ex x being Element of REAL st S1[i,x]
then reconsider ii = i as Element of NAT ;
consider x being Element of REAL such that
A2: x = integral (((proj (ii,n)) * f),A) ;
take x ; ::_thesis: S1[i,x]
thus S1[i,x] by A2; ::_thesis: verum
end;
consider p being FinSequence of REAL such that
A3: ( dom p = Seg n & ( for i being Nat st i in Seg n holds
S1[i,p . i] ) ) from FINSEQ_1:sch_5(A1);
take p ; ::_thesis: ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds
p . i = integral (((proj (i,n)) * f),A) ) )
A4: for i being Element of NAT st i in Seg n holds
p . i = integral (((proj (i,n)) * f),A)
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies p . i = integral (((proj (i,n)) * f),A) )
assume i in Seg n ; ::_thesis: p . i = integral (((proj (i,n)) * f),A)
then S1[i,p . i] by A3;
hence p . i = integral (((proj (i,n)) * f),A) ; ::_thesis: verum
end;
len p = n by A3, FINSEQ_1:def_3;
hence ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds
p . i = integral (((proj (i,n)) * f),A) ) ) by A3, A4, FINSEQ_2:92; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of REAL n st dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral (((proj (i,n)) * f),A) ) & dom b2 = Seg n & ( for i being Element of NAT st i in Seg n holds
b2 . i = integral (((proj (i,n)) * f),A) ) holds
b1 = b2
proof
let x1, x2 be Element of REAL n; ::_thesis: ( dom x1 = Seg n & ( for i being Element of NAT st i in Seg n holds
x1 . i = integral (((proj (i,n)) * f),A) ) & dom x2 = Seg n & ( for i being Element of NAT st i in Seg n holds
x2 . i = integral (((proj (i,n)) * f),A) ) implies x1 = x2 )
assume that
A5: dom x1 = Seg n and
A6: for i being Element of NAT st i in Seg n holds
x1 . i = integral (((proj (i,n)) * f),A) and
A7: dom x2 = Seg n and
A8: for i being Element of NAT st i in Seg n holds
x2 . i = integral (((proj (i,n)) * f),A) ; ::_thesis: x1 = x2
for k being Nat st k in dom x1 holds
x1 . k = x2 . k
proof
let k be Nat; ::_thesis: ( k in dom x1 implies x1 . k = x2 . k )
assume A9: k in dom x1 ; ::_thesis: x1 . k = x2 . k
then reconsider k = k as Element of NAT ;
x2 . k = integral (((proj (k,n)) * f),A) by A5, A8, A9;
hence x1 . k = x2 . k by A5, A6, A9; ::_thesis: verum
end;
hence x1 = x2 by A5, A7, FINSEQ_1:13; ::_thesis: verum
end;
end;
:: deftheorem Def17 defines integral INTEGR15:def_17_:_
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for b4 being Element of REAL n holds
( b4 = integral (f,A) iff ( dom b4 = Seg n & ( for i being Element of NAT st i in Seg n holds
b4 . i = integral (((proj (i,n)) * f),A) ) ) );
theorem :: INTEGR15:13
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f | A = g holds
( f is_integrable_on A iff g is integrable )
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f | A = g holds
( f is_integrable_on A iff g is integrable )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f | A = g holds
( f is_integrable_on A iff g is integrable )
let f be PartFunc of REAL,(REAL n); ::_thesis: for g being Function of A,(REAL n) st f | A = g holds
( f is_integrable_on A iff g is integrable )
let g be Function of A,(REAL n); ::_thesis: ( f | A = g implies ( f is_integrable_on A iff g is integrable ) )
assume A1: f | A = g ; ::_thesis: ( f is_integrable_on A iff g is integrable )
thus ( f is_integrable_on A implies g is integrable ) ::_thesis: ( g is integrable implies f is_integrable_on A )
proof
assume A2: f is_integrable_on A ; ::_thesis: g is integrable
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * g is integrable
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * g is integrable )
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f c= dom (proj (i,n)) ;
then A3: dom ((proj (i,n)) * f) = dom f by RELAT_1:27;
A = dom g by FUNCT_2:def_1
.= (dom f) /\ A by A1, RELAT_1:61 ;
then ((proj (i,n)) * f) || A is total by A3, INTEGRA5:6, XBOOLE_1:17;
then reconsider F = ((proj (i,n)) * f) | A as Function of A,REAL ;
assume i in Seg n ; ::_thesis: (proj (i,n)) * g is integrable
then (proj (i,n)) * f is_integrable_on A by A2, Def16;
then F is integrable by INTEGRA5:def_1;
hence (proj (i,n)) * g is integrable by A1, Lm6; ::_thesis: verum
end;
hence g is integrable by Def13; ::_thesis: verum
end;
assume A4: g is integrable ; ::_thesis: f is_integrable_on A
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is_integrable_on A
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * f is_integrable_on A )
assume A5: i in Seg n ; ::_thesis: (proj (i,n)) * f is_integrable_on A
(proj (i,n)) * g = ((proj (i,n)) * f) | A by A1, Lm6;
then ((proj (i,n)) * f) || A is integrable by A4, A5, Def13;
hence (proj (i,n)) * f is_integrable_on A by INTEGRA5:def_1; ::_thesis: verum
end;
hence f is_integrable_on A by Def16; ::_thesis: verum
end;
theorem :: INTEGR15:14
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f | A = g holds
integral (f,A) = integral g
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f | A = g holds
integral (f,A) = integral g
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f | A = g holds
integral (f,A) = integral g
let f be PartFunc of REAL,(REAL n); ::_thesis: for g being Function of A,(REAL n) st f | A = g holds
integral (f,A) = integral g
let g be Function of A,(REAL n); ::_thesis: ( f | A = g implies integral (f,A) = integral g )
assume A1: f | A = g ; ::_thesis: integral (f,A) = integral g
A2: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(integral_(f,A))_holds_
(integral_(f,A))_._k_=_(integral_g)_._k
let k be Nat; ::_thesis: ( k in dom (integral (f,A)) implies (integral (f,A)) . k = (integral g) . k )
assume A3: k in dom (integral (f,A)) ; ::_thesis: (integral (f,A)) . k = (integral g) . k
then reconsider i = k as Element of NAT ;
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f c= dom (proj (i,n)) ;
then A4: dom ((proj (i,n)) * f) = dom f by RELAT_1:27;
A = dom g by FUNCT_2:def_1
.= (dom f) /\ A by A1, RELAT_1:61 ;
then ((proj (i,n)) * f) || A is total by A4, INTEGRA5:6, XBOOLE_1:17;
then reconsider F = ((proj (i,n)) * f) | A as Function of A,REAL ;
A5: F = (proj (i,n)) * g by A1, Lm6;
A6: i in Seg n by A3, Def17;
then (integral (f,A)) . i = integral (((proj (i,n)) * f),A) by Def17
.= integral (((proj (i,n)) * f) || A) ;
hence (integral (f,A)) . k = (integral g) . k by A6, A5, Def14; ::_thesis: verum
end;
dom (integral (f,A)) = Seg n by Def17
.= dom (integral g) by Def14 ;
hence integral (f,A) = integral g by A2, FINSEQ_1:13; ::_thesis: verum
end;
definition
let a, b be real number ;
let n be Element of NAT ;
let f be PartFunc of REAL,(REAL n);
func integral (f,a,b) -> Element of REAL n means :Def18: :: INTEGR15:def 18
( dom it = Seg n & ( for i being Element of NAT st i in Seg n holds
it . i = integral (((proj (i,n)) * f),a,b) ) );
existence
ex b1 being Element of REAL n st
( dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral (((proj (i,n)) * f),a,b) ) )
proof
defpred S1[ Nat, Element of REAL ] means ex i being Element of NAT st
( $1 = i & $2 = integral (((proj (i,n)) * f),a,b) );
A1: for i being Nat st i in Seg n holds
ex x being Element of REAL st S1[i,x]
proof
let i be Nat; ::_thesis: ( i in Seg n implies ex x being Element of REAL st S1[i,x] )
assume i in Seg n ; ::_thesis: ex x being Element of REAL st S1[i,x]
then reconsider ii = i as Element of NAT ;
consider x being Element of REAL such that
A2: x = integral (((proj (ii,n)) * f),a,b) ;
take x ; ::_thesis: S1[i,x]
thus S1[i,x] by A2; ::_thesis: verum
end;
consider p being FinSequence of REAL such that
A3: ( dom p = Seg n & ( for i being Nat st i in Seg n holds
S1[i,p . i] ) ) from FINSEQ_1:sch_5(A1);
take p ; ::_thesis: ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds
p . i = integral (((proj (i,n)) * f),a,b) ) )
A4: for i being Element of NAT st i in Seg n holds
p . i = integral (((proj (i,n)) * f),a,b)
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies p . i = integral (((proj (i,n)) * f),a,b) )
assume i in Seg n ; ::_thesis: p . i = integral (((proj (i,n)) * f),a,b)
then S1[i,p . i] by A3;
hence p . i = integral (((proj (i,n)) * f),a,b) ; ::_thesis: verum
end;
len p = n by A3, FINSEQ_1:def_3;
hence ( p is Element of REAL n & dom p = Seg n & ( for i being Element of NAT st i in Seg n holds
p . i = integral (((proj (i,n)) * f),a,b) ) ) by A3, A4, FINSEQ_2:92; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of REAL n st dom b1 = Seg n & ( for i being Element of NAT st i in Seg n holds
b1 . i = integral (((proj (i,n)) * f),a,b) ) & dom b2 = Seg n & ( for i being Element of NAT st i in Seg n holds
b2 . i = integral (((proj (i,n)) * f),a,b) ) holds
b1 = b2
proof
let x1, x2 be Element of REAL n; ::_thesis: ( dom x1 = Seg n & ( for i being Element of NAT st i in Seg n holds
x1 . i = integral (((proj (i,n)) * f),a,b) ) & dom x2 = Seg n & ( for i being Element of NAT st i in Seg n holds
x2 . i = integral (((proj (i,n)) * f),a,b) ) implies x1 = x2 )
assume that
A5: dom x1 = Seg n and
A6: for i being Element of NAT st i in Seg n holds
x1 . i = integral (((proj (i,n)) * f),a,b) and
A7: dom x2 = Seg n and
A8: for i being Element of NAT st i in Seg n holds
x2 . i = integral (((proj (i,n)) * f),a,b) ; ::_thesis: x1 = x2
for k being Nat st k in dom x1 holds
x1 . k = x2 . k
proof
let k be Nat; ::_thesis: ( k in dom x1 implies x1 . k = x2 . k )
assume A9: k in dom x1 ; ::_thesis: x1 . k = x2 . k
then reconsider k = k as Element of NAT ;
x2 . k = integral (((proj (k,n)) * f),a,b) by A5, A8, A9;
hence x1 . k = x2 . k by A5, A6, A9; ::_thesis: verum
end;
hence x1 = x2 by A5, A7, FINSEQ_1:13; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines integral INTEGR15:def_18_:_
for a, b being real number
for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for b5 being Element of REAL n holds
( b5 = integral (f,a,b) iff ( dom b5 = Seg n & ( for i being Element of NAT st i in Seg n holds
b5 . i = integral (((proj (i,n)) * f),a,b) ) ) );
begin
theorem Th15: :: INTEGR15:15
for Z being set
for n, i being Element of NAT
for f1, f2 being PartFunc of Z,(REAL n) holds
( (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) & (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) )
proof
let Z be set ; ::_thesis: for n, i being Element of NAT
for f1, f2 being PartFunc of Z,(REAL n) holds
( (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) & (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) )
let n, i be Element of NAT ; ::_thesis: for f1, f2 being PartFunc of Z,(REAL n) holds
( (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) & (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) )
let f1, f2 be PartFunc of Z,(REAL n); ::_thesis: ( (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) & (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) )
A1: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f1 c= dom (proj (i,n)) ;
then A2: dom ((proj (i,n)) * f1) = dom f1 by RELAT_1:27;
A3: rng (f1 + f2) c= dom (proj (i,n)) by A1;
then A4: dom ((proj (i,n)) * (f1 + f2)) = dom (f1 + f2) by RELAT_1:27;
rng f2 c= dom (proj (i,n)) by A1;
then A5: dom ((proj (i,n)) * f2) = dom f2 by RELAT_1:27;
A6: dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_2:def_45;
A7: for z being Element of Z st z in dom ((proj (i,n)) * (f1 + f2)) holds
((proj (i,n)) * (f1 + f2)) . z = (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z
proof
let z be Element of Z; ::_thesis: ( z in dom ((proj (i,n)) * (f1 + f2)) implies ((proj (i,n)) * (f1 + f2)) . z = (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z )
reconsider f1z = f1 /. z as Element of n -tuples_on REAL ;
reconsider f2z = f2 /. z as Element of n -tuples_on REAL ;
assume A8: z in dom ((proj (i,n)) * (f1 + f2)) ; ::_thesis: ((proj (i,n)) * (f1 + f2)) . z = (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z
then A9: z in dom (f1 + f2) by A3, RELAT_1:27;
then A10: z in (dom f1) /\ (dom f2) by VALUED_2:def_45;
then z in dom f1 by XBOOLE_0:def_4;
then A11: f1 . z = f1z by PARTFUN1:def_6;
z in dom f2 by A10, XBOOLE_0:def_4;
then A12: f2 . z = f2z by PARTFUN1:def_6;
(proj (i,n)) . ((f1 + f2) . z) = (proj (i,n)) . ((f1 . z) + (f2 . z)) by A9, VALUED_2:def_45;
then (proj (i,n)) . ((f1 + f2) . z) = ((f1 /. z) + (f2 /. z)) . i by A11, A12, PDIFF_1:def_1;
then A13: (proj (i,n)) . ((f1 + f2) . z) = (f1z . i) + (f2z . i) by RVSUM_1:11;
A14: z in (dom ((proj (i,n)) * f1)) /\ (dom ((proj (i,n)) * f2)) by A2, A5, A4, A8, VALUED_2:def_45;
then z in dom ((proj (i,n)) * f1) by XBOOLE_0:def_4;
then ((proj (i,n)) * f1) . z = (proj (i,n)) . (f1 . z) by FUNCT_1:12;
then A15: ((proj (i,n)) * f1) . z = f1z . i by A11, PDIFF_1:def_1;
z in dom ((proj (i,n)) * f2) by A14, XBOOLE_0:def_4;
then ((proj (i,n)) * f2) . z = (proj (i,n)) . (f2 . z) by FUNCT_1:12;
then A16: ((proj (i,n)) * f2) . z = f2z . i by A12, PDIFF_1:def_1;
z in dom (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) by A6, A2, A5, A4, A8, VALUED_1:def_1;
then (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z = (f1z . i) + (f2z . i) by A15, A16, VALUED_1:def_1;
hence ((proj (i,n)) * (f1 + f2)) . z = (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) . z by A8, A13, FUNCT_1:12; ::_thesis: verum
end;
dom ((proj (i,n)) * (f1 + f2)) = dom (((proj (i,n)) * f1) + ((proj (i,n)) * f2)) by A6, A2, A5, A4, VALUED_1:def_1;
hence (proj (i,n)) * (f1 + f2) = ((proj (i,n)) * f1) + ((proj (i,n)) * f2) by A7, PARTFUN1:5; ::_thesis: (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2)
A17: rng (f1 - f2) c= dom (proj (i,n)) by A1;
then A18: dom ((proj (i,n)) * (f1 - f2)) = dom (f1 - f2) by RELAT_1:27;
A19: dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_2:def_46;
then A20: dom ((proj (i,n)) * (f1 - f2)) = dom (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) by A2, A5, A18, VALUED_1:12;
for z being Element of Z st z in dom ((proj (i,n)) * (f1 - f2)) holds
((proj (i,n)) * (f1 - f2)) . z = (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z
proof
let z be Element of Z; ::_thesis: ( z in dom ((proj (i,n)) * (f1 - f2)) implies ((proj (i,n)) * (f1 - f2)) . z = (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z )
reconsider f1z = f1 /. z as Element of n -tuples_on REAL ;
reconsider f2z = f2 /. z as Element of n -tuples_on REAL ;
assume A21: z in dom ((proj (i,n)) * (f1 - f2)) ; ::_thesis: ((proj (i,n)) * (f1 - f2)) . z = (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z
then A22: z in dom (f1 - f2) by A17, RELAT_1:27;
then A23: z in (dom f1) /\ (dom f2) by VALUED_2:def_46;
then z in dom f1 by XBOOLE_0:def_4;
then A24: f1 . z = f1z by PARTFUN1:def_6;
z in dom f2 by A23, XBOOLE_0:def_4;
then A25: f2 . z = f2z by PARTFUN1:def_6;
z in dom ((proj (i,n)) * f2) by A5, A19, A18, A21, XBOOLE_0:def_4;
then ((proj (i,n)) * f2) . z = (proj (i,n)) . (f2 . z) by FUNCT_1:12;
then A26: ((proj (i,n)) * f2) . z = f2z . i by A25, PDIFF_1:def_1;
(proj (i,n)) . ((f1 - f2) . z) = (proj (i,n)) . ((f1 . z) - (f2 . z)) by A22, VALUED_2:def_46;
then (proj (i,n)) . ((f1 - f2) . z) = ((f1 /. z) - (f2 /. z)) . i by A24, A25, PDIFF_1:def_1;
then A27: (proj (i,n)) . ((f1 - f2) . z) = (f1z . i) - (f2z . i) by RVSUM_1:27;
z in dom ((proj (i,n)) * f1) by A2, A19, A18, A21, XBOOLE_0:def_4;
then ((proj (i,n)) * f1) . z = (proj (i,n)) . (f1 . z) by FUNCT_1:12;
then A28: ((proj (i,n)) * f1) . z = f1z . i by A24, PDIFF_1:def_1;
(((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z = (((proj (i,n)) * f1) . z) - (((proj (i,n)) * f2) . z) by A20, A21, VALUED_1:13;
hence ((proj (i,n)) * (f1 - f2)) . z = (((proj (i,n)) * f1) - ((proj (i,n)) * f2)) . z by A21, A27, A28, A26, FUNCT_1:12; ::_thesis: verum
end;
hence (proj (i,n)) * (f1 - f2) = ((proj (i,n)) * f1) - ((proj (i,n)) * f2) by A20, PARTFUN1:5; ::_thesis: verum
end;
theorem Th16: :: INTEGR15:16
for Z being set
for n, i being Element of NAT
for r being Real
for f being PartFunc of Z,(REAL n) holds (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f)
proof
let Z be set ; ::_thesis: for n, i being Element of NAT
for r being Real
for f being PartFunc of Z,(REAL n) holds (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f)
let n, i be Element of NAT ; ::_thesis: for r being Real
for f being PartFunc of Z,(REAL n) holds (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f)
let r be Real; ::_thesis: for f being PartFunc of Z,(REAL n) holds (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f)
let f be PartFunc of Z,(REAL n); ::_thesis: (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f)
A1: dom (r (#) f) = dom f by VALUED_2:def_39;
A2: dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then A3: rng (r (#) f) c= dom (proj (i,n)) ;
rng f c= dom (proj (i,n)) by A2;
then A4: dom ((proj (i,n)) * f) = dom f by RELAT_1:27;
then dom (r (#) ((proj (i,n)) * f)) = dom f by VALUED_1:def_5;
then A5: dom ((proj (i,n)) * (r (#) f)) = dom (r (#) ((proj (i,n)) * f)) by A1, A3, RELAT_1:27;
for z being Element of Z st z in dom (r (#) ((proj (i,n)) * f)) holds
((proj (i,n)) * (r (#) f)) . z = (r (#) ((proj (i,n)) * f)) . z
proof
let z be Element of Z; ::_thesis: ( z in dom (r (#) ((proj (i,n)) * f)) implies ((proj (i,n)) * (r (#) f)) . z = (r (#) ((proj (i,n)) * f)) . z )
reconsider fz = f /. z as Element of n -tuples_on REAL ;
reconsider rfz = (r (#) f) /. z as Element of n -tuples_on REAL ;
assume A6: z in dom (r (#) ((proj (i,n)) * f)) ; ::_thesis: ((proj (i,n)) * (r (#) f)) . z = (r (#) ((proj (i,n)) * f)) . z
then A7: z in dom ((proj (i,n)) * f) by VALUED_1:def_5;
then A8: f . z = fz by A4, PARTFUN1:def_6;
(r (#) ((proj (i,n)) * f)) . z = r * (((proj (i,n)) * f) . z) by A6, VALUED_1:def_5
.= r * ((proj (i,n)) . fz) by A7, A8, FUNCT_1:12 ;
then A9: (r (#) ((proj (i,n)) * f)) . z = r * (fz . i) by PDIFF_1:def_1;
A10: (r (#) f) . z = rfz by A1, A4, A7, PARTFUN1:def_6;
thus ((proj (i,n)) * (r (#) f)) . z = (proj (i,n)) . ((r (#) f) . z) by A5, A6, FUNCT_1:12
.= rfz . i by A10, PDIFF_1:def_1
.= (r (#) fz) . i by A1, A4, A7, A8, A10, VALUED_2:def_39
.= (r (#) ((proj (i,n)) * f)) . z by A9, RVSUM_1:44 ; ::_thesis: verum
end;
hence (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f) by A5, PARTFUN1:5; ::_thesis: verum
end;
theorem :: INTEGR15:17
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds
( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
proof
let n be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL
for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds
( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds
( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded implies ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) )
assume that
A1: ( f1 is_integrable_on A & f2 is_integrable_on A ) and
A2: ( A c= dom f1 & A c= dom f2 ) and
A3: f1 | A is bounded and
A4: f2 | A is bounded ; ::_thesis: ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
A5: for i being Element of NAT st i in Seg n holds
( A c= dom ((proj (i,n)) * f1) & A c= dom ((proj (i,n)) * f2) )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( A c= dom ((proj (i,n)) * f1) & A c= dom ((proj (i,n)) * f2) ) )
assume i in Seg n ; ::_thesis: ( A c= dom ((proj (i,n)) * f1) & A c= dom ((proj (i,n)) * f2) )
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then ( rng f1 c= dom (proj (i,n)) & rng f2 c= dom (proj (i,n)) ) ;
hence ( A c= dom ((proj (i,n)) * f1) & A c= dom ((proj (i,n)) * f2) ) by A2, RELAT_1:27; ::_thesis: verum
end;
A6: for i being Element of NAT st i in Seg n holds
( ((proj (i,n)) * f1) + ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((proj (i,n)) * f1) - ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( ((proj (i,n)) * f1) + ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((proj (i,n)) * f1) - ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) )
assume A7: i in Seg n ; ::_thesis: ( ((proj (i,n)) * f1) + ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((proj (i,n)) * f1) - ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) )
then A8: ( A c= dom ((proj (i,n)) * f1) & A c= dom ((proj (i,n)) * f2) ) by A5;
(proj (i,n)) * (f2 | A) is bounded by A4, A7, Def15;
then A9: ((proj (i,n)) * f2) | A is bounded by Lm6;
(proj (i,n)) * (f1 | A) is bounded by A3, A7, Def15;
then A10: ((proj (i,n)) * f1) | A is bounded by Lm6;
A11: ( (proj (i,n)) * f1 is_integrable_on A & (proj (i,n)) * f2 is_integrable_on A ) by A1, A7, Def16;
hence ( ((proj (i,n)) * f1) + ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) ) by A8, A10, A9, INTEGRA6:11; ::_thesis: ( ((proj (i,n)) * f1) - ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) )
thus ( ((proj (i,n)) * f1) - ((proj (i,n)) * f2) is_integrable_on A & integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) by A8, A10, A9, A11, INTEGRA6:11; ::_thesis: verum
end;
A12: for i being Element of NAT st i in Seg n holds
( (proj (i,n)) * (f1 + f2) is_integrable_on A & (proj (i,n)) * (f1 - f2) is_integrable_on A )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( (proj (i,n)) * (f1 + f2) is_integrable_on A & (proj (i,n)) * (f1 - f2) is_integrable_on A ) )
assume i in Seg n ; ::_thesis: ( (proj (i,n)) * (f1 + f2) is_integrable_on A & (proj (i,n)) * (f1 - f2) is_integrable_on A )
then ( ((proj (i,n)) * f1) + ((proj (i,n)) * f2) is_integrable_on A & ((proj (i,n)) * f1) - ((proj (i,n)) * f2) is_integrable_on A ) by A6;
hence ( (proj (i,n)) * (f1 + f2) is_integrable_on A & (proj (i,n)) * (f1 - f2) is_integrable_on A ) by Th15; ::_thesis: verum
end;
then for i being Element of NAT st i in Seg n holds
(proj (i,n)) * (f1 + f2) is_integrable_on A ;
hence f1 + f2 is_integrable_on A by Def16; ::_thesis: ( f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
A13: for i being Element of NAT st i in Seg n holds
( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) )
assume A14: i in Seg n ; ::_thesis: ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) )
then (integral (f1,A)) . i = integral (((proj (i,n)) * f1),A) by Def17;
hence ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) by A14, Def17; ::_thesis: verum
end;
A15: for i being Element of NAT st i in Seg n holds
( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) ) )
assume A16: i in Seg n ; ::_thesis: ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) )
then ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) + (integral (((proj (i,n)) * f2),A)) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = (integral (((proj (i,n)) * f1),A)) - (integral (((proj (i,n)) * f2),A)) ) by A13;
hence ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) ) by A6, A16; ::_thesis: verum
end;
A17: for i being Element of NAT st i in Seg n holds
( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 + f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 - f2)),A) )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 + f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 - f2)),A) ) )
assume i in Seg n ; ::_thesis: ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 + f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 - f2)),A) )
then ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) + ((proj (i,n)) * f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral ((((proj (i,n)) * f1) - ((proj (i,n)) * f2)),A) ) by A15;
hence ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 + f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 - f2)),A) ) by Th15; ::_thesis: verum
end;
A18: for i being Element of NAT st i in Seg n holds
( (integral ((f1 + f2),A)) . i = ((integral (f1,A)) . i) + ((integral (f2,A)) . i) & (integral ((f1 - f2),A)) . i = ((integral (f1,A)) . i) - ((integral (f2,A)) . i) )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( (integral ((f1 + f2),A)) . i = ((integral (f1,A)) . i) + ((integral (f2,A)) . i) & (integral ((f1 - f2),A)) . i = ((integral (f1,A)) . i) - ((integral (f2,A)) . i) ) )
assume A19: i in Seg n ; ::_thesis: ( (integral ((f1 + f2),A)) . i = ((integral (f1,A)) . i) + ((integral (f2,A)) . i) & (integral ((f1 - f2),A)) . i = ((integral (f1,A)) . i) - ((integral (f2,A)) . i) )
then ( ((integral (f1,A)) . i) + ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 + f2)),A) & ((integral (f1,A)) . i) - ((integral (f2,A)) . i) = integral (((proj (i,n)) * (f1 - f2)),A) ) by A17;
hence ( (integral ((f1 + f2),A)) . i = ((integral (f1,A)) . i) + ((integral (f2,A)) . i) & (integral ((f1 - f2),A)) . i = ((integral (f1,A)) . i) - ((integral (f2,A)) . i) ) by A19, Def17; ::_thesis: verum
end;
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * (f1 - f2) is_integrable_on A by A12;
hence f1 - f2 is_integrable_on A by Def16; ::_thesis: ( integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) )
A20: dom (integral ((f1 + f2),A)) = Seg n by FINSEQ_1:89;
A21: for i being Element of NAT st i in dom (integral ((f1 + f2),A)) holds
(integral ((f1 + f2),A)) . i = ((integral (f1,A)) + (integral (f2,A))) . i
proof
let i be Element of NAT ; ::_thesis: ( i in dom (integral ((f1 + f2),A)) implies (integral ((f1 + f2),A)) . i = ((integral (f1,A)) + (integral (f2,A))) . i )
assume i in dom (integral ((f1 + f2),A)) ; ::_thesis: (integral ((f1 + f2),A)) . i = ((integral (f1,A)) + (integral (f2,A))) . i
then (integral ((f1 + f2),A)) . i = ((integral (f1,A)) . i) + ((integral (f2,A)) . i) by A18, A20;
hence (integral ((f1 + f2),A)) . i = ((integral (f1,A)) + (integral (f2,A))) . i by RVSUM_1:11; ::_thesis: verum
end;
dom ((integral (f1,A)) + (integral (f2,A))) = Seg n by FINSEQ_1:89;
hence integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) by A21, FINSEQ_1:89, PARTFUN1:5; ::_thesis: integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A))
A22: dom (integral ((f1 - f2),A)) = Seg n by FINSEQ_1:89;
A23: for i being Element of NAT st i in dom (integral ((f1 - f2),A)) holds
(integral ((f1 - f2),A)) . i = ((integral (f1,A)) - (integral (f2,A))) . i
proof
let i be Element of NAT ; ::_thesis: ( i in dom (integral ((f1 - f2),A)) implies (integral ((f1 - f2),A)) . i = ((integral (f1,A)) - (integral (f2,A))) . i )
assume i in dom (integral ((f1 - f2),A)) ; ::_thesis: (integral ((f1 - f2),A)) . i = ((integral (f1,A)) - (integral (f2,A))) . i
then (integral ((f1 - f2),A)) . i = ((integral (f1,A)) . i) - ((integral (f2,A)) . i) by A18, A22;
hence (integral ((f1 - f2),A)) . i = ((integral (f1,A)) - (integral (f2,A))) . i by RVSUM_1:27; ::_thesis: verum
end;
dom ((integral (f1,A)) - (integral (f2,A))) = Seg n by FINSEQ_1:89;
hence integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) by A23, FINSEQ_1:89, PARTFUN1:5; ::_thesis: verum
end;
theorem :: INTEGR15:18
for n being Element of NAT
for r being Real
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
proof
let n be Element of NAT ; ::_thesis: for r being Real
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,(REAL n) st A c= dom f & f is_integrable_on A & f | A is bounded holds
( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
let f be PartFunc of REAL,(REAL n); ::_thesis: ( A c= dom f & f is_integrable_on A & f | A is bounded implies ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) )
assume that
A1: A c= dom f and
A2: f is_integrable_on A and
A3: f | A is bounded ; ::_thesis: ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )
A4: now__::_thesis:_for_i_being_Element_of_NAT_holds_A_c=_dom_((proj_(i,n))_*_f)
let i be Element of NAT ; ::_thesis: A c= dom ((proj (i,n)) * f)
dom (proj (i,n)) = REAL n by FUNCT_2:def_1;
then rng f c= dom (proj (i,n)) ;
hence A c= dom ((proj (i,n)) * f) by A1, RELAT_1:27; ::_thesis: verum
end;
A5: for i being Element of NAT st i in Seg n holds
integral ((r (#) ((proj (i,n)) * f)),A) = r * (integral (((proj (i,n)) * f),A))
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies integral ((r (#) ((proj (i,n)) * f)),A) = r * (integral (((proj (i,n)) * f),A)) )
assume A6: i in Seg n ; ::_thesis: integral ((r (#) ((proj (i,n)) * f)),A) = r * (integral (((proj (i,n)) * f),A))
((proj (i,n)) * f) | A = (proj (i,n)) * (f | A) by Lm6;
then A7: ((proj (i,n)) * f) | A is bounded by A3, A6, Def15;
A8: A c= dom ((proj (i,n)) * f) by A4;
(proj (i,n)) * f is_integrable_on A by A2, A6, Def16;
hence integral ((r (#) ((proj (i,n)) * f)),A) = r * (integral (((proj (i,n)) * f),A)) by A7, A8, INTEGRA6:9; ::_thesis: verum
end;
A9: for i being Element of NAT st i in Seg n holds
(r * (integral (f,A))) . i = r * (integral (((proj (i,n)) * f),A))
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (r * (integral (f,A))) . i = r * (integral (((proj (i,n)) * f),A)) )
assume i in Seg n ; ::_thesis: (r * (integral (f,A))) . i = r * (integral (((proj (i,n)) * f),A))
then r * ((integral (f,A)) . i) = r * (integral (((proj (i,n)) * f),A)) by Def17;
hence (r * (integral (f,A))) . i = r * (integral (((proj (i,n)) * f),A)) by RVSUM_1:45; ::_thesis: verum
end;
A10: for i being Element of NAT st i in Seg n holds
(integral ((r (#) f),A)) . i = (r * (integral (f,A))) . i
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (integral ((r (#) f),A)) . i = (r * (integral (f,A))) . i )
A11: integral ((r (#) ((proj (i,n)) * f)),A) = integral (((proj (i,n)) * (r (#) f)),A) by Th16;
assume A12: i in Seg n ; ::_thesis: (integral ((r (#) f),A)) . i = (r * (integral (f,A))) . i
then ( (integral ((r (#) f),A)) . i = integral (((proj (i,n)) * (r (#) f)),A) & (r * (integral (f,A))) . i = r * (integral (((proj (i,n)) * f),A)) ) by A9, Def17;
hence (integral ((r (#) f),A)) . i = (r * (integral (f,A))) . i by A5, A12, A11; ::_thesis: verum
end;
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * (r (#) f) is_integrable_on A
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * (r (#) f) is_integrable_on A )
assume A13: i in Seg n ; ::_thesis: (proj (i,n)) * (r (#) f) is_integrable_on A
((proj (i,n)) * f) | A = (proj (i,n)) * (f | A) by Lm6;
then A14: ((proj (i,n)) * f) | A is bounded by A3, A13, Def15;
A15: A c= dom ((proj (i,n)) * f) by A4;
(proj (i,n)) * f is_integrable_on A by A2, A13, Def16;
then r (#) ((proj (i,n)) * f) is_integrable_on A by A14, A15, INTEGRA6:9;
hence (proj (i,n)) * (r (#) f) is_integrable_on A by Th16; ::_thesis: verum
end;
hence r (#) f is_integrable_on A by Def16; ::_thesis: integral ((r (#) f),A) = r * (integral (f,A))
A16: dom (integral ((r (#) f),A)) = Seg n by FINSEQ_1:89;
then dom (integral ((r (#) f),A)) = dom (r * (integral (f,A))) by FINSEQ_1:89;
hence integral ((r (#) f),A) = r * (integral (f,A)) by A10, A16, PARTFUN1:5; ::_thesis: verum
end;
theorem :: INTEGR15:19
for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
let f be PartFunc of REAL,(REAL n); ::_thesis: for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
let A be non empty closed_interval Subset of REAL; ::_thesis: for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
let a, b be Real; ::_thesis: ( A = [.a,b.] implies integral (f,A) = integral (f,a,b) )
assume A1: A = [.a,b.] ; ::_thesis: integral (f,A) = integral (f,a,b)
A2: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(integral_(f,A))_holds_
(integral_(f,A))_._i_=_(integral_(f,a,b))_._i
let i be Nat; ::_thesis: ( i in dom (integral (f,A)) implies (integral (f,A)) . i = (integral (f,a,b)) . i )
assume A3: i in dom (integral (f,A)) ; ::_thesis: (integral (f,A)) . i = (integral (f,a,b)) . i
then reconsider k = i as Element of NAT ;
dom (integral (f,A)) = Seg n by Def17;
then ( (integral (f,A)) . k = integral (((proj (k,n)) * f),A) & (integral (f,a,b)) . k = integral (((proj (k,n)) * f),a,b) ) by A3, Def17, Def18;
hence (integral (f,A)) . i = (integral (f,a,b)) . i by A1, INTEGRA5:19; ::_thesis: verum
end;
dom (integral (f,A)) = Seg n by Def17
.= dom (integral (f,a,b)) by Def18 ;
hence integral (f,A) = integral (f,a,b) by A2, FINSEQ_1:13; ::_thesis: verum
end;
theorem :: INTEGR15:20
for n being Element of NAT
for f being PartFunc of REAL,(REAL n)
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.b,a.] holds
- (integral (f,A)) = integral (f,a,b)
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n)
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.b,a.] holds
- (integral (f,A)) = integral (f,a,b)
let f be PartFunc of REAL,(REAL n); ::_thesis: for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.b,a.] holds
- (integral (f,A)) = integral (f,a,b)
let A be non empty closed_interval Subset of REAL; ::_thesis: for a, b being Real st A = [.b,a.] holds
- (integral (f,A)) = integral (f,a,b)
let a, b be Real; ::_thesis: ( A = [.b,a.] implies - (integral (f,A)) = integral (f,a,b) )
assume A1: A = [.b,a.] ; ::_thesis: - (integral (f,A)) = integral (f,a,b)
A2: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(-_(integral_(f,A)))_holds_
(-_(integral_(f,A)))_._i_=_(integral_(f,a,b))_._i
let i be Nat; ::_thesis: ( i in dom (- (integral (f,A))) implies (- (integral (f,A))) . i = (integral (f,a,b)) . i )
assume A3: i in dom (- (integral (f,A))) ; ::_thesis: (- (integral (f,A))) . i = (integral (f,a,b)) . i
then reconsider k = i as Element of NAT ;
A4: dom (integral (f,A)) = Seg n by Def17;
A5: k in dom (integral (f,A)) by A3, VALUED_1:8;
then A6: (integral (f,a,b)) . k = integral (((proj (k,n)) * f),a,b) by A4, Def18;
(- (integral (f,A))) . k = - ((integral (f,A)) . k) by VALUED_1:8
.= - (integral (((proj (k,n)) * f),A)) by A5, A4, Def17 ;
hence (- (integral (f,A))) . i = (integral (f,a,b)) . i by A1, A6, INTEGRA5:20; ::_thesis: verum
end;
dom (- (integral (f,A))) = dom ((- 1) (#) (integral (f,A))) by VALUED_1:def_6
.= dom (integral (f,A)) by VALUED_1:def_5
.= Seg n by Def17
.= dom (integral (f,a,b)) by Def18 ;
hence - (integral (f,A)) = integral (f,a,b) by A2, FINSEQ_1:13; ::_thesis: verum
end;
theorem :: INTEGR15:21
for n being Nat
for Z, x being set
for f, g being PartFunc of Z,(REAL n) st x in dom (f + g) holds
(f + g) /. x = (f /. x) + (g /. x)
proof
let n be Nat; ::_thesis: for Z, x being set
for f, g being PartFunc of Z,(REAL n) st x in dom (f + g) holds
(f + g) /. x = (f /. x) + (g /. x)
let Z, x be set ; ::_thesis: for f, g being PartFunc of Z,(REAL n) st x in dom (f + g) holds
(f + g) /. x = (f /. x) + (g /. x)
let f, g be PartFunc of Z,(REAL n); ::_thesis: ( x in dom (f + g) implies (f + g) /. x = (f /. x) + (g /. x) )
assume A1: x in dom (f + g) ; ::_thesis: (f + g) /. x = (f /. x) + (g /. x)
dom (f + g) = (dom f) /\ (dom g) by VALUED_2:def_45;
then ( x in dom f & x in dom g ) by A1, XBOOLE_0:def_4;
then A2: ( f . x = f /. x & g . x = g /. x ) by PARTFUN1:def_6;
thus (f + g) /. x = (f + g) . x by A1, PARTFUN1:def_6
.= (f /. x) + (g /. x) by A1, A2, VALUED_2:def_45 ; ::_thesis: verum
end;
theorem :: INTEGR15:22
for n being Nat
for Z, x being set
for f, g being PartFunc of Z,(REAL n) st x in dom (f - g) holds
(f - g) /. x = (f /. x) - (g /. x)
proof
let n be Nat; ::_thesis: for Z, x being set
for f, g being PartFunc of Z,(REAL n) st x in dom (f - g) holds
(f - g) /. x = (f /. x) - (g /. x)
let Z, x be set ; ::_thesis: for f, g being PartFunc of Z,(REAL n) st x in dom (f - g) holds
(f - g) /. x = (f /. x) - (g /. x)
let f, g be PartFunc of Z,(REAL n); ::_thesis: ( x in dom (f - g) implies (f - g) /. x = (f /. x) - (g /. x) )
assume A1: x in dom (f - g) ; ::_thesis: (f - g) /. x = (f /. x) - (g /. x)
dom (f - g) = (dom f) /\ (dom g) by VALUED_2:def_46;
then ( x in dom f & x in dom g ) by A1, XBOOLE_0:def_4;
then A2: ( f . x = f /. x & g . x = g /. x ) by PARTFUN1:def_6;
thus (f - g) /. x = (f - g) . x by A1, PARTFUN1:def_6
.= (f /. x) - (g /. x) by A1, A2, VALUED_2:def_46 ; ::_thesis: verum
end;
theorem :: INTEGR15:23
for n being Nat
for Z, x being set
for f being PartFunc of Z,(REAL n)
for r being real number st x in dom (r (#) f) holds
(r (#) f) /. x = r * (f /. x)
proof
let n be Nat; ::_thesis: for Z, x being set
for f being PartFunc of Z,(REAL n)
for r being real number st x in dom (r (#) f) holds
(r (#) f) /. x = r * (f /. x)
let Z, x be set ; ::_thesis: for f being PartFunc of Z,(REAL n)
for r being real number st x in dom (r (#) f) holds
(r (#) f) /. x = r * (f /. x)
let f be PartFunc of Z,(REAL n); ::_thesis: for r being real number st x in dom (r (#) f) holds
(r (#) f) /. x = r * (f /. x)
let r be real number ; ::_thesis: ( x in dom (r (#) f) implies (r (#) f) /. x = r * (f /. x) )
assume A1: x in dom (r (#) f) ; ::_thesis: (r (#) f) /. x = r * (f /. x)
dom (r (#) f) = dom f by VALUED_2:def_39;
then A2: f . x = f /. x by A1, PARTFUN1:def_6;
thus (r (#) f) /. x = (r (#) f) . x by A1, PARTFUN1:def_6
.= r * (f /. x) by A1, A2, VALUED_2:def_39 ; ::_thesis: verum
end;