:: INTEGRA5 semantic presentation
begin
theorem Th1: :: INTEGRA5:1
for F, F1, F2 being FinSequence of REAL
for r1, r2 being Real st ( F1 = <*r1*> ^ F or F1 = F ^ <*r1*> ) & ( F2 = <*r2*> ^ F or F2 = F ^ <*r2*> ) holds
Sum (F1 - F2) = r1 - r2
proof
let F, F1, F2 be FinSequence of REAL ; ::_thesis: for r1, r2 being Real st ( F1 = <*r1*> ^ F or F1 = F ^ <*r1*> ) & ( F2 = <*r2*> ^ F or F2 = F ^ <*r2*> ) holds
Sum (F1 - F2) = r1 - r2
let r1, r2 be Real; ::_thesis: ( ( F1 = <*r1*> ^ F or F1 = F ^ <*r1*> ) & ( F2 = <*r2*> ^ F or F2 = F ^ <*r2*> ) implies Sum (F1 - F2) = r1 - r2 )
assume that
A1: ( F1 = <*r1*> ^ F or F1 = F ^ <*r1*> ) and
A2: ( F2 = <*r2*> ^ F or F2 = F ^ <*r2*> ) ; ::_thesis: Sum (F1 - F2) = r1 - r2
len F1 = (len F) + (len <*r1*>) by A1, FINSEQ_1:22;
then A3: len F1 = (len F) + 1 by FINSEQ_1:39;
len F2 = (len <*r2*>) + (len F) by A2, FINSEQ_1:22;
then A4: len F2 = 1 + (len F) by FINSEQ_1:39;
F1 - F2 = diffreal .: (F1,F2) by RVSUM_1:def_6;
then A5: len F1 = len (F1 - F2) by A3, A4, FINSEQ_2:72;
for k being Element of NAT st k in dom F1 holds
(F1 - F2) . k = (F1 /. k) - (F2 /. k)
proof
let k be Element of NAT ; ::_thesis: ( k in dom F1 implies (F1 - F2) . k = (F1 /. k) - (F2 /. k) )
assume A6: k in dom F1 ; ::_thesis: (F1 - F2) . k = (F1 /. k) - (F2 /. k)
then A7: F1 . k = F1 /. k by PARTFUN1:def_6;
A8: k in Seg (len F1) by A6, FINSEQ_1:def_3;
then k in dom F2 by A3, A4, FINSEQ_1:def_3;
then A9: F2 . k = F2 /. k by PARTFUN1:def_6;
k in dom (F1 - F2) by A5, A8, FINSEQ_1:def_3;
hence (F1 - F2) . k = (F1 /. k) - (F2 /. k) by A7, A9, VALUED_1:13; ::_thesis: verum
end;
then A10: Sum (F1 - F2) = (Sum F1) - (Sum F2) by A3, A4, A5, INTEGRA1:22;
( Sum F1 = r1 + (Sum F) & Sum F2 = (Sum F) + r2 ) by A1, A2, RVSUM_1:74, RVSUM_1:76;
hence Sum (F1 - F2) = r1 - r2 by A10; ::_thesis: verum
end;
theorem Th2: :: INTEGRA5:2
for F1, F2 being FinSequence of REAL st len F1 = len F2 holds
( len (F1 + F2) = len F1 & len (F1 - F2) = len F1 & Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) )
proof
let F1, F2 be FinSequence of REAL ; ::_thesis: ( len F1 = len F2 implies ( len (F1 + F2) = len F1 & len (F1 - F2) = len F1 & Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) ) )
assume A1: len F1 = len F2 ; ::_thesis: ( len (F1 + F2) = len F1 & len (F1 - F2) = len F1 & Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) )
F1 + F2 = addreal .: (F1,F2) by RVSUM_1:def_4;
hence A2: len F1 = len (F1 + F2) by A1, FINSEQ_2:72; ::_thesis: ( len (F1 - F2) = len F1 & Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) )
F1 - F2 = diffreal .: (F1,F2) by RVSUM_1:def_6;
hence A3: len F1 = len (F1 - F2) by A1, FINSEQ_2:72; ::_thesis: ( Sum (F1 + F2) = (Sum F1) + (Sum F2) & Sum (F1 - F2) = (Sum F1) - (Sum F2) )
for k being Element of NAT st k in dom F1 holds
(F1 + F2) . k = (F1 /. k) + (F2 /. k)
proof
let k be Element of NAT ; ::_thesis: ( k in dom F1 implies (F1 + F2) . k = (F1 /. k) + (F2 /. k) )
assume A4: k in dom F1 ; ::_thesis: (F1 + F2) . k = (F1 /. k) + (F2 /. k)
then A5: F1 . k = F1 /. k by PARTFUN1:def_6;
A6: k in Seg (len F1) by A4, FINSEQ_1:def_3;
then k in dom F2 by A1, FINSEQ_1:def_3;
then A7: F2 . k = F2 /. k by PARTFUN1:def_6;
k in dom (F1 + F2) by A2, A6, FINSEQ_1:def_3;
hence (F1 + F2) . k = (F1 /. k) + (F2 /. k) by A5, A7, VALUED_1:def_1; ::_thesis: verum
end;
hence Sum (F1 + F2) = (Sum F1) + (Sum F2) by A1, A2, INTEGRA1:21; ::_thesis: Sum (F1 - F2) = (Sum F1) - (Sum F2)
for k being Element of NAT st k in dom F1 holds
(F1 - F2) . k = (F1 /. k) - (F2 /. k)
proof
let k be Element of NAT ; ::_thesis: ( k in dom F1 implies (F1 - F2) . k = (F1 /. k) - (F2 /. k) )
assume A8: k in dom F1 ; ::_thesis: (F1 - F2) . k = (F1 /. k) - (F2 /. k)
then A9: F1 . k = F1 /. k by PARTFUN1:def_6;
A10: k in Seg (len F1) by A8, FINSEQ_1:def_3;
then k in dom F2 by A1, FINSEQ_1:def_3;
then A11: F2 . k = F2 /. k by PARTFUN1:def_6;
k in dom (F1 - F2) by A3, A10, FINSEQ_1:def_3;
hence (F1 - F2) . k = (F1 /. k) - (F2 /. k) by A9, A11, VALUED_1:13; ::_thesis: verum
end;
hence Sum (F1 - F2) = (Sum F1) - (Sum F2) by A1, A3, INTEGRA1:22; ::_thesis: verum
end;
theorem Th3: :: INTEGRA5:3
for F1, F2 being FinSequence of REAL st len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds
F1 . i <= F2 . i ) holds
Sum F1 <= Sum F2
proof
let F1, F2 be FinSequence of REAL ; ::_thesis: ( len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds
F1 . i <= F2 . i ) implies Sum F1 <= Sum F2 )
assume that
A1: len F1 = len F2 and
A2: for i being Element of NAT st i in dom F1 holds
F1 . i <= F2 . i ; ::_thesis: Sum F1 <= Sum F2
reconsider R1 = F1 as Element of (len F1) -tuples_on REAL by FINSEQ_2:92;
reconsider R2 = F2 as Element of (len F1) -tuples_on REAL by A1, FINSEQ_2:92;
for i being Nat st i in Seg (len F1) holds
R1 . i <= R2 . i
proof
let i be Nat; ::_thesis: ( i in Seg (len F1) implies R1 . i <= R2 . i )
assume i in Seg (len F1) ; ::_thesis: R1 . i <= R2 . i
then i in dom F1 by FINSEQ_1:def_3;
hence R1 . i <= R2 . i by A2; ::_thesis: verum
end;
hence Sum F1 <= Sum F2 by RVSUM_1:82; ::_thesis: verum
end;
begin
notation
let f be PartFunc of REAL,REAL;
let C be non empty Subset of REAL;
synonym f || C for f | C;
end;
definition
let f be PartFunc of REAL,REAL;
let C be non empty Subset of REAL;
:: original: ||
redefine funcf || C -> PartFunc of C,REAL;
correctness
coherence
f || C is PartFunc of C,REAL;
by PARTFUN1:10;
end;
theorem Th4: :: INTEGRA5:4
for f, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds (f || C) (#) (g || C) = (f (#) g) || C
proof
let f, g be PartFunc of REAL,REAL; ::_thesis: for C being non empty Subset of REAL holds (f || C) (#) (g || C) = (f (#) g) || C
let C be non empty Subset of REAL; ::_thesis: (f || C) (#) (g || C) = (f (#) g) || C
A1: dom ((f (#) g) || C) = (dom (f (#) g)) /\ C by RELAT_1:61
.= ((dom f) /\ (dom g)) /\ C by VALUED_1:def_4 ;
A2: dom ((f || C) (#) (g || C)) = (dom (f | C)) /\ (dom (g || C)) by VALUED_1:def_4
.= ((dom f) /\ C) /\ (dom (g | C)) by RELAT_1:61
.= ((dom f) /\ C) /\ ((dom g) /\ C) by RELAT_1:61
.= (((dom f) /\ C) /\ C) /\ (dom g) by XBOOLE_1:16
.= ((dom f) /\ (C /\ C)) /\ (dom g) by XBOOLE_1:16
.= ((dom f) /\ C) /\ (dom g) ;
then A3: dom ((f || C) (#) (g || C)) = dom ((f (#) g) || C) by A1, XBOOLE_1:16;
for c being Element of C st c in dom ((f || C) (#) (g || C)) holds
((f || C) (#) (g || C)) . c = ((f (#) g) || C) . c
proof
let c be Element of C; ::_thesis: ( c in dom ((f || C) (#) (g || C)) implies ((f || C) (#) (g || C)) . c = ((f (#) g) || C) . c )
A4: ((f || C) (#) (g || C)) . c = ((f | C) . c) * ((g | C) . c) by VALUED_1:5;
assume A5: c in dom ((f || C) (#) (g || C)) ; ::_thesis: ((f || C) (#) (g || C)) . c = ((f (#) g) || C) . c
then A6: c in (dom (f || C)) /\ (dom (g || C)) by VALUED_1:def_4;
then A7: c in dom (f || C) by XBOOLE_0:def_4;
A8: c in dom (g || C) by A6, XBOOLE_0:def_4;
((f (#) g) || C) . c = (f (#) g) . c by A3, A5, FUNCT_1:47
.= (f . c) * (g . c) by VALUED_1:5
.= ((f | C) . c) * (g . c) by A7, FUNCT_1:47 ;
hence ((f || C) (#) (g || C)) . c = ((f (#) g) || C) . c by A8, A4, FUNCT_1:47; ::_thesis: verum
end;
hence (f || C) (#) (g || C) = (f (#) g) || C by A2, A1, PARTFUN1:5, XBOOLE_1:16; ::_thesis: verum
end;
theorem Th5: :: INTEGRA5:5
for f, g being PartFunc of REAL,REAL
for C being non empty Subset of REAL holds (f + g) || C = (f || C) + (g || C)
proof
let f, g be PartFunc of REAL,REAL; ::_thesis: for C being non empty Subset of REAL holds (f + g) || C = (f || C) + (g || C)
let C be non empty Subset of REAL; ::_thesis: (f + g) || C = (f || C) + (g || C)
A1: dom ((f || C) + (g || C)) = (dom (f | C)) /\ (dom (g || C)) by VALUED_1:def_1
.= ((dom f) /\ C) /\ (dom (g | C)) by RELAT_1:61
.= ((dom f) /\ C) /\ ((dom g) /\ C) by RELAT_1:61
.= (dom f) /\ (C /\ ((dom g) /\ C)) by XBOOLE_1:16
.= (dom f) /\ ((dom g) /\ (C /\ C)) by XBOOLE_1:16
.= (dom f) /\ ((dom g) /\ C) ;
A2: dom ((f + g) || C) = (dom (f + g)) /\ C by RELAT_1:61
.= ((dom f) /\ (dom g)) /\ C by VALUED_1:def_1 ;
then A3: dom ((f + g) || C) = dom ((f || C) + (g || C)) by A1, XBOOLE_1:16;
for c being Element of C st c in dom ((f + g) || C) holds
((f + g) || C) . c = ((f || C) + (g || C)) . c
proof
let c be Element of C; ::_thesis: ( c in dom ((f + g) || C) implies ((f + g) || C) . c = ((f || C) + (g || C)) . c )
assume A4: c in dom ((f + g) || C) ; ::_thesis: ((f + g) || C) . c = ((f || C) + (g || C)) . c
then c in (dom (f + g)) /\ C by RELAT_1:61;
then A5: c in dom (f + g) by XBOOLE_0:def_4;
A6: c in (dom (f || C)) /\ (dom (g || C)) by A3, A4, VALUED_1:def_1;
then A7: c in dom (f || C) by XBOOLE_0:def_4;
A8: ((f + g) || C) . c = (f + g) . c by A4, FUNCT_1:47
.= (f . c) + (g . c) by A5, VALUED_1:def_1 ;
A9: c in dom (g || C) by A6, XBOOLE_0:def_4;
((f || C) + (g || C)) . c = ((f | C) . c) + ((g || C) . c) by A3, A4, VALUED_1:def_1
.= (f . c) + ((g | C) . c) by A7, FUNCT_1:47 ;
hence ((f + g) || C) . c = ((f || C) + (g || C)) . c by A8, A9, FUNCT_1:47; ::_thesis: verum
end;
hence (f + g) || C = (f || C) + (g || C) by A2, A1, PARTFUN1:5, XBOOLE_1:16; ::_thesis: verum
end;
definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,REAL;
predf is_integrable_on A means :Def1: :: INTEGRA5:def 1
f || A is integrable ;
end;
:: deftheorem Def1 defines is_integrable_on INTEGRA5:def_1_:_
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL holds
( f is_integrable_on A iff f || A is integrable );
definition
let A be non empty closed_interval Subset of REAL;
let f be PartFunc of REAL,REAL;
func integral (f,A) -> Real equals :: INTEGRA5:def 2
integral (f || A);
correctness
coherence
integral (f || A) is Real;
;
end;
:: deftheorem defines integral INTEGRA5:def_2_:_
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL holds integral (f,A) = integral (f || A);
theorem Th6: :: INTEGRA5:6
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st A c= dom f holds
f || A is total
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st A c= dom f holds
f || A is total
let f be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f implies f || A is total )
assume A1: A c= dom f ; ::_thesis: f || A is total
dom (f || A) = (dom f) /\ A by RELAT_1:61
.= A by A1, XBOOLE_1:28 ;
hence f || A is total by PARTFUN1:def_2; ::_thesis: verum
end;
theorem :: INTEGRA5:7
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is bounded_above holds
(f || A) | A is bounded_above
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is bounded_above holds
(f || A) | A is bounded_above
let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is bounded_above implies (f || A) | A is bounded_above )
assume f | A is bounded_above ; ::_thesis: (f || A) | A is bounded_above
then consider r being real number such that
A1: for x being set st x in A /\ (dom f) holds
f . x <= r by RFUNCT_1:70;
for x being set st x in A /\ (dom (f || A)) holds
(f || A) . x <= r
proof
let x be set ; ::_thesis: ( x in A /\ (dom (f || A)) implies (f || A) . x <= r )
dom (f | A) = (dom f) /\ A by RELAT_1:61;
then A2: A /\ (dom (f || A)) = (dom f) /\ A by XBOOLE_1:28;
assume A3: x in A /\ (dom (f || A)) ; ::_thesis: (f || A) . x <= r
then x in dom (f | A) by XBOOLE_1:28;
then (f || A) . x = f . x by FUNCT_1:47;
hence (f || A) . x <= r by A1, A3, A2; ::_thesis: verum
end;
hence (f || A) | A is bounded_above by RFUNCT_1:70; ::_thesis: verum
end;
theorem :: INTEGRA5:8
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is bounded_below holds
(f || A) | A is bounded_below
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is bounded_below holds
(f || A) | A is bounded_below
let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is bounded_below implies (f || A) | A is bounded_below )
assume f | A is bounded_below ; ::_thesis: (f || A) | A is bounded_below
then consider r being real number such that
A1: for x being set st x in A /\ (dom f) holds
f . x >= r by RFUNCT_1:71;
for x being set st x in A /\ (dom (f || A)) holds
(f || A) . x >= r
proof
let x be set ; ::_thesis: ( x in A /\ (dom (f || A)) implies (f || A) . x >= r )
dom (f | A) = (dom f) /\ A by RELAT_1:61;
then A2: A /\ (dom (f || A)) = (dom f) /\ A by XBOOLE_1:28;
assume A3: x in A /\ (dom (f || A)) ; ::_thesis: (f || A) . x >= r
then x in dom (f | A) by XBOOLE_1:28;
then (f || A) . x = f . x by FUNCT_1:47;
hence (f || A) . x >= r by A1, A3, A2; ::_thesis: verum
end;
hence (f || A) | A is bounded_below by RFUNCT_1:71; ::_thesis: verum
end;
theorem :: INTEGRA5:9
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is bounded holds
(f || A) | A is bounded
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is bounded holds
(f || A) | A is bounded
let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is bounded implies (f || A) | A is bounded )
assume f | A is bounded ; ::_thesis: (f || A) | A is bounded
then ( (f || A) | A is bounded_above & (f || A) | A is bounded_below ) ;
hence (f || A) | A is bounded ; ::_thesis: verum
end;
begin
theorem Th10: :: INTEGRA5:10
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st A c= dom f & f | A is continuous holds
f | A is bounded
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st A c= dom f & f | A is continuous holds
f | A is bounded
let f be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f & f | A is continuous implies f | A is bounded )
assume A1: A c= dom f ; ::_thesis: ( not f | A is continuous or f | A is bounded )
assume f | A is continuous ; ::_thesis: f | A is bounded
then A2: f .: A is real-bounded by A1, FCONT_1:29, RCOMP_1:10;
then consider a being real number such that
A3: a is UpperBound of f .: A by XXREAL_2:def_10;
A4: for r being real number st r in f .: A holds
r <= a by A3, XXREAL_2:def_1;
consider b being real number such that
A5: b is LowerBound of f .: A by A2, XXREAL_2:def_9;
A6: for r being real number st r in f .: A holds
b <= r by A5, XXREAL_2:def_2;
for x being set st x in A /\ (dom f) holds
b <= f . x
proof
let x be set ; ::_thesis: ( x in A /\ (dom f) implies b <= f . x )
assume x in A /\ (dom f) ; ::_thesis: b <= f . x
then ( x in A & x in dom f ) by XBOOLE_0:def_4;
then f . x in f .: A by FUNCT_1:def_6;
hence b <= f . x by A6; ::_thesis: verum
end;
then A7: f | A is bounded_below by RFUNCT_1:71;
for x being set st x in A /\ (dom f) holds
f . x <= a
proof
let x be set ; ::_thesis: ( x in A /\ (dom f) implies f . x <= a )
assume x in A /\ (dom f) ; ::_thesis: f . x <= a
then ( x in A & x in dom f ) by XBOOLE_0:def_4;
then f . x in f .: A by FUNCT_1:def_6;
hence f . x <= a by A4; ::_thesis: verum
end;
then f | A is bounded_above by RFUNCT_1:70;
hence f | A is bounded by A7; ::_thesis: verum
end;
theorem Th11: :: INTEGRA5:11
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st A c= dom f & f | A is continuous holds
f is_integrable_on A
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st A c= dom f & f | A is continuous holds
f is_integrable_on A
let f be PartFunc of REAL,REAL; ::_thesis: ( A c= dom f & f | A is continuous implies f is_integrable_on A )
assume A1: A c= dom f ; ::_thesis: ( not f | A is continuous or f is_integrable_on A )
reconsider g = f | A as PartFunc of A,REAL by PARTFUN1:10;
A2: dom g = (dom f) /\ A by RELAT_1:61
.= A by A1, XBOOLE_1:28 ;
then A3: g is total by PARTFUN1:def_2;
for y being set st y in f .: A holds
y in rng g
proof
let y be set ; ::_thesis: ( y in f .: A implies y in rng g )
assume y in f .: A ; ::_thesis: y in rng g
then consider x being set such that
x in dom f and
A4: x in A and
A5: y = f . x by FUNCT_1:def_6;
g . x in rng g by A2, A4, FUNCT_1:def_3;
hence y in rng g by A2, A4, A5, FUNCT_1:47; ::_thesis: verum
end;
then A6: f .: A c= rng g by TARSKI:def_3;
for y being set st y in rng g holds
y in f .: A
proof
let y be set ; ::_thesis: ( y in rng g implies y in f .: A )
assume y in rng g ; ::_thesis: y in f .: A
then consider x being set such that
A7: x in dom g and
A8: y = g . x by FUNCT_1:def_3;
f . x in f .: A by A1, A2, A7, FUNCT_1:def_6;
hence y in f .: A by A7, A8, FUNCT_1:47; ::_thesis: verum
end;
then rng g c= f .: A by TARSKI:def_3;
then A9: rng g = f .: A by A6, XBOOLE_0:def_10;
assume A10: f | A is continuous ; ::_thesis: f is_integrable_on A
then f .: A is real-bounded by A1, FCONT_1:29, RCOMP_1:10;
then A11: ( g | A is bounded_above & g | A is bounded_below ) by A9, INTEGRA1:12, INTEGRA1:14;
reconsider g = g as Function of A,REAL by A3;
A12: f | A is uniformly_continuous by A1, A10, FCONT_2:11;
for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0
proof
let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 )
reconsider osc = (upper_sum (g,T)) - (lower_sum (g,T)) as Real_Sequence ;
assume A13: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0
A14: for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc . m) - 0) < r
proof
let r be real number ; ::_thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc . m) - 0) < r )
assume A15: r > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc . m) - 0) < r
ex r1 being Real st
( r1 > 0 & r1 * (vol A) < r )
proof
now__::_thesis:_ex_r1_being_Real_st_
(_r1_>_0_&_r1_*_(vol_A)_<_r_)
percases ( vol A = 0 or vol A > 0 ) by INTEGRA1:9;
supposeA16: vol A = 0 ; ::_thesis: ex r1 being Real st
( r1 > 0 & r1 * (vol A) < r )
consider r1 being Real such that
A17: r1 = 1 ;
r1 * (vol A) < r by A15, A16;
hence ex r1 being Real st
( r1 > 0 & r1 * (vol A) < r ) by A17; ::_thesis: verum
end;
supposeA18: vol A > 0 ; ::_thesis: ex r1 being Real st
( r1 > 0 & r1 * (vol A) < r )
then r / (vol A) > 0 by A15, XREAL_1:139;
then consider r1 being real number such that
A19: 0 < r1 and
A20: r1 < r / (vol A) by XREAL_1:5;
reconsider r1 = r1 as Real by XREAL_0:def_1;
r1 * (vol A) < r by A18, A20, XREAL_1:79;
hence ex r1 being Real st
( r1 > 0 & r1 * (vol A) < r ) by A19; ::_thesis: verum
end;
end;
end;
hence ex r1 being Real st
( r1 > 0 & r1 * (vol A) < r ) ; ::_thesis: verum
end;
then consider r1 being Real such that
A21: r1 > 0 and
A22: r1 * (vol A) < r ;
consider s being Real such that
A23: 0 < s and
A24: for x1, x2 being Real st x1 in dom (f | A) & x2 in dom (f | A) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < r1 by A12, A21, FCONT_2:1;
consider n being Element of NAT such that
A25: for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0) < s by A13, A23, SEQ_2:def_7;
A26: for m being Element of NAT st n <= m holds
((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A)
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A) )
reconsider D = T . m as Division of A ;
len (upper_volume (g,D)) = len D by INTEGRA1:def_6;
then reconsider UV = upper_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
len (lower_volume (g,D)) = len D by INTEGRA1:def_7;
then reconsider LV = lower_volume (g,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
reconsider OSC = UV - LV as Element of (len D) -tuples_on REAL ;
len (upper_volume ((chi (A,A)),D)) = len D by INTEGRA1:def_6;
then reconsider VOL = upper_volume ((chi (A,A)),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
assume A27: n <= m ; ::_thesis: ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A)
A28: for k being Element of NAT st k in dom D holds
((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k)
proof
let k be Element of NAT ; ::_thesis: ( k in dom D implies ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k) )
assume A29: k in dom D ; ::_thesis: ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k)
reconsider h = g | (divset (D,k)) as PartFunc of (divset (D,k)),REAL by PARTFUN1:10;
dom g = A by PARTFUN1:def_2;
then (dom g) /\ (divset (D,k)) = divset (D,k) by A29, INTEGRA1:8, XBOOLE_1:28;
then dom h = divset (D,k) by RELAT_1:61;
then h is total by PARTFUN1:def_2;
then reconsider h = h as Function of (divset (D,k)),REAL ;
A30: for x1, x2 being Real st x1 in divset (D,k) & x2 in divset (D,k) holds
abs ((h . x1) - (h . x2)) <= r1
proof
(upper_volume ((chi (A,A)),D)) . k = vol (divset (D,k)) by A29, INTEGRA1:20;
then A31: (upper_volume ((chi (A,A)),D)) . k >= 0 by INTEGRA1:9;
k in Seg (len D) by A29, FINSEQ_1:def_3;
then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6;
then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3;
then A32: (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3;
dom h = (dom g) /\ (divset (D,k)) by RELAT_1:61;
then A33: dom h c= dom g by XBOOLE_1:17;
let x1, x2 be Real; ::_thesis: ( x1 in divset (D,k) & x2 in divset (D,k) implies abs ((h . x1) - (h . x2)) <= r1 )
assume that
A34: x1 in divset (D,k) and
A35: x2 in divset (D,k) ; ::_thesis: abs ((h . x1) - (h . x2)) <= r1
A36: x2 in dom h by A35, PARTFUN1:def_2;
then g . x2 = h . x2 by FUNCT_1:47;
then A37: f . x2 = h . x2 by A36, A33, FUNCT_1:47;
A38: abs (x1 - x2) <= (delta T) . m
proof
now__::_thesis:_abs_(x1_-_x2)_<=_(delta_T)_._m
percases ( x1 >= x2 or x1 < x2 ) ;
suppose x1 >= x2 ; ::_thesis: abs (x1 - x2) <= (delta T) . m
then x1 - x2 >= 0 by XREAL_1:48;
then A39: abs (x1 - x2) = x1 - x2 by ABSVALUE:def_1;
( x1 <= upper_bound (divset (D,k)) & x2 >= lower_bound (divset (D,k)) ) by A34, A35, INTEGRA2:1;
then abs (x1 - x2) <= (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) by A39, XREAL_1:13;
then A40: abs (x1 - x2) <= vol (divset (D,k)) by INTEGRA1:def_5;
k in Seg (len D) by A29, FINSEQ_1:def_3;
then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6;
then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3;
then (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3;
then (upper_volume ((chi (A,A)),D)) . k <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def_8;
then A41: (upper_volume ((chi (A,A)),D)) . k <= delta (T . m) by INTEGRA3:def_1;
(upper_volume ((chi (A,A)),D)) . k = vol (divset (D,k)) by A29, INTEGRA1:20;
then abs (x1 - x2) <= delta (T . m) by A40, A41, XXREAL_0:2;
hence abs (x1 - x2) <= (delta T) . m by INTEGRA3:def_2; ::_thesis: verum
end;
suppose x1 < x2 ; ::_thesis: abs (x1 - x2) <= (delta T) . m
then x1 - x2 < 0 by XREAL_1:49;
then abs (x1 - x2) = - (x1 - x2) by ABSVALUE:def_1;
then A42: abs (x1 - x2) = x2 - x1 ;
( x2 <= upper_bound (divset (D,k)) & x1 >= lower_bound (divset (D,k)) ) by A34, A35, INTEGRA2:1;
then abs (x1 - x2) <= (upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) by A42, XREAL_1:13;
then A43: abs (x1 - x2) <= vol (divset (D,k)) by INTEGRA1:def_5;
k in Seg (len D) by A29, FINSEQ_1:def_3;
then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6;
then k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3;
then (upper_volume ((chi (A,A)),D)) . k in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def_3;
then (upper_volume ((chi (A,A)),D)) . k <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def_8;
then A44: (upper_volume ((chi (A,A)),D)) . k <= delta (T . m) by INTEGRA3:def_1;
(upper_volume ((chi (A,A)),D)) . k = vol (divset (D,k)) by A29, INTEGRA1:20;
then abs (x1 - x2) <= delta (T . m) by A43, A44, XXREAL_0:2;
hence abs (x1 - x2) <= (delta T) . m by INTEGRA3:def_2; ::_thesis: verum
end;
end;
end;
hence abs (x1 - x2) <= (delta T) . m ; ::_thesis: verum
end;
(delta T) . m = delta D by INTEGRA3:def_2
.= max (rng (upper_volume ((chi (A,A)),D))) by INTEGRA3:def_1 ;
then ((delta T) . m) - 0 >= 0 by A31, A32, XXREAL_2:def_8;
then A45: abs (x1 - x2) <= abs (((delta T) . m) - 0) by A38, ABSVALUE:def_1;
abs (((delta T) . m) - 0) < s by A25, A27;
then A46: abs (x1 - x2) < s by A45, XXREAL_0:2;
A47: x1 in dom h by A34, PARTFUN1:def_2;
then g . x1 = h . x1 by FUNCT_1:47;
then f . x1 = h . x1 by A47, A33, FUNCT_1:47;
hence abs ((h . x1) - (h . x2)) <= r1 by A24, A46, A47, A36, A33, A37; ::_thesis: verum
end;
vol (divset (D,k)) >= 0 by INTEGRA1:9;
then ((upper_bound (rng (g | (divset (D,k))))) - (lower_bound (rng (g | (divset (D,k)))))) * (vol (divset (D,k))) <= r1 * (vol (divset (D,k))) by A30, INTEGRA4:24, XREAL_1:64;
then ((upper_bound (rng (g | (divset (D,k))))) * (vol (divset (D,k)))) - ((lower_bound (rng (g | (divset (D,k))))) * (vol (divset (D,k)))) <= r1 * (vol (divset (D,k))) ;
then ((upper_volume (g,D)) . k) - ((lower_bound (rng (g | (divset (D,k))))) * (vol (divset (D,k)))) <= r1 * (vol (divset (D,k))) by A29, INTEGRA1:def_6;
then ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * (vol (divset (D,k))) by A29, INTEGRA1:def_7;
hence ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) <= r1 * ((upper_volume ((chi (A,A)),D)) . k) by A29, INTEGRA1:20; ::_thesis: verum
end;
for k being Nat st k in Seg (len D) holds
OSC . k <= (r1 * VOL) . k
proof
let k be Nat; ::_thesis: ( k in Seg (len D) implies OSC . k <= (r1 * VOL) . k )
assume k in Seg (len D) ; ::_thesis: OSC . k <= (r1 * VOL) . k
then A48: k in dom D by FINSEQ_1:def_3;
OSC . k = ((upper_volume (g,D)) . k) - ((lower_volume (g,D)) . k) by RVSUM_1:27;
then OSC . k <= r1 * (VOL . k) by A28, A48;
hence OSC . k <= (r1 * VOL) . k by RVSUM_1:45; ::_thesis: verum
end;
then Sum OSC <= Sum (r1 * VOL) by RVSUM_1:82;
then Sum OSC <= r1 * (Sum VOL) by RVSUM_1:87;
then (Sum UV) - (Sum LV) <= r1 * (Sum VOL) by RVSUM_1:90;
then (upper_sum (g,D)) - (Sum LV) <= r1 * (Sum VOL) by INTEGRA1:def_8;
then (upper_sum (g,D)) - (lower_sum (g,D)) <= r1 * (Sum VOL) by INTEGRA1:def_9;
then (upper_sum (g,D)) - (lower_sum (g,D)) <= r1 * (vol A) by INTEGRA1:24;
then ((upper_sum (g,T)) . m) - (lower_sum (g,D)) <= r1 * (vol A) by INTEGRA2:def_2;
hence ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A) by INTEGRA2:def_3; ::_thesis: verum
end;
for m being Element of NAT st n <= m holds
abs ((osc . m) - 0) < r
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((osc . m) - 0) < r )
reconsider D = T . m as Division of A ;
assume n <= m ; ::_thesis: abs ((osc . m) - 0) < r
then ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) <= r1 * (vol A) by A26;
then A49: ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) < r by A22, XXREAL_0:2;
upper_sum (g,D) >= lower_sum (g,D) by A11, INTEGRA1:28;
then (upper_sum (g,T)) . m >= lower_sum (g,D) by INTEGRA2:def_2;
then (upper_sum (g,T)) . m >= (lower_sum (g,T)) . m by INTEGRA2:def_3;
then A50: ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) >= 0 by XREAL_1:48;
osc . m = ((upper_sum (g,T)) . m) + ((- (lower_sum (g,T))) . m) by SEQ_1:7
.= ((upper_sum (g,T)) . m) + (- ((lower_sum (g,T)) . m)) by SEQ_1:10
.= ((upper_sum (g,T)) . m) - ((lower_sum (g,T)) . m) ;
hence abs ((osc . m) - 0) < r by A49, A50, ABSVALUE:def_1; ::_thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((osc . m) - 0) < r ; ::_thesis: verum
end;
then osc is convergent by SEQ_2:def_6;
then A51: lim osc = 0 by A14, SEQ_2:def_7;
( upper_sum (g,T) is convergent & lower_sum (g,T) is convergent ) by A11, A13, INTEGRA4:8, INTEGRA4:9;
hence (lim (upper_sum (g,T))) - (lim (lower_sum (g,T))) = 0 by A51, SEQ_2:12; ::_thesis: verum
end;
then g is integrable by A11, INTEGRA4:12;
hence f is_integrable_on A by Def1; ::_thesis: verum
end;
theorem Th12: :: INTEGRA5:12
for A being non empty closed_interval Subset of REAL
for X being set
for f being PartFunc of REAL,REAL
for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds
( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for X being set
for f being PartFunc of REAL,REAL
for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds
( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL
for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds
( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )
let f be PartFunc of REAL,REAL; ::_thesis: for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds
( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )
let D be Division of A; ::_thesis: ( A c= X & f is_differentiable_on X & (f `| X) | A is bounded implies ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) ) )
assume that
A1: A c= X and
A2: f is_differentiable_on X and
A3: (f `| X) | A is bounded ; ::_thesis: ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )
(len D) - 1 in NAT
proof
ex j being Nat st len D = 1 + j by NAT_1:10, NAT_1:14;
hence (len D) - 1 in NAT by ORDINAL1:def_12; ::_thesis: verum
end;
then reconsider k1 = (len D) - 1 as Element of NAT ;
deffunc H1( Nat) -> Element of REAL = f . (lower_bound (divset (D,($1 + 1))));
deffunc H2( Nat) -> Element of REAL = (f . (upper_bound (divset (D,$1)))) - (f . (lower_bound (divset (D,$1))));
consider p being FinSequence of REAL such that
A4: ( len p = len D & ( for i being Nat st i in dom p holds
p . i = H2(i) ) ) from FINSEQ_2:sch_1();
X c= dom f by A2, FDIFF_1:def_6;
then A5: A c= dom f by A1, XBOOLE_1:1;
A6: for k being Element of NAT st k in dom D holds
ex r being Real st
( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )
proof
let k be Element of NAT ; ::_thesis: ( k in dom D implies ex r being Real st
( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) )
assume A7: k in dom D ; ::_thesis: ex r being Real st
( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )
now__::_thesis:_ex_r_being_Real_st_
(_r_in_divset_(D,k)_&_(f_._(upper_bound_(divset_(D,k))))_-_(f_._(lower_bound_(divset_(D,k))))_=_(diff_(f,r))_*_(vol_(divset_(D,k)))_)
percases ( lower_bound (divset (D,k)) = upper_bound (divset (D,k)) or lower_bound (divset (D,k)) <> upper_bound (divset (D,k)) ) ;
supposeA8: lower_bound (divset (D,k)) = upper_bound (divset (D,k)) ; ::_thesis: ex r being Real st
( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )
consider r being Real such that
A9: r = upper_bound (divset (D,k)) ;
A10: r in divset (D,k)
proof
ex a, b being Real st
( a <= b & a = lower_bound (divset (D,k)) & b = upper_bound (divset (D,k)) ) by SEQ_4:11;
hence r in divset (D,k) by A9, INTEGRA2:1; ::_thesis: verum
end;
(upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = 0 by A8;
then vol (divset (D,k)) = 0 by INTEGRA1:def_5;
then (diff (f,r)) * (vol (divset (D,k))) = 0 ;
hence ex r being Real st
( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) by A8, A10; ::_thesis: verum
end;
supposeA11: lower_bound (divset (D,k)) <> upper_bound (divset (D,k)) ; ::_thesis: ex r being Real st
( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )
ex r1, r2 being Real st
( r1 <= r2 & r1 = lower_bound (divset (D,k)) & r2 = upper_bound (divset (D,k)) ) by SEQ_4:11;
then A12: lower_bound (divset (D,k)) < upper_bound (divset (D,k)) by A11, XXREAL_0:1;
f | X is continuous by A2, FDIFF_1:25;
then f | A is continuous by A1, FCONT_1:16;
then A13: f | (divset (D,k)) is continuous by A7, FCONT_1:16, INTEGRA1:8;
A14: divset (D,k) = [.(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).] by INTEGRA1:4;
then A15: ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ c= divset (D,k) by XXREAL_1:25;
A16: divset (D,k) c= A by A7, INTEGRA1:8;
then ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ c= A by A15, XBOOLE_1:1;
then f is_differentiable_on ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ by A1, A2, FDIFF_1:26, XBOOLE_1:1;
then consider r being Real such that
A17: r in ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ and
A18: diff (f,r) = ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) / ((upper_bound (divset (D,k))) - (lower_bound (divset (D,k)))) by A5, A16, A13, A12, A14, ROLLE:3, XBOOLE_1:1;
(upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) > 0 by A12, XREAL_1:50;
then (diff (f,r)) * ((upper_bound (divset (D,k))) - (lower_bound (divset (D,k)))) = (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) by A18, XCMPLX_1:87;
then (diff (f,r)) * (vol (divset (D,k))) = (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) by INTEGRA1:def_5;
hence ex r being Real st
( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) by A15, A17; ::_thesis: verum
end;
end;
end;
hence ex r being Real st
( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) ; ::_thesis: verum
end;
A19: dom p = Seg (len D) by A4, FINSEQ_1:def_3;
A20: for i being Element of NAT st i in Seg k1 holds
upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))
proof
let i be Element of NAT ; ::_thesis: ( i in Seg k1 implies upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) )
assume A21: i in Seg k1 ; ::_thesis: upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))
then i <= k1 by FINSEQ_1:1;
then A22: i + 1 <= k1 + 1 by XREAL_1:7;
1 <= i by A21, FINSEQ_1:1;
then 1 + 0 <= i + 1 by XREAL_1:7;
then i + 1 in Seg (len D) by A22, FINSEQ_1:1;
then A23: i + 1 in dom D by FINSEQ_1:def_3;
k1 + 1 = len D ;
then k1 <= len D by NAT_1:11;
then Seg k1 c= Seg (len D) by FINSEQ_1:5;
then i in Seg (len D) by A21;
then A24: i in dom D by FINSEQ_1:def_3;
A25: (i + 1) - 1 = i ;
now__::_thesis:_upper_bound_(divset_(D,i))_=_lower_bound_(divset_(D,(i_+_1)))
percases ( i = 1 or i <> 1 ) ;
supposeA26: i = 1 ; ::_thesis: upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))
then upper_bound (divset (D,i)) = D . i by A24, INTEGRA1:def_4;
hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) by A23, A25, A26, INTEGRA1:def_4; ::_thesis: verum
end;
supposeA27: i <> 1 ; ::_thesis: upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))
i >= 1 by A21, FINSEQ_1:1;
then i + 1 >= 1 + 1 by XREAL_1:6;
then A28: i + 1 <> 1 ;
upper_bound (divset (D,i)) = D . i by A24, A27, INTEGRA1:def_4;
hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) by A23, A25, A28, INTEGRA1:def_4; ::_thesis: verum
end;
end;
end;
hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) ; ::_thesis: verum
end;
consider s2 being FinSequence of REAL such that
A29: ( len s2 = k1 & ( for i being Nat st i in dom s2 holds
s2 . i = H1(i) ) ) from FINSEQ_2:sch_1();
A30: for k being Element of NAT st k in dom D holds
rng (((f `| X) || A) | (divset (D,k))) is real-bounded
proof
dom (f `| X) = X by A2, FDIFF_1:def_7;
then reconsider g = f `| X as PartFunc of X,REAL by RELSET_1:5;
let k be Element of NAT ; ::_thesis: ( k in dom D implies rng (((f `| X) || A) | (divset (D,k))) is real-bounded )
assume k in dom D ; ::_thesis: rng (((f `| X) || A) | (divset (D,k))) is real-bounded
consider r1 being real number such that
A31: for x being set st x in A /\ (dom (f `| X)) holds
(f `| X) . x <= r1 by A3, RFUNCT_1:70;
consider r2 being real number such that
A32: for x being set st x in A /\ (dom (f `| X)) holds
(f `| X) . x >= r2 by A3, RFUNCT_1:71;
A33: dom ((f `| X) | A) = (dom (f `| X)) /\ A by RELAT_1:61;
for x being set st x in A /\ (dom ((f `| X) || A)) holds
((f `| X) || A) . x >= r2
proof
let x be set ; ::_thesis: ( x in A /\ (dom ((f `| X) || A)) implies ((f `| X) || A) . x >= r2 )
A34: A /\ (A /\ (dom (f `| X))) = (A /\ A) /\ (dom (f `| X)) by XBOOLE_1:16
.= A /\ (dom (f `| X)) ;
reconsider y = g . x as Real ;
assume A35: x in A /\ (dom ((f `| X) || A)) ; ::_thesis: ((f `| X) || A) . x >= r2
then y >= r2 by A32, A33, A34;
hence ((f `| X) || A) . x >= r2 by A33, A35, A34, FUNCT_1:47; ::_thesis: verum
end;
then ((f `| X) || A) | A is bounded_below by RFUNCT_1:71;
then A36: rng (((f `| X) || A) | (divset (D,k))) is bounded_below by INTEGRA4:19;
for x being set st x in A /\ (dom ((f `| X) || A)) holds
((f `| X) || A) . x <= r1
proof
let x be set ; ::_thesis: ( x in A /\ (dom ((f `| X) || A)) implies ((f `| X) || A) . x <= r1 )
A37: A /\ (A /\ (dom (f `| X))) = (A /\ A) /\ (dom (f `| X)) by XBOOLE_1:16
.= A /\ (dom (f `| X)) ;
reconsider y = g . x as Real ;
assume A38: x in A /\ (dom ((f `| X) || A)) ; ::_thesis: ((f `| X) || A) . x <= r1
then y <= r1 by A31, A33, A37;
hence ((f `| X) || A) . x <= r1 by A33, A38, A37, FUNCT_1:47; ::_thesis: verum
end;
then ((f `| X) || A) | A is bounded_above by RFUNCT_1:70;
then rng (((f `| X) || A) | (divset (D,k))) is bounded_above by INTEGRA4:18;
hence rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A36; ::_thesis: verum
end;
deffunc H3( Nat) -> Element of REAL = f . (upper_bound (divset (D,$1)));
consider s1 being FinSequence of REAL such that
A39: ( len s1 = k1 & ( for i being Nat st i in dom s1 holds
s1 . i = H3(i) ) ) from FINSEQ_2:sch_1();
A40: dom s2 = Seg k1 by A29, FINSEQ_1:def_3;
( len (s1 ^ <*(f . (upper_bound A))*>) = len (<*(f . (lower_bound A))*> ^ s2) & len (s1 ^ <*(f . (upper_bound A))*>) = len p & ( for i being Element of NAT st i in dom (s1 ^ <*(f . (upper_bound A))*>) holds
p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) ) )
proof
dom <*(f . (upper_bound A))*> = Seg 1 by FINSEQ_1:def_8;
then len <*(f . (upper_bound A))*> = 1 by FINSEQ_1:def_3;
then A41: len (s1 ^ <*(f . (upper_bound A))*>) = k1 + 1 by A39, FINSEQ_1:22;
dom <*(f . (lower_bound A))*> = Seg 1 by FINSEQ_1:def_8;
then len <*(f . (lower_bound A))*> = 1 by FINSEQ_1:def_3;
hence A42: len (s1 ^ <*(f . (upper_bound A))*>) = len (<*(f . (lower_bound A))*> ^ s2) by A29, A41, FINSEQ_1:22; ::_thesis: ( len (s1 ^ <*(f . (upper_bound A))*>) = len p & ( for i being Element of NAT st i in dom (s1 ^ <*(f . (upper_bound A))*>) holds
p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) ) )
thus len (s1 ^ <*(f . (upper_bound A))*>) = len p by A4, A41; ::_thesis: for i being Element of NAT st i in dom (s1 ^ <*(f . (upper_bound A))*>) holds
p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i)
let i be Element of NAT ; ::_thesis: ( i in dom (s1 ^ <*(f . (upper_bound A))*>) implies p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) )
assume A43: i in dom (s1 ^ <*(f . (upper_bound A))*>) ; ::_thesis: p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i)
then A44: (s1 ^ <*(f . (upper_bound A))*>) /. i = (s1 ^ <*(f . (upper_bound A))*>) . i by PARTFUN1:def_6;
i in Seg (len (s1 ^ <*(f . (upper_bound A))*>)) by A43, FINSEQ_1:def_3;
then i in dom (<*(f . (lower_bound A))*> ^ s2) by A42, FINSEQ_1:def_3;
then A45: (<*(f . (lower_bound A))*> ^ s2) /. i = (<*(f . (lower_bound A))*> ^ s2) . i by PARTFUN1:def_6;
A46: ( len D = 1 or not len D is trivial ) by NAT_2:def_1;
now__::_thesis:_p_._i_=_((s1_^_<*(f_._(upper_bound_A))*>)_/._i)_-_((<*(f_._(lower_bound_A))*>_^_s2)_/._i)
percases ( len D = 1 or len D >= 2 ) by A46, NAT_2:29;
supposeA47: len D = 1 ; ::_thesis: p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i)
then A48: i in Seg 1 by A41, A43, FINSEQ_1:def_3;
then A49: i = 1 by FINSEQ_1:2, TARSKI:def_1;
s1 = {} by A39, A47;
then s1 ^ <*(f . (upper_bound A))*> = <*(f . (upper_bound A))*> by FINSEQ_1:34;
then A50: (s1 ^ <*(f . (upper_bound A))*>) /. i = f . (upper_bound A) by A44, A49, FINSEQ_1:def_8;
A51: i in dom D by A47, A48, FINSEQ_1:def_3;
s2 = {} by A29, A47;
then <*(f . (lower_bound A))*> ^ s2 = <*(f . (lower_bound A))*> by FINSEQ_1:34;
then A52: (<*(f . (lower_bound A))*> ^ s2) /. i = f . (lower_bound A) by A45, A49, FINSEQ_1:def_8;
D . i = upper_bound A by A47, A49, INTEGRA1:def_2;
then A53: upper_bound (divset (D,i)) = upper_bound A by A49, A51, INTEGRA1:def_4;
p . i = (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) by A4, A19, A47, A48;
hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) by A49, A51, A50, A52, A53, INTEGRA1:def_4; ::_thesis: verum
end;
supposeA54: len D >= 2 ; ::_thesis: p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i)
1 = 2 - 1 ;
then A55: k1 >= 1 by A54, XREAL_1:9;
now__::_thesis:_p_._i_=_((s1_^_<*(f_._(upper_bound_A))*>)_/._i)_-_((<*(f_._(lower_bound_A))*>_^_s2)_/._i)
percases ( i = 1 or i = len D or ( i <> 1 & i <> len D ) ) ;
supposeA56: i = 1 ; ::_thesis: p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i)
then A57: i in Seg 1 by FINSEQ_1:2, TARSKI:def_1;
then i in dom <*(f . (lower_bound A))*> by FINSEQ_1:def_8;
then (<*(f . (lower_bound A))*> ^ s2) . i = <*(f . (lower_bound A))*> . i by FINSEQ_1:def_7;
then A58: (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound A) by A56, FINSEQ_1:def_8;
Seg 1 c= Seg k1 by A55, FINSEQ_1:5;
then i in Seg k1 by A57;
then A59: i in dom s1 by A39, FINSEQ_1:def_3;
then (s1 ^ <*(f . (upper_bound A))*>) . i = s1 . i by FINSEQ_1:def_7;
then A60: (s1 ^ <*(f . (upper_bound A))*>) . i = f . (upper_bound (divset (D,i))) by A39, A59;
A61: i in Seg 2 by A56, FINSEQ_1:2, TARSKI:def_2;
A62: Seg 2 c= Seg (len D) by A54, FINSEQ_1:5;
then i in Seg (len D) by A61;
then A63: i in dom D by FINSEQ_1:def_3;
p . i = (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) by A4, A19, A62, A61;
hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) by A44, A45, A56, A63, A60, A58, INTEGRA1:def_4; ::_thesis: verum
end;
supposeA64: i = len D ; ::_thesis: p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i)
then i - (len s1) in Seg 1 by A39, FINSEQ_1:2, TARSKI:def_1;
then A65: i - (len s1) in dom <*(f . (upper_bound A))*> by FINSEQ_1:def_8;
i = (i - (len s1)) + (len s1) ;
then (s1 ^ <*(f . (upper_bound A))*>) . i = <*(f . (upper_bound A))*> . (i - (len s1)) by A65, FINSEQ_1:def_7;
then A66: (s1 ^ <*(f . (upper_bound A))*>) /. i = f . (upper_bound A) by A39, A44, A64, FINSEQ_1:def_8;
A67: i - (len <*(f . (lower_bound A))*>) = i - 1 by FINSEQ_1:40;
A68: i <> 1 by A54, A64;
i in Seg (len D) by A64, FINSEQ_1:3;
then A69: i in dom D by FINSEQ_1:def_3;
p . i = (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) by A4, A19, A64, FINSEQ_1:3;
then p . i = (f . (upper_bound (divset (D,i)))) - (f . (D . (i - 1))) by A69, A68, INTEGRA1:def_4;
then A70: p . i = (f . (D . i)) - (f . (D . (i - 1))) by A69, A68, INTEGRA1:def_4;
i - 1 <> 0 by A54, A64;
then i - 1 in Seg k1 by A64, FINSEQ_1:3;
then A71: ( (len <*(f . (lower_bound A))*>) + (i - (len <*(f . (lower_bound A))*>)) = i & i - (len <*(f . (lower_bound A))*>) in dom s2 ) by A29, A67, FINSEQ_1:def_3;
then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . (i - (len <*(f . (lower_bound A))*>)) by FINSEQ_1:def_7;
then (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound (divset (D,i))) by A29, A67, A71;
then (<*(f . (lower_bound A))*> ^ s2) . i = f . (D . (i - 1)) by A69, A68, INTEGRA1:def_4;
hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) by A45, A64, A66, A70, INTEGRA1:def_2; ::_thesis: verum
end;
supposeA72: ( i <> 1 & i <> len D ) ; ::_thesis: p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i)
(len s1) + (len <*(f . (upper_bound A))*>) = k1 + 1 by A39, FINSEQ_1:39;
then A73: i in Seg (len D) by A43, FINSEQ_1:def_7;
A74: ( i in dom s1 & i in Seg k1 & i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 )
proof
i <> 0 by A73, FINSEQ_1:1;
then not i is trivial by A72, NAT_2:def_1;
then i >= 1 + 1 by NAT_2:29;
then A75: i - 1 >= 1 by XREAL_1:19;
A76: 1 <= i by A73, FINSEQ_1:1;
i <= len D by A73, FINSEQ_1:1;
then A77: i < k1 + 1 by A72, XXREAL_0:1;
then A78: i <= k1 by NAT_1:13;
then i in Seg (len s1) by A39, A76, FINSEQ_1:1;
hence i in dom s1 by FINSEQ_1:def_3; ::_thesis: ( i in Seg k1 & i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 )
thus i in Seg k1 by A76, A78, FINSEQ_1:1; ::_thesis: ( i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 )
i <= k1 by A77, NAT_1:13;
then i - 1 <= k1 - 1 by XREAL_1:9;
then A79: (i - 1) + 0 <= (k1 - 1) + 1 by XREAL_1:7;
ex j being Nat st i = 1 + j by A76, NAT_1:10;
hence i - 1 in Seg k1 by A75, A79, FINSEQ_1:1; ::_thesis: ( (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 )
then A80: i - (len <*(f . (lower_bound A))*>) in Seg (len s2) by A29, FINSEQ_1:39;
thus (i - 1) + 1 = i ; ::_thesis: i - (len <*(f . (lower_bound A))*>) in dom s2
thus i - (len <*(f . (lower_bound A))*>) in dom s2 by A80, FINSEQ_1:def_3; ::_thesis: verum
end;
then A81: i - (len <*(f . (lower_bound A))*>) in Seg (len s2) by FINSEQ_1:def_3;
then i - (len <*(f . (lower_bound A))*>) <= len s2 by FINSEQ_1:1;
then A82: i <= (len <*(f . (lower_bound A))*>) + (len s2) by XREAL_1:20;
1 <= i - (len <*(f . (lower_bound A))*>) by A81, FINSEQ_1:1;
then (len <*(f . (lower_bound A))*>) + 1 <= i by XREAL_1:19;
then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . (i - (len <*(f . (lower_bound A))*>)) by A82, FINSEQ_1:23;
then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . (i - 1) by FINSEQ_1:39;
then A83: (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound (divset (D,i))) by A29, A40, A74;
(s1 ^ <*(f . (upper_bound A))*>) . i = s1 . i by A74, FINSEQ_1:def_7;
then (s1 ^ <*(f . (upper_bound A))*>) . i = f . (upper_bound (divset (D,i))) by A39, A74;
hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) by A4, A19, A44, A45, A73, A83; ::_thesis: verum
end;
end;
end;
hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) ; ::_thesis: verum
end;
end;
end;
hence p . i = ((s1 ^ <*(f . (upper_bound A))*>) /. i) - ((<*(f . (lower_bound A))*> ^ s2) /. i) ; ::_thesis: verum
end;
then Sum p = (Sum (s1 ^ <*(f . (upper_bound A))*>)) - (Sum (<*(f . (lower_bound A))*> ^ s2)) by INTEGRA1:22;
then Sum p = ((Sum s1) + (f . (upper_bound A))) - (Sum (<*(f . (lower_bound A))*> ^ s2)) by RVSUM_1:74;
then A84: Sum p = ((Sum s1) + (f . (upper_bound A))) - ((f . (lower_bound A)) + (Sum s2)) by RVSUM_1:76;
A85: dom s1 = Seg k1 by A39, FINSEQ_1:def_3;
A86: dom s1 = Seg k1 by A39, FINSEQ_1:def_3;
for i being Nat st i in dom s1 holds
s1 . i = s2 . i
proof
let i be Nat; ::_thesis: ( i in dom s1 implies s1 . i = s2 . i )
assume A87: i in dom s1 ; ::_thesis: s1 . i = s2 . i
then s1 . i = f . (upper_bound (divset (D,i))) by A39;
then s1 . i = f . (lower_bound (divset (D,(i + 1)))) by A20, A85, A87;
hence s1 . i = s2 . i by A86, A29, A40, A87; ::_thesis: verum
end;
then A88: s1 = s2 by A39, A29, FINSEQ_2:9;
A89: for k being Element of NAT
for r being Real st k in dom D & r in divset (D,k) holds
diff (f,r) in rng (((f `| X) || A) | (divset (D,k)))
proof
A90: dom ((f `| X) | A) = (dom (f `| X)) /\ A by RELAT_1:61
.= X /\ A by A2, FDIFF_1:def_7
.= A by A1, XBOOLE_1:28 ;
let k be Element of NAT ; ::_thesis: for r being Real st k in dom D & r in divset (D,k) holds
diff (f,r) in rng (((f `| X) || A) | (divset (D,k)))
let r be Real; ::_thesis: ( k in dom D & r in divset (D,k) implies diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) )
assume that
A91: k in dom D and
A92: r in divset (D,k) ; ::_thesis: diff (f,r) in rng (((f `| X) || A) | (divset (D,k)))
A93: divset (D,k) c= A by A91, INTEGRA1:8;
then divset (D,k) c= X by A1, XBOOLE_1:1;
then (f `| X) . r = diff (f,r) by A2, A92, FDIFF_1:def_7;
then A94: diff (f,r) = ((f `| X) || A) . r by A92, A93, A90, FUNCT_1:47;
A95: dom (((f `| X) || A) | (divset (D,k))) = A /\ (divset (D,k)) by A90, RELAT_1:61
.= divset (D,k) by A91, INTEGRA1:8, XBOOLE_1:28 ;
then (((f `| X) || A) | (divset (D,k))) . r in rng (((f `| X) || A) | (divset (D,k))) by A92, FUNCT_1:def_3;
hence diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A92, A94, A95, FUNCT_1:47; ::_thesis: verum
end;
A96: for k being Element of NAT st k in dom D holds
(f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k
proof
let k be Element of NAT ; ::_thesis: ( k in dom D implies (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k )
A97: vol (divset (D,k)) >= 0 by INTEGRA1:9;
assume A98: k in dom D ; ::_thesis: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k
then consider r being Real such that
A99: r in divset (D,k) and
A100: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) by A6;
A101: rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A30, A98;
diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A89, A98, A99;
then diff (f,r) <= upper_bound (rng (((f `| X) || A) | (divset (D,k)))) by A101, SEQ_4:def_1;
then (diff (f,r)) * (vol (divset (D,k))) <= (upper_bound (rng (((f `| X) || A) | (divset (D,k))))) * (vol (divset (D,k))) by A97, XREAL_1:64;
hence (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k by A98, A100, INTEGRA1:def_6; ::_thesis: verum
end;
A102: (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D)
proof
len (upper_volume (((f `| X) || A),D)) = len D by INTEGRA1:def_6;
then reconsider q = upper_volume (((f `| X) || A),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
A103: for k being Nat st k in Seg (len D) holds
p . k <= (upper_volume (((f `| X) || A),D)) . k
proof
let k be Nat; ::_thesis: ( k in Seg (len D) implies p . k <= (upper_volume (((f `| X) || A),D)) . k )
assume k in Seg (len D) ; ::_thesis: p . k <= (upper_volume (((f `| X) || A),D)) . k
then ( (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = p . k & k in dom D ) by A4, A19, FINSEQ_1:def_3;
hence p . k <= (upper_volume (((f `| X) || A),D)) . k by A96; ::_thesis: verum
end;
reconsider p = p as Element of (len D) -tuples_on REAL by A4, FINSEQ_2:92;
Sum p <= Sum q by A103, RVSUM_1:82;
hence (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) by A88, A84, INTEGRA1:def_8; ::_thesis: verum
end;
A104: for k being Element of NAT st k in dom D holds
(f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k
proof
let k be Element of NAT ; ::_thesis: ( k in dom D implies (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k )
assume A105: k in dom D ; ::_thesis: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k
then A106: ( vol (divset (D,k)) >= 0 & (lower_bound (rng (((f `| X) || A) | (divset (D,k))))) * (vol (divset (D,k))) = (lower_volume (((f `| X) || A),D)) . k ) by INTEGRA1:9, INTEGRA1:def_7;
A107: rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A30, A105;
consider r being Real such that
A108: r in divset (D,k) and
A109: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) by A6, A105;
diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A89, A105, A108;
then diff (f,r) >= lower_bound (rng (((f `| X) || A) | (divset (D,k)))) by A107, SEQ_4:def_2;
hence (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k by A109, A106, XREAL_1:64; ::_thesis: verum
end;
(f . (upper_bound A)) - (f . (lower_bound A)) >= lower_sum (((f `| X) || A),D)
proof
len (lower_volume (((f `| X) || A),D)) = len D by INTEGRA1:def_7;
then reconsider q = lower_volume (((f `| X) || A),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
A110: for k being Nat st k in Seg (len D) holds
p . k >= (lower_volume (((f `| X) || A),D)) . k
proof
let k be Nat; ::_thesis: ( k in Seg (len D) implies p . k >= (lower_volume (((f `| X) || A),D)) . k )
assume k in Seg (len D) ; ::_thesis: p . k >= (lower_volume (((f `| X) || A),D)) . k
then ( (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = p . k & k in dom D ) by A4, A19, FINSEQ_1:def_3;
hence p . k >= (lower_volume (((f `| X) || A),D)) . k by A104; ::_thesis: verum
end;
reconsider p = p as Element of (len D) -tuples_on REAL by A4, FINSEQ_2:92;
Sum q <= Sum p by A110, RVSUM_1:82;
hence (f . (upper_bound A)) - (f . (lower_bound A)) >= lower_sum (((f `| X) || A),D) by A88, A84, INTEGRA1:def_9; ::_thesis: verum
end;
hence ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) ) by A102; ::_thesis: verum
end;
theorem Th13: :: INTEGRA5:13
for A being non empty closed_interval Subset of REAL
for X being set
for f being PartFunc of REAL,REAL st A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded holds
integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for X being set
for f being PartFunc of REAL,REAL st A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded holds
integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A))
let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded holds
integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A))
let f be PartFunc of REAL,REAL; ::_thesis: ( A c= X & f is_differentiable_on X & f `| X is_integrable_on A & (f `| X) | A is bounded implies integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A)) )
assume that
A1: ( A c= X & f is_differentiable_on X ) and
A2: f `| X is_integrable_on A and
A3: (f `| X) | A is bounded ; ::_thesis: integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A))
(f `| X) || A is integrable by A2, Def1;
then A4: upper_integral ((f `| X) || A) = lower_integral ((f `| X) || A) by INTEGRA1:def_16;
A5: for r being real number st r in rng (upper_sum_set ((f `| X) || A)) holds
(f . (upper_bound A)) - (f . (lower_bound A)) <= r
proof
let r be real number ; ::_thesis: ( r in rng (upper_sum_set ((f `| X) || A)) implies (f . (upper_bound A)) - (f . (lower_bound A)) <= r )
assume r in rng (upper_sum_set ((f `| X) || A)) ; ::_thesis: (f . (upper_bound A)) - (f . (lower_bound A)) <= r
then consider D being Element of divs A such that
A6: ( D in dom (upper_sum_set ((f `| X) || A)) & r = (upper_sum_set ((f `| X) || A)) . D ) by PARTFUN1:3;
reconsider D = D as Division of A by INTEGRA1:def_3;
r = upper_sum (((f `| X) || A),D) by A6, INTEGRA1:def_10;
hence (f . (upper_bound A)) - (f . (lower_bound A)) <= r by A1, A3, Th12; ::_thesis: verum
end;
(f . (upper_bound A)) - (f . (lower_bound A)) <= lower_bound (rng (upper_sum_set ((f `| X) || A))) by A5, SEQ_4:43;
then A7: upper_integral ((f `| X) || A) >= (f . (upper_bound A)) - (f . (lower_bound A)) by INTEGRA1:def_14;
A8: for r being real number st r in rng (lower_sum_set ((f `| X) || A)) holds
r <= (f . (upper_bound A)) - (f . (lower_bound A))
proof
let r be real number ; ::_thesis: ( r in rng (lower_sum_set ((f `| X) || A)) implies r <= (f . (upper_bound A)) - (f . (lower_bound A)) )
assume r in rng (lower_sum_set ((f `| X) || A)) ; ::_thesis: r <= (f . (upper_bound A)) - (f . (lower_bound A))
then consider D being Element of divs A such that
A9: ( D in dom (lower_sum_set ((f `| X) || A)) & r = (lower_sum_set ((f `| X) || A)) . D ) by PARTFUN1:3;
reconsider D = D as Division of A by INTEGRA1:def_3;
r = lower_sum (((f `| X) || A),D) by A9, INTEGRA1:def_11;
hence r <= (f . (upper_bound A)) - (f . (lower_bound A)) by A1, A3, Th12; ::_thesis: verum
end;
upper_bound (rng (lower_sum_set ((f `| X) || A))) <= (f . (upper_bound A)) - (f . (lower_bound A)) by A8, SEQ_4:45;
then upper_integral ((f `| X) || A) <= (f . (upper_bound A)) - (f . (lower_bound A)) by A4, INTEGRA1:def_15;
then upper_integral ((f `| X) || A) = (f . (upper_bound A)) - (f . (lower_bound A)) by A7, XXREAL_0:1;
hence integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A)) by INTEGRA1:def_17; ::_thesis: verum
end;
theorem Th14: :: INTEGRA5:14
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds
rng (f | A) is real-bounded
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds
rng (f | A) is real-bounded
let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is non-decreasing & A c= dom f implies rng (f | A) is real-bounded )
assume that
A1: f | A is non-decreasing and
A2: A c= dom f ; ::_thesis: rng (f | A) is real-bounded
A3: dom (f | A) = (dom f) /\ A by RELAT_1:61
.= A by A2, XBOOLE_1:28 ;
f . (lower_bound A) is LowerBound of rng (f | A)
proof
lower_bound A <= upper_bound A by SEQ_4:11;
then lower_bound A in dom (f | A) by A3, INTEGRA2:1;
then A4: lower_bound A in (dom f) /\ A by RELAT_1:61;
let y be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not y in rng (f | A) or f . (lower_bound A) <= y )
assume y in rng (f | A) ; ::_thesis: f . (lower_bound A) <= y
then consider x being Real such that
A5: x in dom (f | A) and
A6: y = (f | A) . x by PARTFUN1:3;
A7: x in (dom f) /\ A by A5, RELAT_1:61;
( y = f . x & x >= lower_bound A ) by A5, A6, FUNCT_1:47, INTEGRA2:1;
hence f . (lower_bound A) <= y by A1, A7, A4, RFUNCT_2:24; ::_thesis: verum
end;
then A8: rng (f | A) is bounded_below by XXREAL_2:def_9;
f . (upper_bound A) is UpperBound of rng (f | A)
proof
lower_bound A <= upper_bound A by SEQ_4:11;
then upper_bound A in dom (f | A) by A3, INTEGRA2:1;
then A9: upper_bound A in (dom f) /\ A by RELAT_1:61;
let y be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not y in rng (f | A) or y <= f . (upper_bound A) )
assume y in rng (f | A) ; ::_thesis: y <= f . (upper_bound A)
then consider x being Real such that
A10: x in dom (f | A) and
A11: y = (f | A) . x by PARTFUN1:3;
A12: x in (dom f) /\ A by A10, RELAT_1:61;
( y = f . x & x <= upper_bound A ) by A10, A11, FUNCT_1:47, INTEGRA2:1;
hence y <= f . (upper_bound A) by A1, A12, A9, RFUNCT_2:24; ::_thesis: verum
end;
then rng (f | A) is bounded_above by XXREAL_2:def_10;
hence rng (f | A) is real-bounded by A8; ::_thesis: verum
end;
theorem Th15: :: INTEGRA5:15
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds
( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) )
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds
( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is non-decreasing & A c= dom f implies ( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) ) )
assume that
A1: f | A is non-decreasing and
A2: A c= dom f ; ::_thesis: ( lower_bound (rng (f | A)) = f . (lower_bound A) & upper_bound (rng (f | A)) = f . (upper_bound A) )
A3: dom (f | A) = (dom f) /\ A by RELAT_1:61
.= A by A2, XBOOLE_1:28 ;
then A4: rng (f | A) <> {} by RELAT_1:42;
A5: lower_bound A <= upper_bound A by SEQ_4:11;
then A6: upper_bound A in dom (f | A) by A3, INTEGRA2:1;
then A7: upper_bound A in (dom f) /\ A by RELAT_1:61;
A8: for x being real number st x in rng (f | A) holds
x <= f . (upper_bound A)
proof
let y be real number ; ::_thesis: ( y in rng (f | A) implies y <= f . (upper_bound A) )
assume y in rng (f | A) ; ::_thesis: y <= f . (upper_bound A)
then consider x being Real such that
A9: x in dom (f | A) and
A10: y = (f | A) . x by PARTFUN1:3;
( x in (dom f) /\ A & upper_bound A >= x ) by A9, INTEGRA2:1, RELAT_1:61;
then f . (upper_bound A) >= f . x by A1, A7, RFUNCT_2:24;
hence y <= f . (upper_bound A) by A9, A10, FUNCT_1:47; ::_thesis: verum
end;
A11: lower_bound A in dom (f | A) by A3, A5, INTEGRA2:1;
then A12: lower_bound A in (dom f) /\ A by RELAT_1:61;
A13: for y being real number st y in rng (f | A) holds
y >= f . (lower_bound A)
proof
let y be real number ; ::_thesis: ( y in rng (f | A) implies y >= f . (lower_bound A) )
assume y in rng (f | A) ; ::_thesis: y >= f . (lower_bound A)
then consider x being Real such that
A14: x in dom (f | A) and
A15: y = (f | A) . x by PARTFUN1:3;
( x in (dom f) /\ A & lower_bound A <= x ) by A14, INTEGRA2:1, RELAT_1:61;
then f . (lower_bound A) <= f . x by A1, A12, RFUNCT_2:24;
hence y >= f . (lower_bound A) by A14, A15, FUNCT_1:47; ::_thesis: verum
end;
for a being real number st ( for x being real number st x in rng (f | A) holds
x >= a ) holds
f . (lower_bound A) >= a
proof
let a be real number ; ::_thesis: ( ( for x being real number st x in rng (f | A) holds
x >= a ) implies f . (lower_bound A) >= a )
assume A16: for x being real number st x in rng (f | A) holds
x >= a ; ::_thesis: f . (lower_bound A) >= a
( f . (lower_bound A) = (f | A) . (lower_bound A) & (f | A) . (lower_bound A) in rng (f | A) ) by A11, FUNCT_1:47, FUNCT_1:def_3;
hence f . (lower_bound A) >= a by A16; ::_thesis: verum
end;
hence lower_bound (rng (f | A)) = f . (lower_bound A) by A4, A13, SEQ_4:44; ::_thesis: upper_bound (rng (f | A)) = f . (upper_bound A)
for a being real number st ( for x being real number st x in rng (f | A) holds
x <= a ) holds
f . (upper_bound A) <= a
proof
let a be real number ; ::_thesis: ( ( for x being real number st x in rng (f | A) holds
x <= a ) implies f . (upper_bound A) <= a )
assume A17: for x being real number st x in rng (f | A) holds
x <= a ; ::_thesis: f . (upper_bound A) <= a
( f . (upper_bound A) = (f | A) . (upper_bound A) & (f | A) . (upper_bound A) in rng (f | A) ) by A6, FUNCT_1:47, FUNCT_1:def_3;
hence f . (upper_bound A) <= a by A17; ::_thesis: verum
end;
hence upper_bound (rng (f | A)) = f . (upper_bound A) by A4, A8, SEQ_4:46; ::_thesis: verum
end;
Lm1: for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds
f is_integrable_on A
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is non-decreasing & A c= dom f holds
f is_integrable_on A
let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is non-decreasing & A c= dom f implies f is_integrable_on A )
assume that
A1: f | A is non-decreasing and
A2: A c= dom f ; ::_thesis: f is_integrable_on A
A3: for D being Division of A
for k being Element of NAT st k in dom D holds
( 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) & ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) )
proof
let D be Division of A; ::_thesis: for k being Element of NAT st k in dom D holds
( 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) & ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) )
let k be Element of NAT ; ::_thesis: ( k in dom D implies ( 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) & ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) ) )
assume A4: k in dom D ; ::_thesis: ( 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) & ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) )
then A5: ( (upper_volume ((f || A),D)) . k = (upper_bound (rng ((f || A) | (divset (D,k))))) * (vol (divset (D,k))) & (lower_volume ((f || A),D)) . k = (lower_bound (rng ((f || A) | (divset (D,k))))) * (vol (divset (D,k))) ) by INTEGRA1:def_6, INTEGRA1:def_7;
k in Seg (len D) by A4, FINSEQ_1:def_3;
then k in Seg (len (upper_volume ((chi (A,A)),D))) by INTEGRA1:def_6;
then A6: k in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def_3;
vol (divset (D,k)) = (upper_volume ((chi (A,A)),D)) . k by A4, INTEGRA1:20;
then vol (divset (D,k)) in rng (upper_volume ((chi (A,A)),D)) by A6, FUNCT_1:def_3;
then vol (divset (D,k)) <= max (rng (upper_volume ((chi (A,A)),D))) by XXREAL_2:def_8;
then A7: vol (divset (D,k)) <= delta D by INTEGRA3:def_1;
A8: divset (D,k) c= A by A4, INTEGRA1:8;
then A9: divset (D,k) c= dom f by A2, XBOOLE_1:1;
f | (divset (D,k)) is non-decreasing by A1, A4, INTEGRA1:8, RFUNCT_2:30;
then A10: ( lower_bound (rng (f | (divset (D,k)))) = f . (lower_bound (divset (D,k))) & upper_bound (rng (f | (divset (D,k)))) = f . (upper_bound (divset (D,k))) ) by A9, Th15;
dom (f | (divset (D,k))) = (dom f) /\ (divset (D,k)) by RELAT_1:61
.= divset (D,k) by A2, A8, XBOOLE_1:1, XBOOLE_1:28 ;
then A11: rng (f | (divset (D,k))) <> {} by RELAT_1:42;
A12: rng (f | (divset (D,k))) = rng ((f || A) | (divset (D,k))) by A8, FUNCT_1:51;
rng (f | A) is real-bounded by A1, A2, Th14;
then rng (f | (divset (D,k))) is real-bounded by A12, RELAT_1:70, XXREAL_2:45;
then A13: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= 0 by A10, A11, SEQ_4:11, XREAL_1:48;
vol (divset (D,k)) >= 0 by INTEGRA1:9;
then 0 * (vol (divset (D,k))) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (vol (divset (D,k))) by A13;
hence 0 <= ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) by A10, A5, A12; ::_thesis: ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D)
((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) = ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (vol (divset (D,k))) by A10, A5, A12;
hence ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) by A13, A7, XREAL_1:64; ::_thesis: verum
end;
A14: for D being Division of A holds
( (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) & (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 )
proof
let D be Division of A; ::_thesis: ( (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) & (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 )
deffunc H1( Nat) -> Element of REAL = f . (upper_bound (divset (D,$1)));
consider F1 being FinSequence of REAL such that
A15: ( len F1 = len D & ( for i being Nat st i in dom F1 holds
F1 . i = H1(i) ) ) from FINSEQ_2:sch_1();
(len D) - 1 in NAT
proof
ex j being Nat st len D = 1 + j by NAT_1:10, NAT_1:14;
hence (len D) - 1 in NAT by ORDINAL1:def_12; ::_thesis: verum
end;
then consider k1 being Element of NAT such that
A16: k1 = (len D) - 1 ;
deffunc H2( Nat) -> Element of REAL = f . (lower_bound (divset (D,$1)));
consider F2 being FinSequence of REAL such that
A17: ( len F2 = len D & ( for i being Nat st i in dom F2 holds
F2 . i = H2(i) ) ) from FINSEQ_2:sch_1();
deffunc H3( Nat) -> Element of REAL = f . (upper_bound (divset (D,$1)));
A18: dom F2 = Seg (len D) by A17, FINSEQ_1:def_3;
consider F being FinSequence of REAL such that
A19: ( len F = k1 & ( for i being Nat st i in dom F holds
F . i = H3(i) ) ) from FINSEQ_2:sch_1();
A20: dom F = Seg k1 by A19, FINSEQ_1:def_3;
A21: for i being Nat st 1 <= i & i <= len F2 holds
F2 . i = (<*(f . (lower_bound A))*> ^ F) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len F2 implies F2 . i = (<*(f . (lower_bound A))*> ^ F) . i )
assume that
A22: 1 <= i and
A23: i <= len F2 ; ::_thesis: F2 . i = (<*(f . (lower_bound A))*> ^ F) . i
percases ( i = 1 or i <> 1 ) ;
supposeA24: i = 1 ; ::_thesis: F2 . i = (<*(f . (lower_bound A))*> ^ F) . i
A25: i in Seg (len D) by A17, A22, A23, FINSEQ_1:1;
then A26: i in dom D by FINSEQ_1:def_3;
F2 . i = f . (lower_bound (divset (D,i))) by A17, A18, A25
.= f . (lower_bound A) by A24, A26, INTEGRA1:def_4 ;
hence F2 . i = (<*(f . (lower_bound A))*> ^ F) . i by A24, FINSEQ_1:41; ::_thesis: verum
end;
supposeA27: i <> 1 ; ::_thesis: F2 . i = (<*(f . (lower_bound A))*> ^ F) . i
then A28: i > 1 by A22, XXREAL_0:1;
then 1 + 1 <= i by NAT_1:13;
then A29: (len <*(f . (lower_bound A))*>) + 1 <= i by FINSEQ_1:39;
A30: i in Seg (len D) by A17, A22, A23, FINSEQ_1:1;
then A31: i in dom D by FINSEQ_1:def_3;
then reconsider k2 = i - 1 as Element of NAT by A27, INTEGRA1:7;
1 + 1 <= k2 + 1 by A28, NAT_1:13;
then A32: 1 <= k2 by XREAL_1:19;
k2 + 1 <= len F2 by A23;
then A33: k2 <= (len D) - 1 by A17, XREAL_1:19;
then A34: k2 in Seg k1 by A16, A32, FINSEQ_1:1;
A35: upper_bound (divset (D,k2)) = D . (i - 1)
proof
len D <= (len D) + 1 by NAT_1:13;
then (len D) - 1 <= len D by XREAL_1:20;
then k2 <= len D by A33, XXREAL_0:2;
then k2 in Seg (len D) by A32, FINSEQ_1:1;
then A36: k2 in dom D by FINSEQ_1:def_3;
percases ( k2 = 1 or k2 <> 1 ) ;
suppose k2 = 1 ; ::_thesis: upper_bound (divset (D,k2)) = D . (i - 1)
hence upper_bound (divset (D,k2)) = D . (i - 1) by A36, INTEGRA1:def_4; ::_thesis: verum
end;
suppose k2 <> 1 ; ::_thesis: upper_bound (divset (D,k2)) = D . (i - 1)
hence upper_bound (divset (D,k2)) = D . (i - 1) by A36, INTEGRA1:def_4; ::_thesis: verum
end;
end;
end;
len F2 = 1 + ((len D) - 1) by A17
.= (len <*(f . (lower_bound A))*>) + (len F) by A16, A19, FINSEQ_1:39 ;
then A37: (<*(f . (lower_bound A))*> ^ F) . i = F . (i - (len <*(f . (lower_bound A))*>)) by A23, A29, FINSEQ_1:23
.= F . (i - 1) by FINSEQ_1:39 ;
F2 . i = f . (lower_bound (divset (D,i))) by A17, A18, A30
.= f . (D . (i - 1)) by A27, A31, INTEGRA1:def_4 ;
hence F2 . i = (<*(f . (lower_bound A))*> ^ F) . i by A19, A20, A37, A34, A35; ::_thesis: verum
end;
end;
end;
len (<*(f . (lower_bound A))*> ^ F) = (len <*(f . (lower_bound A))*>) + (len F) by FINSEQ_1:22
.= 1 + ((len D) - 1) by A16, A19, FINSEQ_1:39
.= len D ;
then A38: F2 = <*(f . (lower_bound A))*> ^ F by A17, A21, FINSEQ_1:14;
( len (upper_volume ((f || A),D)) = len D & len (lower_volume ((f || A),D)) = len D ) by INTEGRA1:def_6, INTEGRA1:def_7;
then A39: Sum ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) = (Sum (upper_volume ((f || A),D))) - (Sum (lower_volume ((f || A),D))) by Th2
.= (upper_sum ((f || A),D)) - (Sum (lower_volume ((f || A),D))) by INTEGRA1:def_8
.= (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) by INTEGRA1:def_9 ;
A40: dom F1 = Seg (len D) by A15, FINSEQ_1:def_3;
A41: for i being Nat st 1 <= i & i <= len F1 holds
F1 . i = (F ^ <*(f . (upper_bound A))*>) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len F1 implies F1 . i = (F ^ <*(f . (upper_bound A))*>) . i )
assume that
A42: 1 <= i and
A43: i <= len F1 ; ::_thesis: F1 . i = (F ^ <*(f . (upper_bound A))*>) . i
now__::_thesis:_F1_._i_=_(F_^_<*(f_._(upper_bound_A))*>)_._i
percases ( i <= len F or i > len F ) ;
suppose i <= len F ; ::_thesis: F1 . i = (F ^ <*(f . (upper_bound A))*>) . i
then i in Seg (len F) by A42, FINSEQ_1:1;
then A44: ( F . i = f . (upper_bound (divset (D,i))) & i in dom F ) by A19, A20;
i in Seg (len F1) by A42, A43, FINSEQ_1:1;
then F1 . i = f . (upper_bound (divset (D,i))) by A15, A40;
hence F1 . i = (F ^ <*(f . (upper_bound A))*>) . i by A44, FINSEQ_1:def_7; ::_thesis: verum
end;
suppose i > len F ; ::_thesis: F1 . i = (F ^ <*(f . (upper_bound A))*>) . i
then A45: i >= (len F) + 1 by NAT_1:13;
then A46: i = (len F) + 1 by A15, A16, A19, A43, XXREAL_0:1;
A47: i in Seg (len F1) by A42, A43, FINSEQ_1:1;
then A48: i in dom D by A15, FINSEQ_1:def_3;
A49: upper_bound (divset (D,i)) = D . i
proof
now__::_thesis:_upper_bound_(divset_(D,i))_=_D_._i
percases ( i = 1 or i <> 1 ) ;
suppose i = 1 ; ::_thesis: upper_bound (divset (D,i)) = D . i
hence upper_bound (divset (D,i)) = D . i by A48, INTEGRA1:def_4; ::_thesis: verum
end;
suppose i <> 1 ; ::_thesis: upper_bound (divset (D,i)) = D . i
hence upper_bound (divset (D,i)) = D . i by A48, INTEGRA1:def_4; ::_thesis: verum
end;
end;
end;
hence upper_bound (divset (D,i)) = D . i ; ::_thesis: verum
end;
F1 . i = f . (upper_bound (divset (D,i))) by A15, A40, A47;
then F1 . i = f . (D . (len D)) by A15, A16, A19, A43, A45, A49, XXREAL_0:1
.= f . (upper_bound A) by INTEGRA1:def_2 ;
hence F1 . i = (F ^ <*(f . (upper_bound A))*>) . i by A46, FINSEQ_1:42; ::_thesis: verum
end;
end;
end;
hence F1 . i = (F ^ <*(f . (upper_bound A))*>) . i ; ::_thesis: verum
end;
( len (upper_volume ((f || A),D)) = len D & len (lower_volume ((f || A),D)) = len D ) by INTEGRA1:def_6, INTEGRA1:def_7;
then A50: len ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) = len D by Th2;
A51: len (F1 - F2) = len D by A15, A17, Th2;
A52: for k being Element of NAT st k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) holds
((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((delta D) * (F1 - F2)) . k
proof
let k be Element of NAT ; ::_thesis: ( k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) implies ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((delta D) * (F1 - F2)) . k )
assume A53: k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) ; ::_thesis: ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((delta D) * (F1 - F2)) . k
then k in Seg (len (F1 - F2)) by A50, A51, FINSEQ_1:def_3;
then A54: k in dom (F1 - F2) by FINSEQ_1:def_3;
A55: k in Seg (len D) by A50, A53, FINSEQ_1:def_3;
then k in dom D by FINSEQ_1:def_3;
then ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) by A3;
then A56: ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) * (delta D) by A53, VALUED_1:13;
( F1 . k = f . (upper_bound (divset (D,k))) & F2 . k = f . (lower_bound (divset (D,k))) ) by A15, A40, A17, A18, A55;
then ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= (delta D) * ((F1 - F2) . k) by A56, A54, VALUED_1:13;
hence ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k <= ((delta D) * (F1 - F2)) . k by RVSUM_1:44; ::_thesis: verum
end;
(delta D) * (F1 - F2) = ((delta D) multreal) * (F1 - F2) by RVSUM_1:def_7;
then len ((delta D) * (F1 - F2)) = len (F1 - F2) by FINSEQ_2:33;
then len ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) = len ((delta D) * (F1 - F2)) by A15, A17, A50, Th2;
then A57: Sum ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) <= Sum ((delta D) * (F1 - F2)) by A52, Th3;
len (F ^ <*(f . (upper_bound A))*>) = (len F) + (len <*(f . (upper_bound A))*>) by FINSEQ_1:22
.= ((len D) - 1) + 1 by A16, A19, FINSEQ_1:39
.= len D ;
then F1 = F ^ <*(f . (upper_bound A))*> by A15, A41, FINSEQ_1:14;
then Sum (F1 - F2) = (f . (upper_bound A)) - (f . (lower_bound A)) by A38, Th1;
hence (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) by A39, A57, RVSUM_1:87; ::_thesis: (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0
for k being Nat st k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) holds
0 <= ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k
proof
let k be Nat; ::_thesis: ( k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) implies 0 <= ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k )
set r = ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k;
A58: ( len (upper_volume ((f || A),D)) = len D & len (lower_volume ((f || A),D)) = len D ) by INTEGRA1:def_6, INTEGRA1:def_7;
assume A59: k in dom ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) ; ::_thesis: 0 <= ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k
then k in Seg (len ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D)))) by FINSEQ_1:def_3;
then k in Seg (len D) by A58, Th2;
then A60: k in dom D by FINSEQ_1:def_3;
((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k = ((upper_volume ((f || A),D)) . k) - ((lower_volume ((f || A),D)) . k) by A59, VALUED_1:13;
hence 0 <= ((upper_volume ((f || A),D)) - (lower_volume ((f || A),D))) . k by A3, A60; ::_thesis: verum
end;
hence (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 by A39, RVSUM_1:84; ::_thesis: verum
end;
A61: ( f || A is total & (f || A) | A is bounded )
proof
consider x being Real such that
A62: x in A by SUBSET_1:4;
A63: dom (f || A) = (dom f) /\ A by RELAT_1:61
.= A by A2, XBOOLE_1:28 ;
hence f || A is total by PARTFUN1:def_2; ::_thesis: (f || A) | A is bounded
( lower_bound A <= x & x <= upper_bound A ) by A62, INTEGRA2:1;
then A64: lower_bound A <= upper_bound A by XXREAL_0:2;
for x being set st x in A /\ (dom (f || A)) holds
(f || A) . x >= (f || A) . (lower_bound A)
proof
lower_bound A in A by A64, INTEGRA2:1;
then A65: ( lower_bound A in A /\ (dom f) & f . (lower_bound A) = (f | A) . (lower_bound A) ) by A2, A63, FUNCT_1:47, XBOOLE_1:28;
let x be set ; ::_thesis: ( x in A /\ (dom (f || A)) implies (f || A) . x >= (f || A) . (lower_bound A) )
assume A66: x in A /\ (dom (f || A)) ; ::_thesis: (f || A) . x >= (f || A) . (lower_bound A)
then x in A ;
then A67: x in A /\ (dom f) by A2, XBOOLE_1:28;
reconsider x = x as Element of A by A66;
( x >= lower_bound A & f . x = (f | A) . x ) by A63, FUNCT_1:47, INTEGRA2:1;
hence (f || A) . x >= (f || A) . (lower_bound A) by A1, A67, A65, RFUNCT_2:24; ::_thesis: verum
end;
then A68: (f || A) | A is bounded_below by RFUNCT_1:71;
for x being set st x in A /\ (dom (f || A)) holds
(f || A) . x <= (f || A) . (upper_bound A)
proof
upper_bound A in A by A64, INTEGRA2:1;
then A69: ( upper_bound A in A /\ (dom f) & f . (upper_bound A) = (f | A) . (upper_bound A) ) by A2, A63, FUNCT_1:47, XBOOLE_1:28;
let x be set ; ::_thesis: ( x in A /\ (dom (f || A)) implies (f || A) . x <= (f || A) . (upper_bound A) )
assume A70: x in A /\ (dom (f || A)) ; ::_thesis: (f || A) . x <= (f || A) . (upper_bound A)
then x in A ;
then A71: x in A /\ (dom f) by A2, XBOOLE_1:28;
reconsider x = x as Element of A by A70;
( x <= upper_bound A & f . x = (f | A) . x ) by A63, FUNCT_1:47, INTEGRA2:1;
hence (f || A) . x <= (f || A) . (upper_bound A) by A1, A71, A69, RFUNCT_2:24; ::_thesis: verum
end;
then (f || A) | A is bounded_above by RFUNCT_1:70;
hence (f || A) | A is bounded by A68; ::_thesis: verum
end;
for T being DivSequence of A st delta T is convergent & lim (delta T) = 0 holds
(lim (upper_sum ((f || A),T))) - (lim (lower_sum ((f || A),T))) = 0
proof
let T be DivSequence of A; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies (lim (upper_sum ((f || A),T))) - (lim (lower_sum ((f || A),T))) = 0 )
assume A72: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: (lim (upper_sum ((f || A),T))) - (lim (lower_sum ((f || A),T))) = 0
A73: for r being real number st 0 < r holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r
proof
consider x being Real such that
A74: x in A by SUBSET_1:4;
A75: A = A /\ (dom f) by A2, XBOOLE_1:28;
let r be real number ; ::_thesis: ( 0 < r implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r )
assume A76: 0 < r ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r
( lower_bound A <= x & x <= upper_bound A ) by A74, INTEGRA2:1;
then A77: lower_bound A <= upper_bound A by XXREAL_0:2;
then ( lower_bound A in A & upper_bound A in A ) by INTEGRA2:1;
then A78: f . (lower_bound A) <= f . (upper_bound A) by A1, A77, A75, RFUNCT_2:24;
now__::_thesis:_ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_((((upper_sum_((f_||_A),T))_-_(lower_sum_((f_||_A),T)))_._m)_-_0)_<_r
percases ( f . (lower_bound A) = f . (upper_bound A) or f . (lower_bound A) < f . (upper_bound A) ) by A78, XXREAL_0:1;
supposeA79: f . (lower_bound A) = f . (upper_bound A) ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r
for m being Element of NAT st 0 <= m holds
abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r
proof
let m be Element of NAT ; ::_thesis: ( 0 <= m implies abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r )
assume 0 <= m ; ::_thesis: abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r
reconsider D1 = T . m as Division of A ;
A80: ((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m = ((upper_sum ((f || A),T)) . m) + ((- (lower_sum ((f || A),T))) . m) by SEQ_1:7
.= ((upper_sum ((f || A),T)) . m) + (- ((lower_sum ((f || A),T)) . m)) by SEQ_1:10
.= (upper_sum ((f || A),D1)) + (- ((lower_sum ((f || A),T)) . m)) by INTEGRA2:def_2
.= (upper_sum ((f || A),D1)) + (- (lower_sum ((f || A),D1))) by INTEGRA2:def_3 ;
( (upper_sum ((f || A),D1)) - (lower_sum ((f || A),D1)) <= (delta D1) * ((f . (upper_bound A)) - (f . (lower_bound A))) & (upper_sum ((f || A),D1)) - (lower_sum ((f || A),D1)) >= 0 ) by A14;
hence abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r by A76, A79, A80, ABSVALUE:def_1; ::_thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r ; ::_thesis: verum
end;
suppose f . (lower_bound A) < f . (upper_bound A) ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r
then A81: (f . (upper_bound A)) - (f . (lower_bound A)) > 0 by XREAL_1:50;
then r / ((f . (upper_bound A)) - (f . (lower_bound A))) > 0 by A76, XREAL_1:139;
then consider n being Element of NAT such that
A82: for m being Element of NAT st n <= m holds
abs (((delta T) . m) - 0) < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A72, SEQ_2:def_7;
A83: for m being Element of NAT st n <= m holds
(delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A)))
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies (delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A))) )
assume n <= m ; ::_thesis: (delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A)))
then A84: abs (((delta T) . m) - 0) < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A82;
(delta T) . m <= abs ((delta T) . m) by ABSVALUE:4;
hence (delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A84, XXREAL_0:2; ::_thesis: verum
end;
for m being Element of NAT st n <= m holds
abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r )
reconsider D = T . m as Division of A ;
A85: abs ((upper_sum ((f || A),D)) - (lower_sum ((f || A),D))) = abs ((((upper_sum ((f || A),T)) . m) - (lower_sum ((f || A),D))) - 0) by INTEGRA2:def_2
.= abs ((((upper_sum ((f || A),T)) . m) - ((lower_sum ((f || A),T)) . m)) - 0) by INTEGRA2:def_3
.= abs ((((upper_sum ((f || A),T)) . m) + (- ((lower_sum ((f || A),T)) . m))) - 0)
.= abs ((((upper_sum ((f || A),T)) . m) + ((- (lower_sum ((f || A),T))) . m)) - 0) by SEQ_1:10
.= abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) by SEQ_1:7 ;
assume n <= m ; ::_thesis: abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r
then (delta T) . m < r / ((f . (upper_bound A)) - (f . (lower_bound A))) by A83;
then ((delta T) . m) * ((f . (upper_bound A)) - (f . (lower_bound A))) < r by A81, XREAL_1:79;
then A86: (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) < r by INTEGRA3:def_2;
(upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) <= (delta D) * ((f . (upper_bound A)) - (f . (lower_bound A))) by A14;
then A87: (upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) < r by A86, XXREAL_0:2;
(upper_sum ((f || A),D)) - (lower_sum ((f || A),D)) >= 0 by A14;
hence abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r by A87, A85, ABSVALUE:def_1; ::_thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r ; ::_thesis: verum
end;
end;
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) . m) - 0) < r ; ::_thesis: verum
end;
A88: ( upper_sum ((f || A),T) is convergent & lower_sum ((f || A),T) is convergent ) by A61, A72, INTEGRA4:8, INTEGRA4:9;
then (upper_sum ((f || A),T)) - (lower_sum ((f || A),T)) is convergent ;
then lim ((upper_sum ((f || A),T)) - (lower_sum ((f || A),T))) = 0 by A73, SEQ_2:def_7;
hence (lim (upper_sum ((f || A),T))) - (lim (lower_sum ((f || A),T))) = 0 by A88, SEQ_2:12; ::_thesis: verum
end;
then f || A is integrable by A61, INTEGRA4:12;
hence f is_integrable_on A by Def1; ::_thesis: verum
end;
theorem :: INTEGRA5:16
for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,REAL st f | A is monotone & A c= dom f holds
f is_integrable_on A
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | A is monotone & A c= dom f holds
f is_integrable_on A
let f be PartFunc of REAL,REAL; ::_thesis: ( f | A is monotone & A c= dom f implies f is_integrable_on A )
assume that
A1: f | A is monotone and
A2: A c= dom f ; ::_thesis: f is_integrable_on A
percases ( f | A is non-decreasing or f | A is non-increasing ) by A1, RFUNCT_2:def_5;
suppose f | A is non-decreasing ; ::_thesis: f is_integrable_on A
hence f is_integrable_on A by A2, Lm1; ::_thesis: verum
end;
suppose f | A is non-increasing ; ::_thesis: f is_integrable_on A
then A3: ((- 1) (#) f) | A is non-decreasing by RFUNCT_2:35;
A4: ( (- f) || A is total & ((- f) || A) | A is bounded )
proof
consider x being Real such that
A5: x in A by SUBSET_1:4;
A6: dom ((- f) || A) = (dom (- f)) /\ A by RELAT_1:61
.= (dom f) /\ A by VALUED_1:8
.= A by A2, XBOOLE_1:28 ;
hence (- f) || A is total by PARTFUN1:def_2; ::_thesis: ((- f) || A) | A is bounded
( lower_bound A <= x & x <= upper_bound A ) by A5, INTEGRA2:1;
then A7: lower_bound A <= upper_bound A by XXREAL_0:2;
for x being set st x in A /\ (dom ((- f) || A)) holds
((- f) || A) . x >= ((- f) || A) . (lower_bound A)
proof
let x be set ; ::_thesis: ( x in A /\ (dom ((- f) || A)) implies ((- f) || A) . x >= ((- f) || A) . (lower_bound A) )
assume x in A /\ (dom ((- f) || A)) ; ::_thesis: ((- f) || A) . x >= ((- f) || A) . (lower_bound A)
then reconsider x = x as Element of A ;
A8: ( x >= lower_bound A & (- f) . x = ((- f) | A) . x ) by A6, FUNCT_1:47, INTEGRA2:1;
lower_bound A in A by A7, INTEGRA2:1;
then A9: (- f) . (lower_bound A) = ((- f) | A) . (lower_bound A) by A6, FUNCT_1:47;
A10: A = A /\ (dom f) by A2, XBOOLE_1:28
.= A /\ (dom (- f)) by VALUED_1:8 ;
then lower_bound A in A /\ (dom (- f)) by A7, INTEGRA2:1;
hence ((- f) || A) . x >= ((- f) || A) . (lower_bound A) by A3, A10, A8, A9, RFUNCT_2:24; ::_thesis: verum
end;
then A11: ((- f) || A) | A is bounded_below by RFUNCT_1:71;
for x being set st x in A /\ (dom ((- f) || A)) holds
((- f) || A) . x <= ((- f) || A) . (upper_bound A)
proof
let x be set ; ::_thesis: ( x in A /\ (dom ((- f) || A)) implies ((- f) || A) . x <= ((- f) || A) . (upper_bound A) )
assume x in A /\ (dom ((- f) || A)) ; ::_thesis: ((- f) || A) . x <= ((- f) || A) . (upper_bound A)
then reconsider x = x as Element of A ;
A12: ( x <= upper_bound A & (- f) . x = ((- f) | A) . x ) by A6, FUNCT_1:47, INTEGRA2:1;
upper_bound A in A by A7, INTEGRA2:1;
then A13: (- f) . (upper_bound A) = ((- f) | A) . (upper_bound A) by A6, FUNCT_1:47;
A14: A = A /\ (dom f) by A2, XBOOLE_1:28
.= A /\ (dom (- f)) by VALUED_1:8 ;
then upper_bound A in A /\ (dom (- f)) by A7, INTEGRA2:1;
hence ((- f) || A) . x <= ((- f) || A) . (upper_bound A) by A3, A14, A12, A13, RFUNCT_2:24; ::_thesis: verum
end;
then ((- f) || A) | A is bounded_above by RFUNCT_1:70;
hence ((- f) || A) | A is bounded by A11; ::_thesis: verum
end;
dom f = dom (- f) by VALUED_1:8;
then - f is_integrable_on A by A2, A3, Lm1;
then (- f) || A is integrable by Def1;
then A15: (- 1) (#) ((- f) || A) is integrable by A4, INTEGRA2:31;
A16: dom ((- f) || A) = (dom (- f)) /\ A by RELAT_1:61
.= (dom f) /\ A by VALUED_1:8
.= A by A2, XBOOLE_1:28 ;
then A17: A = dom ((- 1) (#) ((- f) || A)) by VALUED_1:def_5;
A18: dom (f || A) = (dom f) /\ A by RELAT_1:61;
then A19: dom (f || A) = A by A2, XBOOLE_1:28;
A20: dom ((- 1) (#) ((- f) || A)) = A by A16, VALUED_1:def_5;
A21: for z being Element of A st z in A holds
((- 1) (#) ((- f) || A)) . z = (f || A) . z
proof
let z be Element of A; ::_thesis: ( z in A implies ((- 1) (#) ((- f) || A)) . z = (f || A) . z )
assume z in A ; ::_thesis: ((- 1) (#) ((- f) || A)) . z = (f || A) . z
((- f) || A) . z = (- f) . z by A16, FUNCT_1:47
.= - (f . z) by VALUED_1:8 ;
then ((- 1) (#) ((- f) || A)) . z = (- 1) * (- (f . z)) by A20, VALUED_1:def_5
.= f . z ;
hence ((- 1) (#) ((- f) || A)) . z = (f || A) . z by A19, FUNCT_1:47; ::_thesis: verum
end;
A = dom (f || A) by A2, A18, XBOOLE_1:28;
then (- 1) (#) ((- f) || A) = f || A by A21, A17, PARTFUN1:5;
hence f is_integrable_on A by A15, Def1; ::_thesis: verum
end;
end;
end;
theorem :: INTEGRA5:17
for f being PartFunc of REAL,REAL
for A, B being non empty closed_interval Subset of REAL st A c= dom f & f | A is continuous & B c= A holds
f is_integrable_on B
proof
let f be PartFunc of REAL,REAL; ::_thesis: for A, B being non empty closed_interval Subset of REAL st A c= dom f & f | A is continuous & B c= A holds
f is_integrable_on B
let A, B be non empty closed_interval Subset of REAL; ::_thesis: ( A c= dom f & f | A is continuous & B c= A implies f is_integrable_on B )
assume that
A1: A c= dom f and
A2: f | A is continuous and
A3: B c= A ; ::_thesis: f is_integrable_on B
f | B is continuous by A2, A3, FCONT_1:16;
hence f is_integrable_on B by A1, A3, Th11, XBOOLE_1:1; ::_thesis: verum
end;
theorem :: INTEGRA5:18
for f being PartFunc of REAL,REAL
for A, B, C being non empty closed_interval Subset of REAL
for X being set st A c= X & f is_differentiable_on X & (f `| X) | A is continuous & lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A holds
( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) )
proof
let f be PartFunc of REAL,REAL; ::_thesis: for A, B, C being non empty closed_interval Subset of REAL
for X being set st A c= X & f is_differentiable_on X & (f `| X) | A is continuous & lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A holds
( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) )
let A, B, C be non empty closed_interval Subset of REAL; ::_thesis: for X being set st A c= X & f is_differentiable_on X & (f `| X) | A is continuous & lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A holds
( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) )
let X be set ; ::_thesis: ( A c= X & f is_differentiable_on X & (f `| X) | A is continuous & lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A implies ( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) ) )
assume that
A1: ( A c= X & f is_differentiable_on X ) and
A2: (f `| X) | A is continuous and
A3: lower_bound A = lower_bound B and
A4: upper_bound B = lower_bound C and
A5: upper_bound C = upper_bound A ; ::_thesis: ( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) )
consider x being Real such that
A6: x in B by SUBSET_1:4;
( lower_bound B <= x & x <= upper_bound B ) by A6, INTEGRA2:1;
then A7: lower_bound B <= upper_bound B by XXREAL_0:2;
consider x being Real such that
A8: x in C by SUBSET_1:4;
( lower_bound C <= x & x <= upper_bound C ) by A8, INTEGRA2:1;
then A9: lower_bound C <= upper_bound C by XXREAL_0:2;
for x being set st x in B holds
x in A
proof
let x be set ; ::_thesis: ( x in B implies x in A )
assume A10: x in B ; ::_thesis: x in A
then reconsider x = x as Real ;
x <= upper_bound B by A10, INTEGRA2:1;
then A11: x <= upper_bound A by A4, A5, A9, XXREAL_0:2;
lower_bound A <= x by A3, A10, INTEGRA2:1;
hence x in A by A11, INTEGRA2:1; ::_thesis: verum
end;
hence A12: B c= A by TARSKI:def_3; ::_thesis: ( C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) )
A13: A c= dom (f `| X) by A1, FDIFF_1:def_7;
then A14: (f `| X) | A is bounded by A2, Th10;
then A15: (f `| X) | B is bounded by A12, RFUNCT_1:74;
for x being set st x in C holds
x in A
proof
let x be set ; ::_thesis: ( x in C implies x in A )
assume A16: x in C ; ::_thesis: x in A
then reconsider x = x as Real ;
lower_bound C <= x by A16, INTEGRA2:1;
then A17: lower_bound A <= x by A3, A4, A7, XXREAL_0:2;
x <= upper_bound A by A5, A16, INTEGRA2:1;
hence x in A by A17, INTEGRA2:1; ::_thesis: verum
end;
hence A18: C c= A by TARSKI:def_3; ::_thesis: integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C))
then A19: (f `| X) | C is bounded by A14, RFUNCT_1:74;
(f `| X) | C is continuous by A2, A18, FCONT_1:16;
then f `| X is_integrable_on C by A13, A18, Th11, XBOOLE_1:1;
then A20: integral ((f `| X),C) = (f . (upper_bound C)) - (f . (lower_bound C)) by A1, A18, A19, Th13, XBOOLE_1:1;
(f `| X) | B is continuous by A2, A12, FCONT_1:16;
then f `| X is_integrable_on B by A13, A12, Th11, XBOOLE_1:1;
then A21: integral ((f `| X),B) = (f . (upper_bound B)) - (f . (lower_bound B)) by A1, A12, A15, Th13, XBOOLE_1:1;
f `| X is_integrable_on A by A2, A13, Th11;
then integral ((f `| X),A) = (f . (upper_bound A)) - (f . (lower_bound A)) by A1, A2, A13, Th10, Th13;
hence integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) by A3, A4, A5, A21, A20; ::_thesis: verum
end;
definition
let a, b be real number ;
assume A1: a <= b ;
func['a,b'] -> non empty closed_interval Subset of REAL equals :Def3: :: INTEGRA5:def 3
[.a,b.];
correctness
coherence
[.a,b.] is non empty closed_interval Subset of REAL;
proof
( a is Real & b is Real ) by XREAL_0:def_1;
hence [.a,b.] is non empty closed_interval Subset of REAL by A1, MEASURE5:14; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines [' INTEGRA5:def_3_:_
for a, b being real number st a <= b holds
['a,b'] = [.a,b.];
definition
let a, b be real number ;
let f be PartFunc of REAL,REAL;
func integral (f,a,b) -> Real equals :Def4: :: INTEGRA5:def 4
integral (f,['a,b']) if a <= b
otherwise - (integral (f,['b,a']));
correctness
coherence
( ( a <= b implies integral (f,['a,b']) is Real ) & ( not a <= b implies - (integral (f,['b,a'])) is Real ) );
consistency
for b1 being Real holds verum;
;
end;
:: deftheorem Def4 defines integral INTEGRA5:def_4_:_
for a, b being real number
for f being PartFunc of REAL,REAL holds
( ( a <= b implies integral (f,a,b) = integral (f,['a,b']) ) & ( not a <= b implies integral (f,a,b) = - (integral (f,['b,a'])) ) );
theorem :: INTEGRA5:19
for f being PartFunc of REAL,REAL
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 f be PartFunc of REAL,REAL; ::_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) )
consider a1, b1 being Real such that
A1: a1 <= b1 and
A2: A = [.a1,b1.] by MEASURE5:14;
assume A = [.a,b.] ; ::_thesis: integral (f,A) = integral (f,a,b)
then A3: ( a1 = a & b1 = b ) by A2, INTEGRA1:5;
then integral (f,a,b) = integral (f,['a,b']) by A1, Def4;
hence integral (f,A) = integral (f,a,b) by A1, A2, A3, Def3; ::_thesis: verum
end;
theorem :: INTEGRA5:20
for f being PartFunc of REAL,REAL
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 f be PartFunc of REAL,REAL; ::_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) )
consider a1, b1 being Real such that
A1: a1 <= b1 and
A2: A = [.a1,b1.] by MEASURE5:14;
assume A3: A = [.b,a.] ; ::_thesis: - (integral (f,A)) = integral (f,a,b)
then A4: ( a1 = b & b1 = a ) by A2, INTEGRA1:5;
now__::_thesis:_-_(integral_(f,A))_=_integral_(f,a,b)
percases ( b < a or b = a ) by A1, A4, XXREAL_0:1;
supposeA5: b < a ; ::_thesis: - (integral (f,A)) = integral (f,a,b)
then integral (f,a,b) = - (integral (f,['b,a'])) by Def4;
hence - (integral (f,A)) = integral (f,a,b) by A3, A5, Def3; ::_thesis: verum
end;
supposeA6: b = a ; ::_thesis: - (integral (f,A)) = integral (f,a,b)
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then ( lower_bound A = b & upper_bound A = a ) by A3, INTEGRA1:5;
then vol A = (upper_bound A) - (upper_bound A) by A6, INTEGRA1:def_5
.= 0 ;
then A7: integral (f,A) = 0 by INTEGRA4:6;
integral (f,a,b) = integral (f,['a,b']) by A6, Def4;
hence - (integral (f,A)) = integral (f,a,b) by A3, A6, A7, Def3; ::_thesis: verum
end;
end;
end;
hence - (integral (f,A)) = integral (f,a,b) ; ::_thesis: verum
end;
theorem :: INTEGRA5:21
for A being non empty closed_interval Subset of REAL
for f, g being PartFunc of REAL,REAL
for X being open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded holds
integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A))
proof
let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being PartFunc of REAL,REAL
for X being open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded holds
integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A))
let f, g be PartFunc of REAL,REAL; ::_thesis: for X being open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded holds
integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A))
let X be open Subset of REAL; ::_thesis: ( f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded implies integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A)) )
assume that
A1: f is_differentiable_on X and
A2: g is_differentiable_on X and
A3: A c= X and
A4: f `| X is_integrable_on A and
A5: (f `| X) | A is bounded and
A6: g `| X is_integrable_on A and
A7: (g `| X) | A is bounded ; ::_thesis: integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A))
A8: (f (#) g) `| X = ((f `| X) (#) g) + (f (#) (g `| X)) by A1, A2, FDIFF_2:20;
g | X is continuous by A2, FDIFF_1:25;
then A9: g | A is continuous by A3, FCONT_1:16;
X c= dom g by A2, FDIFF_1:def_6;
then A10: A c= dom g by A3, XBOOLE_1:1;
then A11: g || A is Function of A,REAL by Th6, FUNCT_2:68;
X c= dom g by A2, FDIFF_1:def_6;
then g is_integrable_on A by A3, A9, Th11, XBOOLE_1:1;
then A12: g || A is integrable by Def1;
A13: A c= dom (g `| X) by A2, A3, FDIFF_1:def_7;
then A14: (g `| X) || A is Function of A,REAL by Th6, FUNCT_2:68;
g | X is continuous by A2, FDIFF_1:25;
then g | A is bounded by A3, A10, Th10, FCONT_1:16;
then A15: ((f `| X) (#) g) | (A /\ A) is bounded by A5, RFUNCT_1:84;
then A16: (((f `| X) (#) g) || A) | A is bounded ;
f | X is continuous by A1, FDIFF_1:25;
then A17: f | A is continuous by A3, FCONT_1:16;
X c= dom f by A1, FDIFF_1:def_6;
then f is_integrable_on A by A3, A17, Th11, XBOOLE_1:1;
then A18: f || A is integrable by Def1;
A19: A c= dom (f `| X) by A1, A3, FDIFF_1:def_7;
then A20: (f `| X) || A is Function of A,REAL by Th6, FUNCT_2:68;
A21: ( (g `| X) || A is integrable & ((g `| X) || A) | A is bounded ) by A6, A7, Def1;
A22: ( (f `| X) || A is integrable & ((f `| X) || A) | A is bounded ) by A4, A5, Def1;
dom ((f `| X) (#) g) = (dom (f `| X)) /\ (dom g) by VALUED_1:def_4;
then A c= dom ((f `| X) (#) g) by A10, A19, XBOOLE_1:19;
then A23: ((f `| X) (#) g) || A is Function of A,REAL by Th6, FUNCT_2:68;
X c= dom f by A1, FDIFF_1:def_6;
then A24: A c= dom f by A3, XBOOLE_1:1;
then A25: f || A is Function of A,REAL by Th6, FUNCT_2:68;
f | X is continuous by A1, FDIFF_1:25;
then f | A is bounded by A3, A24, Th10, FCONT_1:16;
then A26: (f (#) (g `| X)) | (A /\ A) is bounded by A7, RFUNCT_1:84;
then A27: ((f (#) (g `| X)) || A) | A is bounded ;
(((f `| X) (#) g) + (f (#) (g `| X))) | (A /\ A) is bounded by A15, A26, RFUNCT_1:83;
then A28: ((f (#) g) `| X) | A is bounded by A1, A2, FDIFF_2:20;
A29: ( (f (#) g) . (upper_bound A) = (f . (upper_bound A)) * (g . (upper_bound A)) & (f (#) g) . (lower_bound A) = (f . (lower_bound A)) * (g . (lower_bound A)) ) by VALUED_1:5;
dom (f (#) (g `| X)) = (dom f) /\ (dom (g `| X)) by VALUED_1:def_4;
then A c= dom (f (#) (g `| X)) by A24, A13, XBOOLE_1:19;
then A30: (f (#) (g `| X)) || A is Function of A,REAL by Th6, FUNCT_2:68;
(g || A) | A is bounded by A9, A10, Th10;
then ((f `| X) || A) (#) (g || A) is integrable by A12, A11, A20, A22, INTEGRA4:29;
then A31: ((f `| X) (#) g) || A is integrable by Th4;
(f || A) | A is bounded by A17, A24, Th10;
then (f || A) (#) ((g `| X) || A) is integrable by A18, A25, A14, A21, INTEGRA4:29;
then A32: (f (#) (g `| X)) || A is integrable by Th4;
then integral ((((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A)) = (integral (((f `| X) (#) g) || A)) + (integral ((f (#) (g `| X)) || A)) by A31, A23, A16, A30, A27, INTEGRA1:57;
then A33: integral ((((f `| X) (#) g) + (f (#) (g `| X))) || A) = (integral (((f `| X) (#) g),A)) + (integral ((f (#) (g `| X)),A)) by Th5;
(((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A) is integrable by A31, A32, A23, A16, A30, A27, INTEGRA1:57;
then (((f `| X) (#) g) + (f (#) (g `| X))) || A is integrable by Th5;
then A34: (f (#) g) `| X is_integrable_on A by A8, Def1;
integral (((f (#) g) `| X) || A) = integral (((f (#) g) `| X),A)
.= ((f (#) g) . (upper_bound A)) - ((f (#) g) . (lower_bound A)) by A1, A2, A3, A34, A28, Th13, FDIFF_2:20 ;
hence integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A)) by A8, A29, A33; ::_thesis: verum
end;