:: Antiderivatives and Integration
:: by Noboru Endou
::
:: Received June 30, 2023
:: Copyright (c) 2023-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, SUBSET_1, SEQ_1, FDIFF_1, XXREAL_0, CARD_1,
COMPLEX1, FUNCT_1, RELAT_1, ARYTM_3, NAT_1, REALSET1, ARYTM_1, VALUED_1,
CARD_3, SEQ_2, ORDINAL2, SQUARE_1, VALUED_0, XXREAL_2, FUNCT_2, TARSKI,
RCOMP_1, XXREAL_1, PARTFUN1, XBOOLE_0, FCONT_1, FUNCT_7, INTEGRA5,
FINSEQ_1, ZFMISC_1, LIMFUNC2, INTEGRA1, ORDINAL4, FINSEQ_2, MEASURE7,
SEQ_4, MEASURE5, FDIFF_3, FDIFF_12, SUPINF_1, MEMBERED, INTEGR26;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, XCMPLX_0, XREAL_0,
NUMBERS, XXREAL_0, COMPLEX1, XXREAL_1, XXREAL_2, RELSET_1, FUNCT_1,
PARTFUN1, FUNCT_2, VALUED_0, VALUED_1, RCOMP_1, FINSEQ_1, SEQ_1,
RFUNCT_1, FINSEQ_2, SEQ_2, SEQ_4, FCONT_1, SUPINF_1, LIMFUNC2, FDIFF_1,
RVSUM_1, MEASURE5, INTEGRA1, INTEGRA5, FDIFF_3, FDIFF_12, MEMBERED;
constructors FCONT_1, RELSET_1, RVSUM_1, REAL_1, SQUARE_1, COMPLEX1, COMSEQ_2,
MEASURE6, MESFUNC5, INTEGRA5, FDIFF_1, INTEGRA2, SEQ_4, FDIFF_3,
FDIFF_12, LIMFUNC2;
registrations XREAL_0, RELSET_1, INTEGRA1, RCOMP_1, INT_1, MEMBERED, XBOOLE_0,
NUMBERS, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, SEQ_2, FCONT_3, FINSEQ_2,
RELAT_1, ORDINAL1, XXREAL_0, NAT_1, FINSEQ_1, FDIFF_1, CARD_1, MEASURE5,
SEQ_4, FCONT_1, RFUNCT_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities XCMPLX_0, INTEGRA1, INTEGRA5, VALUED_1;
expansions INTEGRA1, INTEGRA5, FDIFF_1, TARSKI;
theorems TARSKI, PARTFUN1, RVSUM_1, ZFMISC_1, INTEGRA1, INTEGRA2, RFUNCT_1,
FUNCT_1, SEQ_1, SEQ_2, FDIFF_1, ABSVALUE, XCMPLX_1, FINSEQ_1, FINSEQ_2,
RCOMP_1, FCONT_1, RELAT_1, XREAL_0, XXREAL_0, PARTFUN2, FUNCT_2,
XBOOLE_0, XBOOLE_1, SEQ_4, XREAL_1, COMPLEX1, INTEGRA4, INTEGRA5,
INTEGRA6, VALUED_1, XXREAL_1, XXREAL_2, ORDINAL1, MEASURE5, RELSET_1,
NAT_1, RFUNCT_2, PDIFFEQ1, FDIFF_3, MEASURE6, ROLLE, NAT_2, INT_1,
FDIFF_12, LIMFUNC2;
schemes FUNCT_2, PARTFUN1, FINSEQ_2;
begin :: Basic theorems on continuity and derivativity
reserve h,h1 for 0-convergent non-zero Real_Sequence,
c,c1 for constant Real_Sequence;
registration
cluster open_interval -> open for Subset of REAL;
coherence
proof
let I be Subset of REAL;
assume A1: I is open_interval;
now assume I is non empty; then
I = ].inf I,sup I.[ by A1,MEASURE6:16;
hence I is open by FDIFF_12:2;
end;
hence thesis;
end;
end;
theorem Th1:
for I be Interval st inf I in I holds inf I = lower_bound I
proof
let I be Interval;
assume inf I in I; then
reconsider J=I as non empty left_end real-membered set by XXREAL_2:def 5;
inf J = lower_bound J;
hence inf I = lower_bound I;
end;
theorem Th2:
for I be interval Subset of REAL st sup I in I holds sup I = upper_bound I
proof
let I be interval Subset of REAL;
assume sup I in I; then
reconsider J=I as non empty right_end real-membered set by XXREAL_2:def 6;
sup J = upper_bound J;
hence sup I = upper_bound I;
end;
theorem Th3:
for a,b be Real, I be Interval st a in I & b in I holds [.a,b.] c= I
proof
let a,b be Real, I be Interval;
assume that
A1: a in I and
A2: b in I;
per cases by MEASURE5:1;
suppose I is open_interval; then
consider p,q be R_eal such that
A3: I = ].p,q.[ by MEASURE5:def 2;
A4: p < a & b < q by A1,A2,A3,XXREAL_1:4;
now let x be Real;
assume x in [.a,b.]; then
a <= x & x <= b by XXREAL_1:1; then
p < x & x < q by A4,XXREAL_0:2;
hence x in I by A3,XXREAL_1:4;
end;
hence [.a,b.] c= I;
end;
suppose I is closed_interval; then
consider p,q be Real such that
A5: I = [.p,q.] by MEASURE5:def 3;
A6: p <= a & b <= q by A1,A2,A5,XXREAL_1:1;
now let x be Real;
assume x in [.a,b.]; then
a <= x & x <= b by XXREAL_1:1; then
p <= x & x <= q by A6,XXREAL_0:2;
hence x in I by A5,XXREAL_1:1;
end;
hence [.a,b.] c= I;
end;
suppose I is left_open_interval; then
consider p be R_eal, q be Real such that
A7: I = ].p,q.] by MEASURE5:def 5;
A8: p < a & b <= q by A1,A2,A7,XXREAL_1:2;
now let x be Real;
assume x in [.a,b.]; then
a <= x & x <= b by XXREAL_1:1; then
p < x & x <= q by A8,XXREAL_0:2;
hence x in I by A7,XXREAL_1:2;
end;
hence [.a,b.] c= I;
end;
suppose I is right_open_interval; then
consider p be Real, q be R_eal such that
A9: I = [.p,q.[ by MEASURE5:def 4;
A10: p <= a & b < q by A1,A2,A9,XXREAL_1:3;
now let x be Real;
assume x in [.a,b.]; then
a <= x & x <= b by XXREAL_1:1; then
p <= x & x < q by A10,XXREAL_0:2;
hence x in I by A9,XXREAL_1:3;
end;
hence [.a,b.] c= I;
end;
end;
theorem Th4:
for f be PartFunc of REAL,REAL, a,b be Real st
a < b & [.a,b.[ c= dom f & f|([.a,b.[) is continuous &
f is_differentiable_on ].a,b.[ & f`|(].a,b.[) is_right_convergent_in a holds
f is_right_differentiable_in a & Rdiff(f,a) = lim_right(f`|(].a,b.[),a)
proof
let f be PartFunc of REAL,REAL, a,b be Real;
assume that
A1: a < b and
A2: [.a,b.[ c= dom f and
A3: f|([.a,b.[) is continuous and
A4: f is_differentiable_on ].a,b.[ and
A5: f`|(].a,b.[) is_right_convergent_in a;
consider e be Real such that
A6: a < e & e < b by A1,XREAL_1:5;
[.a,e.] c= [.a,b.[ by A6,XXREAL_1:43; then
A7: [.a,e.] c= dom f by A2;
set r = e-a;
a+r=e; then
A8: ex r be Real st r > 0 & [.a,a+r.] c= dom f by A7,A6,XREAL_1:50;
for h,c st rng c = {a} & rng (h+c) c= dom f &
(for n be Nat holds h.n > 0) holds
h"(#)(f/*(h+c) - f/*c) is convergent &
lim(h"(#)(f/*(h+c)-f/*c)) = lim_right(f`|(].a,b.[),a)
proof
let h,c;
assume that
A9: rng c = {a} and
A10: rng(h+c) c= dom f and
A11: for n be Nat holds h.n > 0;
A12: h is convergent & lim h = 0;
A13: a in [.a,b.[ by A1,XXREAL_1:3;
A14: dom(f`|(].a,b.[)) = ].a,b.[ by A4,FDIFF_1:def 7;
A15: for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds
|. (h"(#)(f/*(h+c) - f/*c)).m - lim_right(f`|(].a,b.[),a) .| < p
proof
let p be Real;
assume 0 < p; then
consider R be Real such that
A16: a < R and
A17: for r1 be Real st r1 < R & a < r1 & r1 in dom(f`|(].a,b.[)) holds
|. (f`|(].a,b.[)).r1 - lim_right(f`|(].a,b.[),a) .| < p
by A5,LIMFUNC2:42;
set r = min(b,R);
A18: a < r & r <= b & r <= R by A1,A16,XXREAL_0:17,21; then
r-a > 0 by XREAL_1:50; then
consider N be Nat such that
A19: for m be Nat st N <= m holds |. h.m - 0 .| < r-a by A12,SEQ_2:def 7;
take N;
thus for m be Nat st N <= m holds
|. (h"(#)(f/*(h+c) - f/*c)).m - lim_right(f`|(].a,b.[),a) .| < p
proof
let m be Nat;
assume N <= m; then
h.m > 0 & |. h.m - 0 .| < r-a by A11,A19; then
A20: h.m < r-a by ABSVALUE:def 1;
A21: m in NAT by ORDINAL1:def 12; then
A22: m in dom(h+c) & m in dom c by FUNCT_2:def 1; then
c.m in rng c by FUNCT_1:3; then
A23: c.m = a by A9,TARSKI:def 1; then
A24: (h+c).m = h.m + a by A22,VALUED_1:def 1; then
A25: (h+c).m < (r-a) + a by A20,XREAL_1:8;
set H=(h+c).m;
A26: a < H by A11,A24,XREAL_1:29;
A27: H < b by A18,A25,XXREAL_0:2; then
[.a,H.] c= [.a,b.[ by XXREAL_1:43; then
A28: [.a,H.] c= dom f by A2;
A29: f|[.a,H.] is continuous by A3,A27,FCONT_1:16,XXREAL_1:43;
A30: ].a,H.[ c= ].a,b.[ by A27,XXREAL_1:46; then
consider x0 be Real such that
A31: x0 in ].a,H.[ and
A32: diff(f,x0) = (f.H - f.a)/(H-a) by A26,A28,A29,A4,FDIFF_1:26,ROLLE:3;
A33: a < x0 & x0 < H by A31,XXREAL_1:4; then
x0 < r by A25,XXREAL_0:2; then
A34: x0 < R by A18,XXREAL_0:2;
A35: dom(f/*(h+c) - f/*c) = NAT /\ NAT by FUNCT_2:def 1;
f.H = (f/*(h+c)).m & f.a = (f/*c).m
by A10,A21,A23,A13,A2,A9,ZFMISC_1:31,FUNCT_2:108; then
f.H - f.a = (f/*(h+c) - f/*c).m
by A35,VALUED_1:13,ORDINAL1:def 12; then
((f/*(h+c)-f/*c)/"h).m = (f.H - f.a)/(H-a) by A24,VALUED_1:17; then
(h"(#)(f/*(h+c) - f/*c)).m = (f`|(].a,b.[)).x0
by A4,A30,A31,A32,FDIFF_1:def 7;
hence |. (h"(#)(f/*(h+c) - f/*c)).m - lim_right(f`|(].a,b.[),a) .| < p
by A17,A33,A34,A30,A31,A14;
end;
end;
hence h"(#)(f/*(h+c) - f/*c) is convergent by SEQ_2:def 6;
hence lim(h"(#)(f/*(h+c)-f/*c)) = lim_right(f`|(].a,b.[),a)
by A15,SEQ_2:def 7;
end;
hence f is_right_differentiable_in a &
Rdiff(f,a) = lim_right(f`|(].a,b.[),a) by A8,FDIFF_3:15;
end;
theorem Th5:
for f be PartFunc of REAL,REAL, a,b be Real st
a < b & ].a,b.] c= dom f & f|(].a,b.]) is continuous &
f is_differentiable_on ].a,b.[ & f`|(].a,b.[) is_left_convergent_in b holds
f is_left_differentiable_in b & Ldiff(f,b) = lim_left(f`|(].a,b.[),b)
proof
let f be PartFunc of REAL,REAL, a,b be Real;
assume that
A1: a < b and
A2: ].a,b.] c= dom f and
A3: f|(].a,b.]) is continuous and
A4: f is_differentiable_on ].a,b.[ and
A5: f`|(].a,b.[) is_left_convergent_in b;
consider e be Real such that
A6: a < e & e < b by A1,XREAL_1:5;
[.e,b.] c= ].a,b.] by A6,XXREAL_1:39; then
A7: [.e,b.] c= dom f by A2;
set r = b-e;
e=b-r; then
A8: ex r be Real st r > 0 & [.b-r,b.] c= dom f by A7,A6,XREAL_1:50;
for h,c st rng c = {b} & rng (h+c) c= dom f &
(for n be Nat holds h.n < 0) holds
h"(#)(f/*(h+c) - f/*c) is convergent &
lim(h"(#)(f/*(h+c)-f/*c)) = lim_left(f`|(].a,b.[),b)
proof
let h,c;
assume that
A9: rng c = {b} and
A10: rng(h+c) c= dom f and
A11: for n be Nat holds h.n < 0;
A12: h is convergent & lim h = 0;
A13: b in ].a,b.] by A1,XXREAL_1:2;
A14: dom(f`|(].a,b.[)) = ].a,b.[ by A4,FDIFF_1:def 7;
A15: for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds
|. (h"(#)(f/*(h+c) - f/*c)).m - lim_left(f`|(].a,b.[),b) .| < p
proof
let p be Real;
assume
A16: 0 < p;
consider R be Real such that
A17: R < b and
A18: for r1 be Real st R < r1 & r1 < b & r1 in dom(f`|(].a,b.[)) holds
|. (f`|(].a,b.[)).r1 - lim_left(f`|(].a,b.[),b) .| < p
by A5,A16,LIMFUNC2:41;
set r = max(a,R);
A19: r < b & a <= r & R <= r by A1,A17,XXREAL_0:25,29;
b-r > 0 by A19,XREAL_1:50; then
consider N be Nat such that
A20: for m be Nat st N <= m holds |. h.m - 0 .| < b-r by A12,SEQ_2:def 7;
take N;
thus for m be Nat st N <= m holds
|. (h"(#)(f/*(h+c) - f/*c)).m - lim_left(f`|(].a,b.[),b) .| < p
proof
let m be Nat;
assume
A21: N <= m;
A22: |. h.m - 0 .| < b-r by A20,A21;
h.m < 0 by A11; then
-h.m < b-r by A22,ABSVALUE:30; then
A23: h.m > -(b-r) by XREAL_1:25;
A24: m in NAT by ORDINAL1:def 12; then
A25: m in dom(h+c) & m in dom c by FUNCT_2:def 1; then
c.m in rng c by FUNCT_1:3; then
A26: c.m = b by A9,TARSKI:def 1; then
A27: (h+c).m = h.m + b by A25,VALUED_1:def 1; then
A28: (r-b)+b < (h+c).m by A23,XREAL_1:8;
set H=(h+c).m;
A29: H < b by A11,A27,XREAL_1:30;
A30: a < H by A19,A28,XXREAL_0:2; then
[.H,b.] c= ].a,b.] by XXREAL_1:39; then
A31: [.H,b.] c= dom f by A2;
A32: f|[.H,b.] is continuous by A3,A30,FCONT_1:16,XXREAL_1:39;
A33: ].H,b.[ c= ].a,b.[ by A30,XXREAL_1:46; then
consider x0 be Real such that
A34: x0 in ].H,b.[ and
A35: diff(f,x0) = (f.b - f.H)/(b-H) by A29,A31,A32,A4,FDIFF_1:26,ROLLE:3;
A36: H < x0 & x0 < b by A34,XXREAL_1:4; then
r < x0 by A28,XXREAL_0:2; then
A37: R < x0 by A19,XXREAL_0:2;
A38: dom(f/*c - f/*(h+c)) = NAT /\ NAT by FUNCT_2:def 1;
A39: f.H = (f/*(h+c)).m by A10,A24,FUNCT_2:108;
f.b = (f/*c).m by A26,A13,A24,A2,A9,ZFMISC_1:31,FUNCT_2:108; then
A40: f.b - f.H = (f/*c - f/*(h+c)).m by A39,A38,ORDINAL1:def 12,VALUED_1:13;
-(h.m) = b-H by A27; then
(f.b - f.H)/(b-H) = (f/*c - f/*(h+c)).m / (-h).m by A40,VALUED_1:8; then
(f.b - f.H)/(b-H) = ((f/*c - f/*(h+c))/"(-h)).m by VALUED_1:17; then
(f.b - f.H)/(b-H) = (-((f/*c - f/*(h+c))/"h)).m by SEQ_1:48; then
(f.b - f.H)/(b-H) = (((-(f/*c - f/*(h+c)))/"h)).m by SEQ_1:48; then
(f.b - f.H)/(b-H) = (( (-1)(#)f/*c + (-1)(#)(-f/*(h+c)) )/"h).m
by SEQ_1:22; then
(f.b - f.H)/(b-H) = (( -f/*c + ((-1)*(-1))(#)f/*(h+c) )/"h).m
by RFUNCT_1:17; then
(f.b - f.H)/(b-H) = (( -f/*c + f/*(h+c) )/"h).m by SEQ_1:27; then
(h"(#)(f/*(h+c) - f/*c)).m = (f`|(].a,b.[)).x0
by A4,A33,A34,A35,FDIFF_1:def 7;
hence |. (h"(#)(f/*(h+c) - f/*c)).m - lim_left(f`|(].a,b.[),b) .| < p
by A18,A36,A37,A33,A34,A14;
end;
end;
hence h"(#)(f/*(h+c) - f/*c) is convergent by SEQ_2:def 6;
hence lim(h"(#)(f/*(h+c)-f/*c)) = lim_left(f`|(].a,b.[),b)
by A15,SEQ_2:def 7;
end;
hence f is_left_differentiable_in b &
Ldiff(f,b) = lim_left(f`|(].a,b.[),b) by A8,FDIFF_3:9;
end;
theorem Th6:
for a,b,x be Real, f be PartFunc of REAL,REAL, I be Interval st
inf I <= a & b <= sup I & I c= dom f &
f|I is continuous & x in ].a,b.[ holds
f is_continuous_in x
proof
let a,b,x be Real, f be PartFunc of REAL,REAL, I be Interval;
assume that
A1: inf I <= a and
A2: b <= sup I and
A3: I c= dom f and
A4: f|I is continuous and
A5: x in ].a,b.[;
A6: ].inf I,sup I.[ c= I by FDIFF_12:2;
A7: ].a,b.[ c= ].inf I,sup I.[ by A1,A2,XXREAL_1:46; then
].a,b.[ c= I by A6; then
A8: f|(].a,b.[) is continuous by A4,FCONT_1:16;
].a,b.[ c= dom f by A7,A6,A3; then
A9: ].a,b.[ c= dom(f|].a,b.[) by RELAT_1:62;
now let r be Real;
assume 0 < r; then
consider s1 be Real such that
A10: 0 < s1 &
for x1 be Real st x1 in dom(f|(].a,b.[)) & |.x1-x.| < s1 holds
|. (f|(].a,b.[)).x1 - (f|(].a,b.[)).x .| < r
by A8,A5,A9,FCONT_1:def 2,3;
a < x & x < b by A5,XXREAL_1:4; then
A11: 0 < x-a & 0 < b-x by XREAL_1:50; then
A12: 0 < (x-a)/2 & 0 < (b-x)/2 by XREAL_1:215;
set s2 = min((x-a)/2,(b-x)/2);
A13: 0 < s2 by A12,XXREAL_0:21;
take s = min(s1,s2);
thus 0 < s by A10,A13,XXREAL_0:21;
A14: (x-a)/2 < x-a & (b-x)/2 < b-x by A11,XREAL_1:216;
s2 <= (x-a)/2 & s2 <= (b-x)/2 by XXREAL_0:17; then
A15: s2 < x-a & s2 < b-x by A14,XXREAL_0:2;
A16: s <= s1 & s <= s2 by XXREAL_0:17; then
s < x-a & s < b-x by A15,XXREAL_0:2; then
A17: a < x-s & x+s < b by XREAL_1:12,20;
thus for x1 be Real st x1 in dom f & |.x1-x.| < s holds
|. f.x1-f.x .| < r
proof
let x1 be Real;
assume that
x1 in dom f and
A18: |.x1-x.| < s;
A19: -|.x1-x.| <= x1-x & x1-x <= |.x1-x.| by ABSVALUE:4; then
x1-x < s by A18,XXREAL_0:2; then
x1 < x+s by XREAL_1:19; then
A20: x1 < b by A17,XXREAL_0:2;
-(x1-x) <= |.x1-x.| by A19,XREAL_1:26; then
x-x1 < s by A18,XXREAL_0:2; then
x < s+x1 by XREAL_1:19; then
x-s < x1 by XREAL_1:19; then
a < x1 by A17,XXREAL_0:2; then
A21: x1 in dom(f|(].a,b.[)) by A9,A20,XXREAL_1:4; then
A22: (f|(].a,b.[)).x1 = f.x1 & (f|(].a,b.[)).x = f.x by A5,A9,FUNCT_1:47;
|.x1-x.| < s1 by A18,A16,XXREAL_0:2;
hence |. f.x1-f.x .| < r by A10,A21,A22;
end;
end;
hence f is_continuous_in x by FCONT_1:3;
end;
theorem
for X be open Subset of REAL, f,F be PartFunc of REAL,REAL st
X c= dom f & f|X is continuous holds
for x be Real st x in X holds f is_continuous_in x
proof
let X be open Subset of REAL, f,F be PartFunc of REAL,REAL;
assume that
A1: X c= dom f and
A2: f|X is continuous;
A3: dom(f|X) = X by A1,RELAT_1:62;
hereby let x be Real;
assume
A4: x in X;
for r be Real st 0 < r
ex s be Real st 0 < s & for x1 be Real st x1 in dom f & |.x1-x.| < s
holds |.f.x1 - f.x.| < r
proof
let r be Real;
consider ss1 be Real such that
A5: 0 < ss1 and
A6: ].x-ss1,x+ss1.[ c= X by A4,RCOMP_1:19;
assume 0 < r; then
consider s be Real such that
A7: 0 < s and
A8: for x1 be Real st x1 in dom(f|X) & |.x1-x.|<s holds
|.(f|X).x1 - (f|X).x.| < r by A2,A4,A3,FCONT_1:def 2,3;
set s1=min(ss1,s);
take s1;
now let x1 be Real;
assume that
x1 in dom f and
A9: |.x1-x.|<s1;
s1 <= s by XXREAL_0:17; then
A10: |.x1-x.| < s by A9,XXREAL_0:2;
s1 <= ss1 by XXREAL_0:17;
then |.x1-x.| < ss1 by A9,XXREAL_0:2;
then
A11: x1 in ].x-ss1,x+ss1.[ by RCOMP_1:1;
then |.f.x1-f.x.| = |.(f|X).x1 - f.x.| by A6,A3,FUNCT_1:47;
then |.f.x1-f.x.| = |.(f|X).x1 - (f|X).x.| by A4,A3,FUNCT_1:47;
hence |.f.x1-f.x.|<r by A8,A6,A10,A11,A3;
end;
hence thesis by A7,A5,XXREAL_0:15;
end;
hence f is_continuous_in x by FCONT_1:3;
end;
end;
theorem Th8:
for a,b,x be Real, f be PartFunc of REAL,REAL st a <= x < b &
].a,b.[ c= dom f & f is_right_convergent_in x holds
f|(].a,b.[) is_right_convergent_in x &
lim_right(f|(].a,b.[),x) = lim_right(f,x)
proof
let a,b,x be Real, f be PartFunc of REAL,REAL;
assume that
A1: a <= x < b and
A2: ].a,b.[ c= dom f and
A3: f is_right_convergent_in x;
A4: dom(f|(].a,b.[)) = ].a,b.[ by A2,RELAT_1:62;
A5: for r be Real st x < r
ex g be Real st g < r & x < g & g in dom(f|(].a,b.[))
proof
let r be Real;
assume A6: x < r;
set s = min(r,b);
consider g be Real such that
A7: x < g & g < s by A6,A1,XXREAL_0:21,XREAL_1:5;
A8: s <= r & s <= b by XXREAL_0:17; then
A9: g < r by A7,XXREAL_0:2;
a < g & g < b by A1,A7,A8,XXREAL_0:2;
hence thesis by A7,A9,A4,XXREAL_1:4;
end;
A10: for r be Real st 0 < r
ex d be Real st x < d & for x1 be Real st x1 < d & x < x1 &
x1 in dom(f|(].a,b.[)) holds
|. (f|(].a,b.[)).x1 - lim_right(f,x) .| < r
proof
let r be Real;
assume 0 < r; then
consider d0 be Real such that
A11: x < d0 &
for x1 be Real st x1 < d0 & x < x1 & x1 in dom f holds
|. f.x1 - lim_right(f,x) .| < r by A3,LIMFUNC2:42;
set d = min(d0,b);
for x1 be Real st x1 < d & x < x1 & x1 in dom(f|(].a,b.[))
holds |. (f|(].a,b.[)).x1 - lim_right(f,x) .| < r
proof
let x1 be Real;
assume that
A12: x1 < d and
A13: x < x1 and
A14: x1 in dom(f|(].a,b.[));
d <= d0 by XXREAL_0:17; then
A15: x1 < d0 by A12,XXREAL_0:2;
x1 in dom f by A14,RELAT_1:57; then
|. f.x1 - lim_right(f,x) .| < r by A15,A13,A11;
hence |. (f|(].a,b.[)).x1 - lim_right(f,x) .| < r by A14,FUNCT_1:47;
end;
hence thesis by A11,A1,XXREAL_0:21;
end;
hence f|(].a,b.[) is_right_convergent_in x by A5,LIMFUNC2:10;
hence lim_right(f|(].a,b.[),x) = lim_right(f,x) by A10,LIMFUNC2:42;
end;
theorem Th9:
for a,b,x be Real, f be PartFunc of REAL,REAL st a < x <= b &
].a,b.[ c= dom f & f is_left_convergent_in x holds
f|(].a,b.[) is_left_convergent_in x &
lim_left(f|(].a,b.[),x) = lim_left(f,x)
proof
let a,b,x be Real, f be PartFunc of REAL,REAL;
assume that
A1: a < x <= b and
A2: ].a,b.[ c= dom f and
A3: f is_left_convergent_in x;
A4: dom(f|(].a,b.[)) = ].a,b.[ by A2,RELAT_1:62;
A5: for r be Real st r < x
ex g be Real st r < g & g < x & g in dom(f|(].a,b.[))
proof
let r be Real;
assume A6: r < x;
set s = max(r,a);
consider g be Real such that
A7: s < g & g < x by A6,A1,XXREAL_0:29,XREAL_1:5;
r <= s & a <= s by XXREAL_0:25; then
r < g & a < g & g < b by A1,A7,XXREAL_0:2;
hence thesis by A7,A4,XXREAL_1:4;
end;
A8: for r be Real st 0 < r
ex d be Real st d < x & for x1 be Real st d < x1 & x1 < x &
x1 in dom(f|(].a,b.[)) holds
|. (f|(].a,b.[)).x1 - lim_left(f,x) .| < r
proof
let r be Real;
assume 0 < r; then
consider d0 be Real such that
A9: d0 < x &
for x1 be Real st d0 < x1 & x1 < x & x1 in dom f holds
|. f.x1 - lim_left(f,x) .| < r by A3,LIMFUNC2:41;
set d = max(d0,a);
for x1 be Real st d < x1 & x1 < x & x1 in dom(f|(].a,b.[))
holds |. (f|(].a,b.[)).x1 - lim_left(f,x) .| < r
proof
let x1 be Real;
assume that
A10: d < x1 and
A11: x1 < x and
A12: x1 in dom(f|(].a,b.[));
d0 <= d by XXREAL_0:25; then
A13: d0 < x1 by A10,XXREAL_0:2;
x1 in dom f by A12,RELAT_1:57; then
|. f.x1 - lim_left(f,x) .| < r by A13,A11,A9;
hence |. (f|(].a,b.[)).x1 - lim_left(f,x) .| < r by A12,FUNCT_1:47;
end;
hence thesis by A9,A1,XXREAL_0:29;
end;
hence f|(].a,b.[) is_left_convergent_in x by A5,LIMFUNC2:7;
hence lim_left(f|(].a,b.[),x) = lim_left(f,x) by A8,LIMFUNC2:41;
end;
theorem Th10:
for a,b,x be Real, f be PartFunc of REAL,REAL st
[.a,b.] c= dom f & f|[.a,b.] is continuous & x in [.a,b.[ holds
f is_right_convergent_in x & lim_right(f|(].a,b.[),x) = f.x
proof
let a,b,x be Real, f be PartFunc of REAL,REAL;
assume that
A1: [.a,b.] c= dom f and
A2: f|[.a,b.] is continuous and
A3: x in [.a,b.[;
A4: a <= x & x < b by A3,XXREAL_1:3;
A5: for r be Real st x < r ex g be Real st g < r & x < g & g in dom f
proof
let r be Real;
set r1 = min(r,b);
assume x < r; then
consider g be Real such that
A6: x < g & g < r1 by A4,XXREAL_0:21,XREAL_1:5;
r1 <= r by XXREAL_0:17; then
A7: g < r by A6,XXREAL_0:2;
r1 <= b by XXREAL_0:17; then
a <= g & g < b by A4,A6,XXREAL_0:2; then
g in [.a,b.] by XXREAL_1:1;
hence thesis by A1,A6,A7;
end;
A8: dom(f|[.a,b.]) = [.a,b.] by A1,RELAT_1:62;
A9: [.a,b.[ c= [.a,b.] by XXREAL_1:24;
].a,b.[ c= [.a,b.] by XXREAL_1:25; then
A10: ].a,b.[ c= dom f by A1;
A11: for r be Real st 0 < r
ex s be Real st x < s & for x1 be Real st x1 < s & x < x1 & x1 in dom f
holds |. f.x1-f.x .| < r
proof
let r be Real;
assume 0 < r; then
consider e be Real such that
A12: 0 < e & for x1 be Real st x1 in dom(f|[.a,b.]) & |.x1-x.|<e holds
|.(f|[.a,b.]).x1 - (f|[.a,b.]).x .| < r by A9,A2,A3,A8,FCONT_1:def 2,3;
set s1 = x+e;
set s = min(s1,b);
A13: s <= s1 & s <= b by XXREAL_0:17;
A14: x < s1 by A12,XREAL_1:29;
take s;
thus x < s by A4,A14,XXREAL_0:21;
hereby let x1 be Real;
assume that
A15: x1 < s and
A16: x < x1 and
x1 in dom f;
A17: x1 - x < s - x by A15,XREAL_1:9;
s - x <= s1 - x by XXREAL_0:17,XREAL_1:9; then
A18: x1 - x < s1 - x by A17,XXREAL_0:2;
x1-x > 0 by A16,XREAL_1:50; then
A19: |.x1-x.| < e by A18,ABSVALUE:def 1;
a <= x by A9,A3,XXREAL_1:1; then
A20: a < x1 & x1 < b by A15,A13,A16,XXREAL_0:2; then
A21: x1 in dom(f|[.a,b.]) by A8,XXREAL_1:1;
(f|[.a,b.]).x1 = f.x1 & (f|[.a,b.]).x = f.x
by A9,A3,A8,A20,XXREAL_1:1,FUNCT_1:47;
hence |. f.x1-f.x .| < r by A12,A19,A21;
end;
end;
hence
A22: f is_right_convergent_in x by A5,LIMFUNC2:10;
A23: for r be Real st 0 < r
ex s be Real st x < s &
for x1 be Real st x1 < s & x < x1 & x1 in dom(f|(].a,b.[))
holds |. (f|(].a,b.[)).x1 - f.x .| < r
proof
let r be Real;
assume 0 < r; then
consider s0 be Real such that
A24: x < s0 & for x1 be Real st x1 < s0 & x < x1 & x1 in dom f
holds |. f.x1-f.x .| < r by A11;
set s = min(s0,b);
for x1 be Real st x1 < s & x < x1 & x1 in dom(f|(].a,b.[))
holds |. (f|(].a,b.[)).x1 - f.x .| < r
proof
let x1 be Real;
assume that
A25: x1 < s and
A26: x < x1 and
A27: x1 in dom(f|(].a,b.[));
s <= s0 by XXREAL_0:17; then
A28: x1 < s0 by A25,XXREAL_0:2;
x1 in dom f by A27,RELAT_1:57; then
|. f.x1-f.x .| < r by A24,A28,A26;
hence |. (f|(].a,b.[)).x1 - f.x .| < r by A27,FUNCT_1:47;
end;
hence thesis by A24,A4,XXREAL_0:21;
end;
f|(].a,b.[) is_right_convergent_in x &
lim_right(f|(].a,b.[),x) = lim_right(f,x) by A4,A22,A10,Th8;
hence lim_right(f|(].a,b.[),x) = f.x by A23,LIMFUNC2:42;
end;
theorem Th11:
for a,b,x be Real, f be PartFunc of REAL,REAL st
[.a,b.] c= dom f & f|[.a,b.] is continuous & x in ].a,b.] holds
f is_left_convergent_in x & lim_left(f|(].a,b.[),x) = f.x
proof
let a,b,x be Real, f be PartFunc of REAL,REAL;
assume that
A1: [.a,b.] c= dom f and
A2: f|[.a,b.] is continuous and
A3: x in ].a,b.];
A4: a < x & x <= b by A3,XXREAL_1:2;
A5: for r be Real st r < x ex g be Real st r < g & g < x & g in dom f
proof
let r be Real;
set r1 = max(r,a);
assume r < x; then
consider g be Real such that
A6: r1 < g & g < x by A4,XXREAL_0:29,XREAL_1:5;
r <= r1 by XXREAL_0:25; then
A7: r < g by A6,XXREAL_0:2;
a <= r1 by XXREAL_0:25; then
a <= g & g < b by A4,A6,XXREAL_0:2; then
g in [.a,b.] by XXREAL_1:1;
hence thesis by A1,A6,A7;
end;
A8: dom(f|[.a,b.]) = [.a,b.] by A1,RELAT_1:62;
A9: ].a,b.] c= [.a,b.] by XXREAL_1:23;
].a,b.[ c= [.a,b.] by XXREAL_1:25; then
A10: ].a,b.[ c= dom f by A1;
A11: for r be Real st 0 < r
ex s be Real st s < x & for x1 be Real st s < x1 & x1 < x & x1 in dom f
holds |. f.x1-f.x .| < r
proof
let r be Real;
assume 0 < r; then
consider e be Real such that
A12: 0 < e & for x1 be Real st x1 in dom(f|[.a,b.]) & |.x1-x.|<e holds
|.(f|[.a,b.]).x1 - (f|[.a,b.]).x .| < r by A9,A2,A3,A8,FCONT_1:def 2,3;
set s1 = x-e;
set s = max(s1,a);
A13: s1 <= s & a <= s by XXREAL_0:25;
A14: s1 < x by A12,XREAL_1:44;
take s;
thus s < x by A4,A14,XXREAL_0:29;
hereby let x1 be Real;
assume that
A15: s < x1 and
A16: x1 < x and
x1 in dom f;
A17: s- x < x1 - x by A15,XREAL_1:9;
s1 - x <= s - x by XXREAL_0:25,XREAL_1:9; then
s1 - x < x1 - x by A17,XXREAL_0:2; then
A18: -(x1-x) < -(s1-x) by XREAL_1:24;
x1-x < 0 by A16,XREAL_1:49; then
A19: |.x1-x.| < e by A18,ABSVALUE:30;
x <= b by A9,A3,XXREAL_1:1; then
A20: a < x1 & x1 < b by A15,A13,A16,XXREAL_0:2; then
A21: x1 in dom(f|[.a,b.]) by A8,XXREAL_1:1;
(f|[.a,b.]).x1 = f.x1 & (f|[.a,b.]).x = f.x
by A9,A20,A8,A3,XXREAL_1:1,FUNCT_1:47;
hence |. f.x1-f.x .| < r by A12,A19,A21;
end;
end;
hence
A22: f is_left_convergent_in x by A5,LIMFUNC2:7;
A23: for r be Real st 0 < r
ex s be Real st s < x &
for x1 be Real st s < x1 & x1 < x & x1 in dom(f|(].a,b.[))
holds |. (f|(].a,b.[)).x1 - f.x .| < r
proof
let r be Real;
assume 0 < r; then
consider s0 be Real such that
A24: s0 < x & for x1 be Real st s0 < x1 & x1 < x & x1 in dom f
holds |. f.x1-f.x .| < r by A11;
set s = max(s0,a);
for x1 be Real st s < x1 & x1 < x & x1 in dom(f|(].a,b.[))
holds |. (f|(].a,b.[)).x1 - f.x .| < r
proof
let x1 be Real;
assume that
A25: s < x1 and
A26: x1 < x and
A27: x1 in dom(f|(].a,b.[));
s0 <= s by XXREAL_0:25; then
A28: s0 < x1 by A25,XXREAL_0:2;
x1 in dom f by A27,RELAT_1:57; then
|. f.x1-f.x .| < r by A24,A28,A26;
hence |. (f|(].a,b.[)).x1 - f.x .| < r by A27,FUNCT_1:47;
end;
hence thesis by A24,A4,XXREAL_0:29;
end;
A29: f|(].a,b.[) is_left_convergent_in x &
lim_left(f|(].a,b.[),x) = lim_left(f,x) by A4,A22,A10,Th9;
thus lim_left(f|(].a,b.[),x) = f.x by A23,A29,LIMFUNC2:41;
end;
theorem Th12:
for x be Real, f be PartFunc of REAL,REAL, I be non empty Interval,
X be Subset of REAL st I c= X & x in I & x <> sup I holds
f is_right_differentiable_in x iff f|X is_right_differentiable_in x
proof
let x be Real, f be PartFunc of REAL,REAL, I be non empty Interval,
X be Subset of REAL;
assume that
A1: I c= X and
A2: x in I and
A3: x <> sup I;
f|I c= f|X by A1,RELAT_1:75; then
A4: dom(f|I) c= dom(f|X) by RELAT_1:11;
A5: dom(f|X) c= dom f by RELAT_1:60;
hereby assume A6: f is_right_differentiable_in x; then
f|I is_right_differentiable_in x by A2,A3,FDIFF_12:4; then
consider r be Real such that
A7: r > 0 & [.x,x+r.] c= dom(f|I) by FDIFF_3:def 3;
A8: [.x,x+r.] c= dom(f|X) by A4,A7;
x < x+r by A7,XREAL_1:29; then
A9: x in dom(f|X) by A8,XXREAL_1:1;
for h,c st rng c = {x} & rng(h+c) c= dom(f|X) &
(for n be Nat holds h.n > 0) holds
h"(#)((f|X)/*(h+c) - (f|X)/*c) is convergent
proof
let h,c;
assume that
A10: rng c = {x} and
A11: rng(h+c) c= dom(f|X) and
A12: for n be Nat holds h.n > 0;
A13: (f|X)/*c = f/*c & (f|X)/*(h+c) = f/*(h+c)
by A11,A9,A10,ZFMISC_1:31,FUNCT_2:117;
rng(h+c) c= dom f by A11,A5;
hence h"(#)((f|X)/*(h+c) - (f|X)/*c) is convergent
by A13,A10,A12,A6,FDIFF_3:def 3;
end;
hence f|X is_right_differentiable_in x by A7,A8,FDIFF_3:def 3;
end;
assume f|X is_right_differentiable_in x; then
(f|X)|I is_right_differentiable_in x by A2,A3,FDIFF_12:4; then
f|I is_right_differentiable_in x by A1,RELAT_1:74;
hence f is_right_differentiable_in x by FDIFF_12:9;
end;
theorem Th13:
for x be Real, f be PartFunc of REAL,REAL, I be non empty Interval,
X be Subset of REAL st I c= X & x in I & x <> inf I holds
f is_left_differentiable_in x iff f|X is_left_differentiable_in x
proof
let x be Real, f be PartFunc of REAL,REAL, I be non empty Interval,
X be Subset of REAL;
assume that
A1: I c= X and
A2: x in I and
A3: x <> inf I;
f|I c= f|X by A1,RELAT_1:75; then
A4: dom(f|I) c= dom(f|X) by RELAT_1:11;
A5: dom(f|X) c= dom f by RELAT_1:60;
hereby assume A6: f is_left_differentiable_in x; then
f|I is_left_differentiable_in x by A2,A3,FDIFF_12:5; then
consider r be Real such that
A7: r > 0 & [.x-r,x.] c= dom(f|I) by FDIFF_3:def 4;
A8: [.x-r,x.] c= dom(f|X) by A4,A7;
x-r < x by A7,XREAL_1:44; then
A9: x in dom(f|X) by A8,XXREAL_1:1;
for h,c st rng c = {x} & rng(h+c) c= dom(f|X) &
(for n be Nat holds h.n < 0) holds
h"(#)((f|X)/*(h+c) - (f|X)/*c) is convergent
proof
let h,c;
assume that
A10: rng c = {x} and
A11: rng(h+c) c= dom(f|X) and
A12: for n be Nat holds h.n < 0;
A13: (f|X)/*c = f/*c & (f|X)/*(h+c) = f/*(h+c)
by A11,A9,A10,ZFMISC_1:31,FUNCT_2:117;
rng(h+c) c= dom f by A11,A5;
hence h"(#)((f|X)/*(h+c) - (f|X)/*c) is convergent
by A13,A10,A12,A6,FDIFF_3:def 4;
end;
hence f|X is_left_differentiable_in x by A7,A8,FDIFF_3:def 4;
end;
assume
f|X is_left_differentiable_in x; then
(f|X)|I is_left_differentiable_in x by A2,A3,FDIFF_12:5; then
f|I is_left_differentiable_in x by A1,RELAT_1:74;
hence f is_left_differentiable_in x by FDIFF_12:10;
end;
theorem Th14:
for f be PartFunc of REAL,REAL, I be open Subset of REAL,
X be Subset of REAL st I c= X holds
f is_differentiable_on I iff f|X is_differentiable_on I
proof
let f be PartFunc of REAL,REAL, I be open Subset of REAL,
X be Subset of REAL;
assume
A1: I c= X;
A2: dom(f|X) = dom f /\ X by RELAT_1:61;
hereby assume A3: f is_differentiable_on I;
now let x be Real;
assume x in I; then
f|I is_differentiable_in x by A3;
hence (f|X)|I is_differentiable_in x by A1,RELAT_1:74;
end;
hence f|X is_differentiable_on I by A1,A3,A2,XBOOLE_1:19;
end;
assume A4: f|X is_differentiable_on I;
now let x be Real;
assume x in I; then
(f|X)|I is_differentiable_in x by A4;
hence f|I is_differentiable_in x by A1,RELAT_1:74;
end;
hence f is_differentiable_on I by A4,A2,XBOOLE_1:18;
end;
theorem Th15:
for f be PartFunc of REAL,REAL, I be non empty Interval,
X be Subset of REAL st
I c= X holds
f is_differentiable_on_interval I iff f|X is_differentiable_on_interval I
proof
let f be PartFunc of REAL,REAL, I be non empty Interval,
X be Subset of REAL;
assume
A1: I c= X;
reconsider J = ].inf I,sup I.[ as open Subset of REAL by FDIFF_12:2;
J c= I by FDIFF_12:2; then
A2: J c= X by A1;
hereby assume f is_differentiable_on_interval I; then
A3: I c= dom f & inf I < sup I &
(inf I in I implies f is_right_differentiable_in lower_bound I) &
(sup I in I implies f is_left_differentiable_in upper_bound I) &
f is_differentiable_on ].inf I,sup I.[ by FDIFF_12:def 1;
dom(f|X) = dom f /\ X by RELAT_1:61; then
A4: I c= dom(f|X) by A1,A3,XBOOLE_1:19;
A5: now assume
A6: inf I in I; then
inf I = lower_bound I by Th1;
hence f|X is_right_differentiable_in lower_bound I
by A1,A6,A3,Th12;
end;
A7: now assume
A8: sup I in I; then
sup I = upper_bound I by Th2;
hence f|X is_left_differentiable_in upper_bound I
by A1,A8,A3,Th13;
end;
f|X is_differentiable_on J by A3,A2,Th14;
hence f|X is_differentiable_on_interval I by A3,A4,A5,A7,FDIFF_12:def 1;
end;
assume f|X is_differentiable_on_interval I; then
A9: I c= dom(f|X) & inf I < sup I &
(inf I in I implies f|X is_right_differentiable_in lower_bound I) &
(sup I in I implies f|X is_left_differentiable_in upper_bound I) &
f|X is_differentiable_on ].inf I,sup I.[ by FDIFF_12:def 1;
dom(f|X) = dom f /\ X by RELAT_1:61; then
A10: I c= dom f & I c= X by A9,XBOOLE_1:18;
A11: now assume A12: inf I in I; then
inf I = lower_bound I by Th1;
hence f is_right_differentiable_in lower_bound I
by A9,A10,A12,Th12;
end;
A13: now assume A14: sup I in I; then
sup I = upper_bound I by Th2;
hence f is_left_differentiable_in upper_bound I
by A9,A10,A14,Th13;
end;
f is_differentiable_on ].inf I,sup I.[ by A9,A2,Th14;
hence f is_differentiable_on_interval I by A9,A10,A11,A13,FDIFF_12:def 1;
end;
theorem Th16:
for f be PartFunc of REAL,REAL, I be non empty Interval,
X be Subset of REAL st
I c= X & f is_differentiable_on_interval I holds f`\I = (f|X)`\I
proof
let f be PartFunc of REAL,REAL, I be non empty Interval,
X be Subset of REAL;
assume that
A1: I c= X and
A2: f is_differentiable_on_interval I;
A3: f|X is_differentiable_on_interval I by A1,A2,Th15;
A4: f|I is_differentiable_on_interval I by A2,Th15;
A5: (f|X)|I is_differentiable_on_interval I by A3,Th15;
A6: dom(f`\I) = I & dom((f|X)`\I) = I by A2,A3,FDIFF_12:def 2;
now let x be Element of REAL;
assume
A7: x in dom(f`\I);
per cases;
suppose
A8: x = inf I; then
A9: x = lower_bound I by A6,A7,Th1;
A10: f|I is_right_differentiable_in x by A4,A6,A7,A8,A9,FDIFF_12:def 1;
(f`\I).x = Rdiff(f,x) by A2,A6,A7,A8,FDIFF_12:def 2; then
A11: (f`\I).x = Rdiff(f|I,x) by A10,FDIFF_12:9;
A12: (f|X)|I is_right_differentiable_in x by A5,A6,A7,A8,A9,FDIFF_12:def 1;
((f|X)`\I).x = Rdiff(f|X,x) by A3,A6,A7,A8,FDIFF_12:def 2; then
((f|X)`\I).x = Rdiff(((f|X)|I),x) by A12,FDIFF_12:9;
hence (f`\I).x = ((f|X)`\I).x by A11,A1,RELAT_1:74;
end;
suppose
A13: x = sup I; then
A14: x = upper_bound I by A6,A7,Th2;
A15: f|I is_left_differentiable_in x by A4,A6,A7,A13,A14,FDIFF_12:def 1;
(f`\I).x = Ldiff(f,x) by A2,A6,A7,A13,FDIFF_12:def 2; then
A16: (f`\I).x = Ldiff(f|I,x) by A15,FDIFF_12:10;
A17: (f|X)|I is_left_differentiable_in x by A5,A6,A7,A13,A14,FDIFF_12:def 1;
((f|X)`\I).x = Ldiff(f|X,x) by A3,A6,A7,A13,FDIFF_12:def 2; then
((f|X)`\I).x = Ldiff(((f|X)|I),x) by A17,FDIFF_12:10;
hence (f`\I).x = ((f|X)`\I).x by A16,A1,RELAT_1:74;
end;
suppose
A18: x <> inf I & x <> sup I;
reconsider J = ].inf I,sup I.[ as open Subset of REAL by FDIFF_12:2;
J c= I by FDIFF_12:2; then
A19: J c= X by A1;
A20: x in J by A6,A7,A18,FDIFF_12:3;
f is_differentiable_on J by A2,FDIFF_12:def 1; then
f|J is_differentiable_in x by A6,A7,A18,FDIFF_12:3; then
f is_differentiable_in x by A20,PDIFFEQ1:2; then
A21: diff(f,x) = diff(f|J,x) by A20,PDIFFEQ1:2;
f|X is_differentiable_on J by A3,FDIFF_12:def 1; then
(f|X)|J is_differentiable_in x by A6,A7,A18,FDIFF_12:3; then
f|X is_differentiable_in x by A20,PDIFFEQ1:2; then
diff(f|X,x) = diff((f|X)|J,x) by A20,PDIFFEQ1:2; then
A22: diff(f|X,x) = diff(f|J,x) by A19,RELAT_1:74;
(f`\I).x = diff(f,x) by A2,A6,A7,A18,FDIFF_12:def 2;
hence (f`\I).x = ((f|X)`\I).x by A21,A22,A3,A6,A7,A18,FDIFF_12:def 2;
end;
end;
hence f`\I = (f|X)`\I by A6,PARTFUN1:5;
end;
theorem Th17:
for f be PartFunc of REAL,REAL, I,J be non empty Interval st
f is_differentiable_on_interval I & J c= I & inf J < sup J holds
(f`\I)|J = (f`\J)
proof
let f be PartFunc of REAL,REAL, I,J be non empty Interval;
assume that
A1: f is_differentiable_on_interval I and
A2: J c= I and
A3: inf J < sup J;
f is_differentiable_on_interval J by A1,A2,A3,FDIFF_12:38; then
A4: dom(f`\I) = I & dom(f`\J) = J by A1,FDIFF_12:def 2;
for x be Element of REAL st x in dom((f`\I)|J) holds
((f`\I)|J).x = (f`\J).x
proof
let x be Element of REAL;
assume A5: x in dom((f`\I)|J); then
((f`\I)|J).x = (f`\I).x by FUNCT_1:47;
hence ((f`\I)|J).x = (f`\J).x by A1,A2,A3,A5,FDIFF_12:38;
end;
hence (f`\I)|J = (f`\J) by A4,A2,RELAT_1:62,PARTFUN1:5;
end;
begin :: Generalization of previous theorems
theorem Th18: ::: generalized XREAL_1:5
for a,b be R_eal st a < b ex c be Real st a < c & c < b
proof
let a,b be R_eal;
assume A1: a < b;
per cases;
suppose A2: a in REAL; then
A3: b in REAL or b = +infty by A1,XXREAL_0:10;
now assume A4: b = +infty;
consider c be Real such that
A5: a < c by A2,XREAL_1:1;
c in REAL by XREAL_0:def 1;
hence ex c be Real st a < c & c < b by A5,A4,XXREAL_0:9;
end;
hence thesis by A3,A1,A2,XREAL_1:5;
end;
suppose A6: b in REAL; then
A7: a in REAL or a = -infty by A1,XXREAL_0:13;
now assume A8: a = -infty;
consider c be Real such that
A9: c < b by A6,XREAL_1:2;
c in REAL by XREAL_0:def 1;
hence ex c be Real st a < c & c < b by A9,A8,XXREAL_0:12;
end;
hence thesis by A7,A1,A6,XREAL_1:5;
end;
suppose not a in REAL & not b in REAL; then
a = +infty or a = -infty &
b = +infty or b = -infty by XXREAL_0:14; then
a < 0 & 0 < b by A1,XXREAL_0:4,6;
hence ex c be Real st a < c & c < b;
end;
end;
theorem Th19: ::: generalized ROLLE:7
for p,q be R_eal for f be PartFunc of REAL,REAL
st f is_differentiable_on ].p,q.[ &
(for x be Real st x in ].p,q.[ holds diff(f,x) = 0) holds
f|(].p,q.[) is constant
proof
let p,q be R_eal, f be PartFunc of REAL,REAL;
assume that
A1: f is_differentiable_on ].p,q.[ and
A2: for x be Real st x in ].p,q.[ holds diff(f,x) = 0;
now let x1,x2 be Element of REAL;
assume x1 in ].p,q.[ /\ dom f & x2 in ].p,q.[ /\ dom f; then
A3: x1 in ].p,q.[ & x2 in ].p,q.[ by XBOOLE_0:def 4;
now per cases by XXREAL_0:1;
suppose x1=x2;
hence f.x1=f.x2;
end;
suppose
A4: x1<x2; then
0<>x2-x1; then
A5: 0<>(x2-x1)" by XCMPLX_1:202;
reconsider Z=].x1,x2.[ as open Subset of REAL;
A6: [.x1,x2.] c= ].p,q.[ by A3,XXREAL_2:def 12; then
A7: f|[.x1,x2.] is continuous by A1,FDIFF_1:25,FCONT_1:16;
A8: Z c= [.x1,x2.] by XXREAL_1:25; then
f is_differentiable_on Z by A1,A6,FDIFF_1:26,XBOOLE_1:1; then
A9: ex x0 be Real st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1)
by A1,A4,A6,A7,ROLLE:3,XBOOLE_1:1;
Z c= ].p,q.[ by A6,A8; then
0 = (f.x2-f.x1) by A2,A5,A9,XCMPLX_1:6;
hence f.x1=f.x2;
end;
suppose
A10: x2<x1; then
0<>x1-x2; then
A11: 0<>(x1-x2)" by XCMPLX_1:202;
reconsider Z=].x2,x1.[ as open Subset of REAL;
A12: [.x2,x1.] c= ].p,q.[ by A3,XXREAL_2:def 12; then
A13: f|[.x2,x1.] is continuous by A1,FDIFF_1:25,FCONT_1:16;
A14: Z c= [.x2,x1.] by XXREAL_1:25; then
f is_differentiable_on Z by A1,A12,FDIFF_1:26,XBOOLE_1:1; then
A15: ex x0 be Real st x0 in ].x2,x1.[ & diff(f,x0) = (f.x1-f.x2)/(x1- x2)
by A1,A10,A12,A13,ROLLE:3,XBOOLE_1:1;
Z c= ].p,q.[ by A12,A14; then
0 = (f.x1-f.x2) by A2,A11,A15,XCMPLX_1:6;
hence f.x1=f.x2;
end;
end;
hence f.x1=f.x2;
end;
hence thesis by PARTFUN2:58;
end;
theorem Th20: ::: generalized ROLLE:8
for p,q be R_eal, f1,f2 be PartFunc of REAL,REAL
st f1 is_differentiable_on ].p,q.[ & f2 is_differentiable_on ].p,q.[ &
(for x be Real st x in ].p,q.[ holds diff(f1,x) = diff(f2,x)) holds
(f1-f2)|(].p,q.[) is constant &
ex r be Real st for x be Real st x in ].p,q.[ holds f1.x = f2.x+r
proof
let p,q be R_eal, f1,f2 be PartFunc of REAL,REAL;
assume that
A1: f1 is_differentiable_on ].p,q.[ & f2 is_differentiable_on ].p,q.[ and
A2: for x be Real st x in ].p,q.[ holds diff(f1,x) = diff(f2,x);
].p,q.[ is open_interval by MEASURE5:def 2; then
reconsider Z=].p,q.[ as open Subset of REAL;
].p,q.[ c= dom f1 /\ dom f2 by A1,XBOOLE_1:19; then
A3: ].p,q.[ c= dom (f1-f2) by VALUED_1:12; then
A4: f1-f2 is_differentiable_on Z by A1,FDIFF_1:19;
now let x be Real;
assume
A5: x in ].p,q.[; then
diff(f1-f2,x) = ((f1-f2)`|Z).x by A4,FDIFF_1:def 7; then
diff(f1-f2,x) = diff(f1,x)-diff(f2,x) by A1,A3,A5,FDIFF_1:19; then
diff(f1-f2,x) = diff(f1,x)-diff(f1,x) by A2,A5;
hence diff(f1-f2,x) = 0;
end; then
A6: (f1-f2)|Z is constant by A1,A3,Th19,FDIFF_1:19;
hence (f1-f2)|(].p,q.[) is constant;
consider r being Element of REAL such that
A7: for x being Element of REAL st x in ].p,q.[ /\ dom(f1-f2) holds
(f1-f2).x = r by A6,PARTFUN2:57;
take r;
let x be Real;
assume
A8: x in ].p,q.[; then
x in ].p,q.[ /\ dom(f1-f2) by A3,XBOOLE_1:28; then
r = (f1-f2).x by A7; then
r = f1.x - f2.x by A3,A8,VALUED_1:13;
hence thesis;
end;
theorem ::: generalized ROLLE:9
for p,q be R_eal, f be PartFunc of REAL,REAL st
f is_differentiable_on ].p,q.[
& (for x be Real st x in ].p,q.[ holds 0<diff(f,x)) holds
f|(].p,q.[) is increasing
proof
let p,q be R_eal, f be PartFunc of REAL,REAL;
assume that
A1: f is_differentiable_on ].p,q.[ and
A2: for x be Real st x in ].p,q.[ holds 0<diff(f,x);
now let x1,x2 be Real;
assume that
A3: x1 in ].p,q.[ /\ dom f & x2 in ].p,q.[ /\ dom f and
A4: x1<x2;
A5: 0 < x2-x1 by A4,XREAL_1:50;
reconsider Z=].x1,x2.[ as open Subset of REAL;
x1 in ].p,q.[ & x2 in ].p,q.[ by A3,XBOOLE_0:def 4; then
A6: [.x1,x2.] c= ].p,q.[ by XXREAL_2:def 12; then
A7: f|[.x1,x2.] is continuous by A1,FDIFF_1:25,FCONT_1:16;
A8: Z c= [.x1,x2.] by XXREAL_1:25; then
f is_differentiable_on Z by A1,A6,FDIFF_1:26,XBOOLE_1:1; then
ex x0 be Real st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1)
by A1,A4,A6,A7,ROLLE:3,XBOOLE_1:1; then
0<f.x2-f.x1 by A2,A5,A6,A8; then
f.x1+0<f.x2 by XREAL_1:20;
hence f.x1<f.x2;
end;
hence thesis by RFUNCT_2:20;
end;
theorem ::: generalized ROLLE:10
for p,q be R_eal, f be PartFunc of REAL,REAL st
f is_differentiable_on ].p,q.[
& (for x be Real st x in ].p,q.[ holds diff(f,x)<0) holds
f|(].p,q.[) is decreasing
proof
let p,q be R_eal, f be PartFunc of REAL,REAL;
assume that
A1: f is_differentiable_on ].p,q.[ and
A2: for x be Real st x in ].p,q.[ holds diff(f,x)<0;
now let x1,x2 be Real;
assume that
A3: x1 in ].p,q.[ /\ dom f & x2 in ].p,q.[ /\ dom f and
A4: x1 < x2;
A5: 0 < x2-x1 by A4,XREAL_1:50;
reconsider Z=].x1,x2.[ as open Subset of REAL;
x1 in ].p,q.[ & x2 in ].p,q.[ by A3,XBOOLE_0:def 4; then
A6: [.x1,x2.] c= ].p,q.[ by XXREAL_2:def 12; then
A7: f|[.x1,x2.] is continuous by A1,FDIFF_1:25,FCONT_1:16;
A8: Z c= [.x1,x2.] by XXREAL_1:25; then
f is_differentiable_on Z by A1,A6,FDIFF_1:26,XBOOLE_1:1; then
ex x0 be Real st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1)
by A1,A4,A6,A7,ROLLE:3,XBOOLE_1:1; then
f.x2-f.x1<0 by A2,A5,A6,A8; then
f.x2<f.x1+0 by XREAL_1:19;
hence f.x2<f.x1;
end;
hence thesis by RFUNCT_2:21;
end;
theorem ::: generalized ROLLE:11
for p,q be R_eal, f be PartFunc of REAL,REAL st
f is_differentiable_on ].p,q.[
& (for x be Real st x in ].p,q.[ holds 0<=diff(f,x)) holds
f|(].p,q.[) is non-decreasing
proof
let p,q be R_eal, f be PartFunc of REAL,REAL;
assume that
A1: f is_differentiable_on ].p,q.[ and
A2: for x be Real st x in ].p,q.[ holds 0<=diff(f,x);
now let x1,x2 be Real;
assume that
A3: x1 in ].p,q.[ /\ dom f & x2 in ].p,q.[ /\ dom f and
A4: x1 < x2;
A5: 0 <> x2-x1 by A4;
reconsider Z=].x1,x2.[ as open Subset of REAL;
x1 in ].p,q.[ & x2 in ].p,q.[ by A3,XBOOLE_0:def 4; then
A6: [.x1,x2.] c= ].p,q.[ by XXREAL_2:def 12; then
A7: f|[.x1,x2.] is continuous by A1,FDIFF_1:25,FCONT_1:16;
A8: Z c= [.x1,x2.] by XXREAL_1:25; then
f is_differentiable_on Z by A1,A6,FDIFF_1:26,XBOOLE_1:1; then
ex x0 be Real st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1)
by A1,A4,A6,A7,ROLLE:3,XBOOLE_1:1; then
A9: 0 <= (f.x2-f.x1)/(x2-x1) by A2,A8,A6;
0 <= x2-x1 by A4,XREAL_1:50; then
0*(x2-x1) <= (f.x2-f.x1)/(x2-x1)*(x2-x1) by A9; then
0 <= f.x2-f.x1 by A5,XCMPLX_1:87; then
f.x1+0 <= f.x2 by XREAL_1:19;
hence f.x1<=f.x2;
end;
hence thesis by RFUNCT_2:22;
end;
theorem ::: generalized ROLLE:12
for p,q be R_eal, f be PartFunc of REAL,REAL st
f is_differentiable_on ].p,q.[
& (for x be Real st x in ].p,q.[ holds diff(f,x)<=0) holds
f|(].p,q.[) is non-increasing
proof
let p,q be R_eal, f be PartFunc of REAL,REAL;
assume that
A1: f is_differentiable_on ].p,q.[ and
A2: for x be Real st x in ].p,q.[ holds diff(f,x)<=0;
now let x1,x2 be Real;
assume that
A3: x1 in ].p,q.[ /\ dom f & x2 in ].p,q.[ /\ dom f and
A4: x1 < x2;
A5: 0 <= x2-x1 by A4,XREAL_1:50;
reconsider Z=].x1,x2.[ as open Subset of REAL;
x1 in ].p,q.[ & x2 in ].p,q.[ by A3,XBOOLE_0:def 4; then
A6: [.x1,x2.] c= ].p,q.[ by XXREAL_2:def 12; then
A7: f|[.x1,x2.] is continuous by A1,FDIFF_1:25,FCONT_1:16;
A8: Z c= [.x1,x2.] by XXREAL_1:25; then
f is_differentiable_on Z by A1,A6,FDIFF_1:26,XBOOLE_1:1; then
A9: ex x0 be Real st x0 in ].x1,x2.[ & diff(f,x0) = (f.x2-f.x1)/(x2- x1)
by A1,A4,A6,A7,ROLLE:3,XBOOLE_1:1;
A10: 0 <> x2-x1 by A4;
Z c= ].p,q.[ by A6,A8; then
(f.x2-f.x1)/(x2-x1)*(x2-x1)<=0*(x2-x1) by A2,A5,A9,XREAL_1:64; then
f.x2-f.x1<=0 by A10,XCMPLX_1:87; then
f.x2<=f.x1+0 by XREAL_1:20;
hence f.x2<=f.x1;
end;
hence thesis by RFUNCT_2:23;
end;
theorem
for X be open Subset of REAL, x0 be Real, f be PartFunc of REAL,REAL st
x0 in X & f is_differentiable_on X holds diff(f,x0) = diff(f|X,x0)
proof
let X be open Subset of REAL, x0 be Real, f be PartFunc of REAL,REAL;
assume that
A1: x0 in X and
A2: f is_differentiable_on X;
A3: f|X is_differentiable_in x0 by A1,A2; then
A4: f is_differentiable_in x0 by A1,PDIFFEQ1:2;
consider N be Neighbourhood of x0 such that
A5: N c= dom(f|X) &
ex L be LinearFunc, R be RestFunc st diff(f|X,x0) = L.1
& for x be Real st x in N holds (f|X).x-(f|X).x0 = L.(x-x0)+R.(x-x0)
by A3,FDIFF_1:def 5;
consider L be LinearFunc, R be RestFunc such that
A6: diff(f|X,x0) = L.1 &
for x be Real st x in N holds (f|X).x-(f|X).x0 = L.(x-x0)+R.(x-x0)
by A5;
dom(f|X) c= dom f by RELAT_1:60; then
A7: N c= dom f by A5;
for x be Real st x in N holds f.x - f.x0 = L.(x-x0)+R.(x-x0)
proof
let x be Real;
assume A8: x in N; then
x in dom(f|X) by A5; then
(f|X).x = f.x & (f|X).x0 = f.x0 by A1,FUNCT_1:49;
hence thesis by A6,A8;
end;
hence diff(f,x0) = diff(f|X,x0) by A6,A4,A7,FDIFF_1:def 5;
end;
theorem Th26: ::: generalized INTEGRA6:29
for a,b be Real, f be PartFunc of REAL,REAL st a < b & [.a,b.] c= dom f &
f|[.a,b.] is continuous
ex F be PartFunc of REAL,REAL st ].a,b.[ c= dom F &
(for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x)) &
F is_differentiable_on ].a,b.[ & F`|(].a,b.[) = f|(].a,b.[)
proof
let a,b be Real, f be PartFunc of REAL,REAL;
assume that
A1: a < b and
A2: [.a,b.] c= dom f and
A3: f|[.a,b.] is continuous;
consider x0 be Real such that
A4: a < x0 & x0 < b by A1,XREAL_1:5;
A5: x0 in ].a,b.[ by A4,XXREAL_1:4;
A6: [.a,b.] = ['a,b'] by A1,INTEGRA5:def 3; then
A7: f|['a,b'] is bounded by A2,A3,INTEGRA5:10;
a in ['a,b'] & b in ['a,b'] by A1,A6,XXREAL_1:1; then
A8: inf ['a,b'] <= a & b <= sup ['a,b'] by XXREAL_2:3,4;
A9: f is_integrable_on ['a,b'] by A2,A3,A6,INTEGRA5:11; then
consider F be PartFunc of REAL,REAL such that
A10: ].a,b.[ c= dom F &
(for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x)) &
F is_differentiable_in x0 & diff(F,x0) = f.x0
by A1,A7,A2,A6,A5,A3,A8,Th6,INTEGRA6:29;
for x be Real st x in ].a,b.[ holds F|(].a,b.[) is_differentiable_in x
proof
let x be Real;
assume
A11: x in ].a,b.[; then
f is_continuous_in x by A2,A3,A6,A8,Th6; then
F is_differentiable_in x by A1,A9,A7,A2,A6,A10,A11,INTEGRA6:28;
hence thesis by A11,PDIFFEQ1:2;
end; then
A12:F is_differentiable_on ].a,b.[ by A10; then
A13:dom(F`|(].a,b.[)) = ].a,b.[ by FDIFF_1:def 7;
].a,b.[ c= [.a,b.] by XXREAL_1:25; then
].a,b.[ c= dom f by A2; then
A14:dom(f|(].a,b.[)) = ].a,b.[ by RELAT_1:62;
for x be Element of REAL st x in dom(F`|(].a,b.[)) holds
(F`|(].a,b.[)).x = (f|(].a,b.[)).x
proof
let x be Element of REAL;
assume
A15: x in dom(F`|(].a,b.[)); then
A16: f is_continuous_in x by A2,A3,A13,A6,A8,Th6;
(F`|(].a,b.[)).x = diff(F,x) by A12,A13,A15,FDIFF_1:def 7; then
(F`|(].a,b.[)).x = f.x by A1,A9,A7,A2,A6,A10,A15,A13,A16,INTEGRA6:28;
hence (F`|(].a,b.[)).x = (f|(].a,b.[)).x by A15,A13,A14,FUNCT_1:47;
end;
hence thesis by A10,A12,A13,A14,PARTFUN1:5;
end;
theorem Th27: ::: generalized INTEGRA6:28
for a,b be Real, f,F be PartFunc of REAL,REAL st
a < b & [.a,b.] c= dom f & f|[.a,b.] is continuous & ].a,b.[ c= dom F &
(for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x)) holds
F is_differentiable_on ].a,b.[ & F`|(].a,b.[) = f|(].a,b.[)
proof
let a,b be Real, f,F be PartFunc of REAL,REAL;
assume that
A1: a < b and
A2: [.a,b.] c= dom f and
A3: f|[.a,b.] is continuous and
A4: ].a,b.[ c= dom F and
A5: for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x);
consider G be PartFunc of REAL,REAL such that
A6: ].a,b.[ c= dom G &
(for x be Real st x in ].a,b.[ holds G.x = integral(f,a,x)) &
G is_differentiable_on ].a,b.[ & G`|(].a,b.[) = f|(].a,b.[)
by A1,A2,A3,Th26;
A7: dom(F|(].a,b.[)) = ].a,b.[ & dom(G|(].a,b.[)) = ].a,b.[
by A4,A6,RELAT_1:62;
for x be Element of REAL st x in dom(F|(].a,b.[)) holds
(F|(].a,b.[)).x = (G|(].a,b.[)).x
proof
let x be Element of REAL;
assume A8: x in dom(F|(].a,b.[)); then
(F|(].a,b.[)).x = F.x by FUNCT_1:47; then
(F|(].a,b.[)).x = integral(f,a,x) by A5,A7,A8; then
(F|(].a,b.[)).x = G.x by A6,A7,A8;
hence thesis by A7,A8,FUNCT_1:47;
end; then
A9: F|(].a,b.[) = G|(].a,b.[) by A7,PARTFUN1:5;
hence F is_differentiable_on ].a,b.[ by A4,A6; then
F`|(].a,b.[) = (F|(].a,b.[))`|(].a,b.[) by PDIFFEQ1:4;
hence F`|(].a,b.[) = f|(].a,b.[) by A6,A9,PDIFFEQ1:4;
end;
begin :: Antiderivatives and related theorems
definition
let f,F be PartFunc of REAL,REAL, I be non empty Interval;
pred F is_antiderivative_of f,I means :Def1:
F is_differentiable_on_interval I & F`\I = f|I;
end;
theorem :: corresponds to INTEGRA7:12
for f,F,g,G be PartFunc of REAL,REAL, I be non empty Interval st
F is_antiderivative_of f,I & G is_antiderivative_of g,I
holds F+G is_antiderivative_of f+g,I & F-G is_antiderivative_of f-g,I
proof
let f,F,g,G be PartFunc of REAL,REAL, I be non empty Interval;
assume that
A1: F is_antiderivative_of f,I and
A2: G is_antiderivative_of g,I;
I c= dom F & I c= dom G by A1,A2,FDIFF_12:def 1; then
I c= dom F /\ dom G by XBOOLE_1:19; then
A3: I c= dom(F+G) & I c= dom(F-G) by VALUED_1:def 1,12; then
(F+G)`\I = F`\I + G`\I & (F-G)`\I = F`\I - G`\I by A2,A1,FDIFF_12:19,20;
hence thesis by A3,A1,A2,RFUNCT_1:44,47,FDIFF_12:19,20;
end;
theorem :: corresponds to INTEGRA7:13
for f,F be PartFunc of REAL,REAL, I be non empty Interval, r be Real st
F is_antiderivative_of f,I holds r(#)F is_antiderivative_of r(#)f,I
proof
let f,F be PartFunc of REAL,REAL, I be non empty Interval, r be Real;
assume A1: F is_antiderivative_of f,I; then
r(#)F is_differentiable_on_interval I &
(r(#)F)`\I = r(#)(F`\I) by FDIFF_12:23;
hence r(#)F is_antiderivative_of r(#)f,I by A1,RFUNCT_1:49;
end;
theorem :: corresponds to INTEGRA7:14
for f,g,F,G be PartFunc of REAL,REAL, I be non empty Interval st
F is_antiderivative_of f,I & G is_antiderivative_of g,I holds
F(#)G is_antiderivative_of f(#)G+F(#)g,I
proof
let f,g,F,G be PartFunc of REAL,REAL, I be non empty Interval;
assume that
A1: F is_antiderivative_of f,I and
A2: G is_antiderivative_of g,I;
A3: (F(#)G)`\I = G(#)(F`\I) + F(#)(G`\I) by A1,A2,FDIFF_12:24;
G(#)(F`\I) = (G(#)f)|I & F(#)(G`\I) = (F(#)g)|I by A1,A2,RFUNCT_1:45;
hence F(#)G is_antiderivative_of f(#)G+F(#)g,I
by A3,A1,A2,FDIFF_12:24,RFUNCT_1:44;
end;
theorem :: corresponds to INTEGRA7:15
for f,g,F,G be PartFunc of REAL,REAL, I be non empty Interval st
F is_antiderivative_of f,I & G is_antiderivative_of g,I &
(for x be set st x in I holds G.x <> 0) holds
F/G is_antiderivative_of (f(#)G-F(#)g)/(G(#)G),I
proof
let f,g,F,G be PartFunc of REAL,REAL, I be non empty Interval;
assume that
A1: F is_antiderivative_of f,I and
A2: G is_antiderivative_of g,I and
A3: for x be set st x in I holds G.x <> 0;
A4: I c= dom F & I c= dom G by A1,A2,FDIFF_12:def 1;
A5: dom(F/G) = dom F /\ (dom G \ G"{0}) by RFUNCT_1:def 1;
now let x be set;
assume A6: x in I; then
G.x <> 0 by A3; then
not G.x in {0} by TARSKI:def 1; then
not x in G"{0} by FUNCT_1:def 7; then
x in dom G \ G"{0} by A4,A6,XBOOLE_0:def 5;
hence x in dom(F/G) by A4,A5,A6,XBOOLE_0:def 4;
end; then
A7: I c= dom(F/G); then
A8:(F/G)`\I = ((F`\I)(#)G - (G`\I)(#)F)/(G^2) by A1,A2,FDIFF_12:25;
(F`\I)(#)G = (f(#)G)|I & (G`\I)(#)F = (g(#)F)|I by A1,A2,RFUNCT_1:45; then
(F`\I)(#)G - (G`\I)(#)F = (f(#)G - g(#)F)|I by RFUNCT_1:47;
hence F/G is_antiderivative_of (f(#)G-F(#)g)/(G(#)G),I
by A7,A8,A1,A2,FDIFF_12:25,RFUNCT_1:48;
end;
theorem Th32:
for a,b be Real, f,F be PartFunc of REAL,REAL st
a <= b & [.a,b.] c= dom f & f|[.a,b.] is continuous & [.a,b.] c= dom F &
(for x be Real st x in [.a,b.] holds F.x = integral(f,a,x)) holds
for x be Real st x in ].a,b.[ holds
F is_differentiable_in x & diff(F,x) = f.x
proof
let a,b be Real, f,F be PartFunc of REAL,REAL;
set O = ].a,b.[;
assume that
A1: a <= b and
A2: [.a,b.] c= dom f and
A3: f|[.a,b.] is continuous and
A4: [.a,b.] c= dom F and
A5: for x be Real st x in [.a,b.] holds F.x = integral(f,a,x);
A6:['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
A7: O c= [.a,b.] by XXREAL_1:25; then
A8: dom(F|O) = O & dom(f|O) = O by A2,A4,XBOOLE_1:1,RELAT_1:62;
deffunc G0(Real) = In(integral(f,a,$1),REAL);
consider G1 be Function of REAL,REAL such that
A9: for h be Element of REAL holds G1.h=G0(h) from FUNCT_2:sch 4;
reconsider G=G1|O as PartFunc of REAL,REAL;
dom G1 = REAL by FUNCT_2:def 1; then
A10: dom G = O by RELAT_1:62;
A11:now let x be Real;
A12: x is Element of REAL by XREAL_0:def 1;
assume x in ].a,b.[; then
G.x = G1.x by A10,FUNCT_1:47; then
G.x = G0(x) by A9,A12;
hence G.x = integral(f,a,x);
end;
A13:now let x be Element of REAL;
assume
A14: x in dom(F|O);
(F|O).x = F.x by A14,FUNCT_1:47;
then (F|O).x = integral(f,a,x) by A5,A14,A7,A8;
hence (F|O).x = G.x by A11,A8,A14;
end;
A15: for x be Real st x in O holds G is_differentiable_in x & diff(G,x)=f.x
proof
let x be Real;
A16: f|O is continuous by A3,FCONT_1:16,XXREAL_1:25;
assume
A17: x in ]. a,b .[; then
a < x & x < b by XXREAL_1:4; then
a < b by XXREAL_0:2; then
A18: inf O = a & sup O = b by XXREAL_2:28,32;
].a,b.[ c= dom f by A7,A2; then
A19: f is_continuous_in x by A16,A17,A18,Th6;
f|[' a,b '] is bounded & f is_integrable_on [' a,b ']
by A2,A3,A6,INTEGRA5:10,11;
hence thesis by A1,A2,A10,A11,A6,A17,A19,INTEGRA6:28;
end;
A20: F|O = G by A8,A10,A13,PARTFUN1:5;
thus for x be Real st x in ].a,b.[ holds F is_differentiable_in x &
diff(F,x) = f.x
proof
let x be Real;
assume
A21: x in ].a,b.[; then
A22: G is_differentiable_in x & diff(G,x)=f.x by A15;
hence F is_differentiable_in x by A20,A21,PDIFFEQ1:2;
hence diff(F,x)=f.x by A20,A21,A22,PDIFFEQ1:2;
end;
end;
theorem Th33:
for a,b be Real, f,F be PartFunc of REAL,REAL st
a <= b & [.a,b.] c= dom f & f|['a,b'] is bounded &
f is_integrable_on ['a,b'] & [.a,b.] = dom F &
for x be Real st x in [.a,b.] holds F.x = integral(f,a,x)
holds F is Lipschitzian
proof
let a,b be Real, f,F be PartFunc of REAL,REAL;
assume that
A1: a <= b and
A2: [.a,b.] c= dom f and
A3: f|['a,b'] is bounded and
A4: f is_integrable_on ['a,b'] and
A5: [.a,b.] = dom F and
A6: for x be Real st x in [.a,b.] holds F.x = integral(f,a,x);
A7: [.a,b.] = ['a,b'] by A1,INTEGRA5:def 3;
consider r0 be Real such that
A8: for x be object st x in ['a,b'] /\ dom f holds |. f.x .| <= r0
by A3,RFUNCT_1:73;
reconsider r = max(r0,1) as Real;
A9: 0 < r by XXREAL_0:25;
A10: r0 <= r by XXREAL_0:25;
A11: for p,q be Real st p in [.a,b.] & q in [.a,b.] & p <= q holds
f is_integrable_on ['p,q'] & f|['p,q'] is bounded
proof
let p,q be Real;
assume A12: p in [.a,b.] & q in [.a,b.] & p <= q;
a <= p & q <= b by A12,XXREAL_1:1;
hence thesis by A2,A3,A4,A7,A12,INTEGRA6:18;
end;
for x1,x2 be Real st x1 in dom F & x2 in dom F holds
|. F.x1 - F.x2 .| <= r*|.x1-x2.|
proof
let x1,x2 be Real;
assume A13: x1 in dom F & x2 in dom F; then
F.x1 = integral(f,a,x1) & F.x2 = integral(f,a,x2) by A5,A6; then
A14: F.x1 = F.x2 + integral(f,x2,x1)
by A1,A4,A3,A2,A5,A7,A13,INTEGRA6:20;
per cases;
suppose A15: x1 <= x2; then
A16: f is_integrable_on ['x1,x2'] & f|['x1,x2'] is bounded by A5,A13,A11;
A17: [.x1,x2.] = ['x1,x2'] by A15,INTEGRA5:def 3;
A18: ['x1,x2'] c= [.a,b.] by A17,A5,A13,XXREAL_2:def 12; then
A19: ['x1,x2'] c= dom f by A2;
A20: x1 in ['x1,x2'] & x2 in ['x1,x2'] by A15,A17,XXREAL_1:1;
for x be Real st x in ['x1,x2'] holds |. f.x .| <= r
proof
let x be Real;
assume x in ['x1,x2']; then
x in [.a,b.] /\ dom f by A18,A19,XBOOLE_0:def 4; then
|. f.x .| <= r0 by A8,A7;
hence |. f.x .| <= r by A10,XXREAL_0:2;
end; then
|. F.x1 - F.x2 .| <= r * (x2-x1) by A14,A15,A16,A19,A20,INTEGRA6:23; then
|. F.x1 - F.x2 .| <= r * |.x2-x1.| by A15,XREAL_1:48,COMPLEX1:43;
hence |. F.x1 - F.x2 .| <= r*|.x1-x2.| by COMPLEX1:60;
end;
suppose A21: x2 <= x1; then
A22: f is_integrable_on ['x2,x1'] & f|['x2,x1'] is bounded by A5,A13,A11;
A23: [.x2,x1.] = ['x2,x1'] by A21,INTEGRA5:def 3;
A24: ['x2,x1'] c= [.a,b.] by A23,A5,A13,XXREAL_2:def 12; then
A25: ['x2,x1'] c= dom f by A2;
A26: x1 in ['x2,x1'] & x2 in ['x2,x1'] by A21,A23,XXREAL_1:1;
for x be Real st x in ['x2,x1'] holds |. f.x .| <= r
proof
let x be Real;
assume x in ['x2,x1']; then
x in [.a,b.] /\ dom f by A24,A25,XBOOLE_0:def 4; then
|. f.x .| <= r0 by A8,A7;
hence |. f.x .| <= r by A10,XXREAL_0:2;
end; then
|. F.x1 - F.x2 .| <= r * (x1-x2) by A14,A21,A22,A25,A26,INTEGRA6:23;
hence |. F.x1 - F.x2 .| <= r*|.x1-x2.| by A21,XREAL_1:48,COMPLEX1:43;
end;
end;
hence F is Lipschitzian by A9,FCONT_1:def 3;
end;
theorem Th34:
for a,b be Real, f,F be PartFunc of REAL,REAL st
a < b & [.a,b.] c= dom f & f|[.a,b.] is continuous & [.a,b.] c= dom F &
(for x be Real st x in [.a,b.] holds F.x = integral(f,a,x)) holds
F`|(].a,b.[) is_right_convergent_in a &
F`|(].a,b.[) is_left_convergent_in b
proof
let a,b be Real, f,F be PartFunc of REAL,REAL;
assume that
A1: a < b and
A2: [.a,b.] c= dom f and
A3: f|[.a,b.] is continuous and
A4: [.a,b.] c= dom F and
A5: for x be Real st x in [.a,b.] holds F.x = integral(f,a,x);
A6: [.a,b.] = ['a,b'] by A1,INTEGRA5:def 3;
A7: ].a,b.[ c= [.a,b.] by XXREAL_1:25; then
A8: ].a,b.[ c= dom f & ].a,b.[ c= dom F by A2,A4;
for x be Real st x in ].a,b.[ holds F|(].a,b.[) is_differentiable_in x
proof
let x be Real;
assume A9: x in ].a,b.[; then
F is_differentiable_in x by A1,A2,A3,A4,A5,Th32;
hence F|(].a,b.[) is_differentiable_in x by A9,PDIFFEQ1:2;
end; then
A10:F is_differentiable_on ].a,b.[ by A8; then
A11: dom(F`|(].a,b.[)) = ].a,b.[ by FDIFF_1:def 7;
A12: dom(f|(].a,b.[)) = ].a,b.[ by A8,RELAT_1:62;
for x be Element of REAL st x in dom(F`|(].a,b.[)) holds
(F`|(].a,b.[)).x = (f|(].a,b.[)).x
proof
let x be Element of REAL;
assume
A13: x in dom(F`|(].a,b.[)); then
(F`|(].a,b.[)).x = diff(F,x) by A11,A10,FDIFF_1:def 7; then
(F`|(].a,b.[)).x = f.x by A11,A13,A1,A2,A3,A4,A5,Th32;
hence (F`|(].a,b.[)).x = (f|(].a,b.[)).x by A11,A13,FUNCT_1:49;
end; then
A14: F`|(].a,b.[) = f|(].a,b.[) by A11,A12,PARTFUN1:5;
A15: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; then
A16: a in ['a,b'] & b in ['a,b'] by A1,XXREAL_1:1;
A17: for r be Real st a<r
ex g be Real st g < r & a < g & g in dom(F`|(].a,b.[))
proof
let r be Real;
assume a < r; then
consider g be Real such that
A18: a < g & g < min(r,b) by A1,XXREAL_0:21,XREAL_1:5;
take g;
min(r,b) <= r & min(r,b) <= b by XXREAL_0:17; then
g < r & g < b by A18,XXREAL_0:2;
hence thesis by A18,A11,XXREAL_1:4;
end;
for g1 be Real st 0 < g1
ex r be Real st a<r & for r1 be Real st
r1<r & a<r1 & r1 in dom(F`|(].a,b.[))
holds |. (F`|(].a,b.[)).r1 - f.a .| < g1
proof
let g1 be Real;
assume 0 < g1; then
consider s be Real such that
A19: 0 < s and
A20: for x1 be Real st x1 in ['a,b'] & |.x1-a.|<s holds
|.f.x1-f.a.| < g1 by A16,A2,A3,A15,FCONT_1:14;
take r = a+s;
thus a < r by A19,XREAL_1:29;
thus for r1 be Real st r1<r & a<r1 & r1 in dom(F`|(].a,b.[)) holds
|. (F`|(].a,b.[)).r1 - f.a .| < g1
proof
let r1 be Real;
assume that
A21: r1 < r and
A22: a < r1 and
A23: r1 in dom(F`|(].a,b.[));
0 < r1-a by A22,XREAL_1:50; then
A24: |. r1-a .| = r1-a by COMPLEX1:43;
r1-a < r-a by A21,XREAL_1:14; then
|. f.r1 - f.a .| < g1 by A6,A7,A11,A23,A20,A24;
hence |. (F`|(].a,b.[)).r1 - f.a .| < g1 by A14,A11,A23,FUNCT_1:49;
end;
end;
hence F`|(].a,b.[) is_right_convergent_in a by A17,LIMFUNC2:10;
A25: for r be Real st r<b
ex g be Real st r < g & g < b & g in dom(F`|(].a,b.[))
proof
let r be Real;
assume r < b; then
consider g be Real such that
A26: max(a,r) < g & g < b by A1,XXREAL_0:29,XREAL_1:5;
take g;
a <= max(a,r) & r <= max(a,r) by XXREAL_0:25; then
r < g & a < g by A26,XXREAL_0:2;
hence thesis by A26,A11,XXREAL_1:4;
end;
for g1 be Real st 0 < g1
ex r be Real st r<b & for r1 be Real st
r<r1 & r1<b & r1 in dom(F`|(].a,b.[))
holds |. (F`|(].a,b.[)).r1 - f.b .| < g1
proof
let g1 be Real;
assume 0 < g1; then
consider s be Real such that
A27: 0 < s and
A28: for x1 be Real st x1 in ['a,b'] & |.x1-b.|<s holds
|.f.x1-f.b.| < g1 by A16,A2,A3,A15,FCONT_1:14;
take r = b-s;
thus r < b by A27,XREAL_1:44;
thus for r1 be Real st r<r1 & r1<b & r1 in dom(F`|(].a,b.[)) holds
|. (F`|(].a,b.[)).r1 - f.b .| < g1
proof
let r1 be Real;
assume that
A29: r < r1 and
A30: r1 < b and
A31: r1 in dom(F`|(].a,b.[));
r1-b < 0 by A30,XREAL_1:49; then
A32: |. r1-b .| = -(r1-b) by COMPLEX1:70;
b-r1 < b-r by A29,XREAL_1:15; then
|. f.r1 - f.b .| < g1 by A11,A31,A6,A7,A28,A32;
hence |. (F`|(].a,b.[)).r1 - f.b .| < g1 by A14,A11,A31,FUNCT_1:49;
end;
end;
hence F`|(].a,b.[) is_left_convergent_in b by A25,LIMFUNC2:7;
end;
theorem Th35:
for a,b be Real, f,F be PartFunc of REAL,REAL st
a < b & [.a,b.] c= dom f & f|[.a,b.] is continuous & [.a,b.] c= dom F &
(for x be Real st x in [.a,b.] holds F.x = integral(f,a,x)) holds
F is_right_differentiable_in a & Rdiff(F,a) = lim_right(F`|(].a,b.[),a)
proof
let a,b be Real, f,F be PartFunc of REAL,REAL;
assume that
A1: a < b and
A2: [.a,b.] c= dom f and
A3: f|[.a,b.] is continuous and
A4: [.a,b.] c= dom F and
A5: for x be Real st x in [.a,b.] holds F.x = integral(f,a,x);
A6: [.a,b.] = ['a,b'] by A1,INTEGRA5:def 3;
].a,b.[ c= [.a,b.] by XXREAL_1:25; then
A7: ].a,b.[ c= dom f & ].a,b.[ c= dom F by A2,A4;
A8: [.a,b.[ c= [.a,b.] by XXREAL_1:24; then
A9: [.a,b.[ c= dom F by A4;
for x be Real st x in ].a,b.[ holds F|(].a,b.[) is_differentiable_in x
proof
let x be Real;
assume A10: x in ].a,b.[; then
F is_differentiable_in x by A1,A2,A3,A4,A5,Th32;
hence F|(].a,b.[) is_differentiable_in x by A10,PDIFFEQ1:2;
end; then
A11:F is_differentiable_on ].a,b.[ by A7;
A12:F`|(].a,b.[) is_right_convergent_in a by A1,A2,A3,A4,A5,Th34;
A13:dom(F|[.a,b.]) = [.a,b.] by A4,RELAT_1:62;
A14:for x be Real st x in [.a,b.] holds (F|[.a,b.]).x = integral(f,a,x)
proof
let x be Real;
assume A15: x in [.a,b.]; then
(F|[.a,b.]).x = F.x by FUNCT_1:49;
hence thesis by A15,A5;
end;
f|['a,b'] is bounded & f is_integrable_on ['a,b']
by A2,A3,A6,INTEGRA5:10,11; then
F|[.a,b.[ is Lipschitzian by A8,A1,A2,A13,A14,Th33,FCONT_1:33;
hence F is_right_differentiable_in a &
Rdiff(F,a) = lim_right(F`|(].a,b.[),a) by A1,A9,A11,A12,Th4;
end;
theorem Th36:
for a,b be Real, f,F be PartFunc of REAL,REAL st
a < b & [.a,b.] c= dom f & f|[.a,b.] is continuous & [.a,b.] c= dom F &
(for x be Real st x in [.a,b.] holds F.x = integral(f,a,x)) holds
F is_left_differentiable_in b & Ldiff(F,b) = lim_left(F`|(].a,b.[),b)
proof
let a,b be Real, f,F be PartFunc of REAL,REAL;
assume that
A1: a < b and
A2: [.a,b.] c= dom f and
A3: f|[.a,b.] is continuous and
A4: [.a,b.] c= dom F and
A5: for x be Real st x in [.a,b.] holds F.x = integral(f,a,x);
A6: [.a,b.] = ['a,b'] by A1,INTEGRA5:def 3;
].a,b.[ c= [.a,b.] by XXREAL_1:25; then
A7: ].a,b.[ c= dom f & ].a,b.[ c= dom F by A2,A4;
A8: ].a,b.] c= [.a,b.] by XXREAL_1:23; then
A9: ].a,b.] c= dom F by A4;
for x be Real st x in ].a,b.[ holds F|(].a,b.[) is_differentiable_in x
proof
let x be Real;
assume A10: x in ].a,b.[; then
F is_differentiable_in x by A1,A2,A3,A4,A5,Th32;
hence F|(].a,b.[) is_differentiable_in x by A10,PDIFFEQ1:2;
end; then
A11:F is_differentiable_on ].a,b.[ by A7;
A12:F`|(].a,b.[) is_left_convergent_in b by A1,A2,A3,A4,A5,Th34;
A13:dom(F|[.a,b.]) = [.a,b.] by A4,RELAT_1:62;
A14:for x be Real st x in [.a,b.] holds (F|[.a,b.]).x = integral(f,a,x)
proof
let x be Real;
assume A15: x in [.a,b.]; then
(F|[.a,b.]).x = F.x by FUNCT_1:49;
hence thesis by A15,A5;
end;
f|['a,b'] is bounded & f is_integrable_on ['a,b']
by A2,A3,A6,INTEGRA5:10,11; then
F|(].a,b.]) is Lipschitzian by A8,A1,A2,A13,A14,Th33,FCONT_1:33;
hence F is_left_differentiable_in b &
Ldiff(F,b) = lim_left(F`|(].a,b.[),b) by A1,A9,A11,A12,Th5;
end;
theorem Th37:
for a,b be Real, f,F be PartFunc of REAL,REAL st
a < b & [.a,b.] c= dom f & f|[.a,b.] is continuous & [.a,b.] c= dom F &
(for x be Real st x in [.a,b.] holds F.x = integral(f,a,x)) holds
F is_differentiable_on_interval ['a,b'] & F`\['a,b'] = f|['a,b']
proof
let a,b be Real, f,F be PartFunc of REAL,REAL;
assume that
A1: a < b and
A2: [.a,b.] c= dom f and
A3: f|[.a,b.] is continuous and
A4: [.a,b.] c= dom F and
A5: for x be Real st x in [.a,b.] holds F.x = integral(f,a,x);
reconsider I = ['a,b'] as non empty Interval;
A6: I = [.a,b.] by A1,INTEGRA5:def 3; then
A7: inf I = a & sup I = b by A1,XXREAL_2:25,29;
A8: inf I in I implies F is_right_differentiable_in lower_bound I
proof
assume inf I in I; then
a = lower_bound I by A7,Th1;
hence F is_right_differentiable_in lower_bound I
by A1,A2,A3,A4,A5,Th35;
end;
A9: sup I in I implies F is_left_differentiable_in upper_bound I
proof
assume sup I in I; then
b = upper_bound I by A7,Th2;
hence F is_left_differentiable_in upper_bound I
by A1,A2,A3,A4,A5,Th36;
end;
A10: ].a,b.[ c= [.a,b.] by XXREAL_1:25; then
A11: ].a,b.[ c= dom f & ].a,b.[ c= dom F by A2,A4;
for x be Real st x in ].a,b.[ holds F|(].a,b.[) is_differentiable_in x
proof
let x be Real;
assume A12: x in ].a,b.[; then
F is_differentiable_in x by A1,A2,A3,A4,A5,Th32;
hence F|(].a,b.[) is_differentiable_in x by A12,PDIFFEQ1:2;
end; then
A13: F is_differentiable_on ].inf I,sup I.[ by A7,A11;
thus
A14: F is_differentiable_on_interval ['a,b']
by A1,A4,A6,A7,A8,A9,A13,FDIFF_12:def 1;
for x be Real st x in ].a,b.[ holds F.x = integral(f,a,x) by A5,A10; then
A15: F`|(].a,b.[) = f|(].a,b.[) by A1,A2,A3,A11,Th27;
A16: dom(F`\['a,b']) = ['a,b'] & dom(f|['a,b']) = ['a,b']
by A2,A6,A14,FDIFF_12:def 2,RELAT_1:62;
for x be Element of REAL st x in dom(F`\['a,b']) holds
(F`\['a,b']).x = (f|['a,b']).x
proof
let x be Element of REAL;
assume A17: x in dom(F`\['a,b']);
per cases;
suppose A18: x = inf I; then
(F`\['a,b']).x = Rdiff(F,x) by A14,A17,A16,FDIFF_12:def 2; then
A19: (F`\['a,b']).x = lim_right(f|(].a,b.[),a)
by A15,A1,A2,A3,A4,A5,A7,A18,Th35;
x in [.a,b.[ by A1,A7,A18,XXREAL_1:3; then
(F`\['a,b']).x = f.x by A19,A2,A3,A7,A18,Th10;
hence (F`\['a,b']).x = (f|['a,b']).x by A17,A16,FUNCT_1:49;
end;
suppose A20: x = sup I; then
(F`\['a,b']).x = Ldiff(F,x) by A14,A17,A16,FDIFF_12:def 2; then
A21: (F`\['a,b']).x = lim_left(f|(].a,b.[),b)
by A15,A1,A2,A3,A4,A5,A7,A20,Th36;
x in ].a,b.] by A1,A7,A20,XXREAL_1:2; then
(F`\['a,b']).x = f.x by A21,A2,A3,A7,A20,Th11;
hence (F`\['a,b']).x = (f|['a,b']).x by A17,A16,FUNCT_1:49;
end;
suppose A22: x <> inf I & x <> sup I; then
A23: (F`\['a,b']).x = diff(F,x) by A14,A17,A16,FDIFF_12:def 2;
a <= x & x <= b by A17,A16,A6,XXREAL_1:1; then
a < x & x < b by A22,A7,XXREAL_0:1; then
x in ].a,b.[ by XXREAL_1:4; then
(F`\['a,b']).x = f.x by A1,A2,A3,A4,A5,A23,Th32;
hence (F`\['a,b']).x = (f|['a,b']).x by A17,A16,FUNCT_1:49;
end;
end;
hence F`\['a,b'] = f|['a,b'] by A16,PARTFUN1:5;
end;
theorem
for f be PartFunc of REAL,REAL, a,b be Real holds
integral(f,b,a) = -integral(f,a,b)
proof
let f be PartFunc of REAL,REAL, a,b be Real;
per cases;
suppose a <= b; then
A1: ['a,b'] = [.a,b.] by INTEGRA5:def 3; then
integral(f,['a,b']) = integral(f,a,b) by INTEGRA5:19;
hence integral(f,b,a) = -integral(f,a,b) by A1,INTEGRA5:20;
end;
suppose a > b; then
A2: ['b,a'] = [.b,a.] by INTEGRA5:def 3; then
-integral(f,['b,a']) = integral(f,a,b) by INTEGRA5:20;
hence integral(f,b,a) = -integral(f,a,b) by A2,INTEGRA5:19;
end;
end;
theorem
for a,b be Real, f,F be PartFunc of REAL,REAL st
a < b & [.a,b.] c= dom f & f|[.a,b.] is continuous & [.a,b.] c= dom F &
(for x be Real st x in [.a,b.] holds F.x = integral(f,a,x)) holds
for x be Real st x in ].a,b.[ holds
F is_differentiable_in x & diff(F,x) = f.x
proof
let a,b be Real, f,F be PartFunc of REAL,REAL;
set O = ].a,b.[;
assume that
A1: a < b and
A2: [.a,b.] c= dom f and
A3: f|[.a,b.] is continuous and
A4: [.a,b.] c= dom F and
A5: for x be Real st x in [.a,b.] holds F.x = integral(f,a,x);
reconsider I = ['a,b'] as non empty Interval;
A6: I = [.a,b.] by A1,INTEGRA5:def 3; then
A7: inf I = a & sup I = b by A1,XXREAL_2:25,29;
A8: F is_differentiable_on_interval ['a,b'] &
F`\['a,b'] = f|['a,b'] by A1,A2,A3,A4,A5,Th37; then
A9: F is_differentiable_on ].a,b.[ by A7,FDIFF_12:def 1;
hereby let x be Real;
assume A10: x in ].a,b.[;
hence F is_differentiable_in x by A9,FDIFF_1:9;
A11: ].a,b.[ c= ['a,b'] by A6,XXREAL_1:25;
inf I < x & x < sup I by A7,A10,XXREAL_1:4; then
(F`\['a,b']).x = diff(F,x) by A8,A10,A11,FDIFF_12:def 2;
hence diff(F,x) = f.x by A8,A10,A11,FUNCT_1:49;
end;
end;
Lm1:
for f be PartFunc of REAL,REAL, I be non empty Interval, a be Real
ex F be PartFunc of REAL,REAL st dom F = REAL &
for x be Real st x in I holds F.x = integral(f,a,x)
proof
let f be PartFunc of REAL,REAL;
let I be non empty Interval;
let a be Real;
deffunc G(Real) = 0;
defpred C[set] means $1 in I;
deffunc F(Real) = integral(f,a,$1);
consider F be Function such that
A1: dom F = REAL &
for x be Element of REAL holds (C[x] implies F.x = F(x)) &
(not C[x] implies F.x = G(x)) from PARTFUN1:sch 4;
now let y be object;
assume y in rng F; then
consider x be object such that
A2: x in dom F and
A3: y = F.x by FUNCT_1:def 3;
reconsider x as Element of REAL by A1,A2;
A4: now
assume not x in I; then
F.x = In(0,REAL) by A1;
hence y in REAL by A3;
end;
now
assume x in I; then
F.x = integral(f,a,x) by A1;
hence y in REAL by A3,XREAL_0:def 1;
end;
hence y in REAL by A4;
end; then
rng F c= REAL; then
reconsider F as PartFunc of REAL,REAL by A1,RELSET_1:4;
take F;
thus thesis by A1;
end;
theorem
for a,b be Real, f be PartFunc of REAL,REAL st
a < b & [.a,b.] c= dom f & f|([.a,b.]) is continuous
ex F be PartFunc of REAL,REAL st F is_antiderivative_of f,['a,b'] &
(for x be Real st x in [.a,b.] holds F.x = integral(f,a,x))
proof
let a,b be Real, f be PartFunc of REAL,REAL;
assume that
A1: a < b and
A2: [.a,b.] c= dom f and
A3: f|([.a,b.]) is continuous;
reconsider I = ['a,b'] as non empty Interval;
A4: I = [.a,b.] by A1,INTEGRA5:def 3;
consider F be PartFunc of REAL,REAL such that
A5: dom F = REAL &
for x be Real st x in I holds F.x = integral(f,a,x) by Lm1;
F is_differentiable_on_interval I & F`\I = f|I by A1,A2,A3,A5,A4,Th37;
hence thesis by Def1,A5,A4;
end;
theorem
for c be Real, f,F,G be PartFunc of REAL,REAL, I be non empty Interval st
I c= dom f & F is_antiderivative_of f,I &
I c= dom G & (for x be Real st x in I holds G.x = F.x + c) holds
G is_antiderivative_of f,I
proof
let c be Real, f,F,G be PartFunc of REAL,REAL, I be non empty Interval;
assume that
A1: I c= dom f and
A2: F is_antiderivative_of f,I and
A3: I c= dom G and
A4: for x be Real st x in I holds G.x = F.x + c;
A5: I c= dom F & inf I < sup I by A2,FDIFF_12:def 1;
reconsider c0=c as Element of REAL by XREAL_0:def 1;
deffunc F(Element of REAL) = c0;
consider F0 be Function of REAL,REAL such that
A6: for x be Element of REAL holds F0.x = F(x) from FUNCT_2:sch 4;
set G0 = F0|I;
dom F0 = REAL by FUNCT_2:def 1; then
A7: dom G0 = I by RELAT_1:62;
A8: now let y be object;
assume y in rng G0; then
consider x be Element of REAL such that
A9: x in dom G0 & G0.x = y by PARTFUN1:3;
G0.x = F0.x by A9,FUNCT_1:47; then
G0.x = c by A6;
hence y in {c} by A9,TARSKI:def 1;
end; then
A10: rng G0 c= {c};
now let y be object;
assume y in {c}; then
A11: y = c by TARSKI:def 1;
consider x be object such that
A12: x in I by XBOOLE_0:def 1;
reconsider x as Element of REAL by A12;
G0.x = F0.x by A12,FUNCT_1:49; then
G0.x = c by A6;
hence y in rng G0 by A7,A12,A11,FUNCT_1:3;
end; then
{c} c= rng G0; then
A13:rng G0 = {c} by A10,XBOOLE_0:def 10; then
A14:G0 is_differentiable_on_interval I &
for x be Real st x in I holds (G0`\I).x = 0 by A5,A7,FDIFF_12:15;
A15:dom(F|I) = I by A5,RELAT_1:62;
A16:dom(F|I + G0) = dom(F|I) /\ dom G0 by VALUED_1:def 1;
A17: F|I is_differentiable_on_interval I by A2,Th15;
A18: dom(f|I) = I by A1,RELAT_1:62;
now let x be Element of REAL;
assume
A19: x in dom(G|I); then
(G|I).x = G.x by FUNCT_1:47; then
A20: (G|I).x = F.x + c by A19,A4;
A21: F.x = (F|I).x by A19,A15,FUNCT_1:47;
G0.x in {c} by A7,A19,A8,FUNCT_1:3; then
G0.x = c by TARSKI:def 1;
hence (G|I).x = ((F|I)+G0).x by A16,A15,A7,A19,A20,A21,VALUED_1:def 1;
end; then
A22: G|I = F|I + G0 by A16,A15,A7,A3,RELAT_1:62,PARTFUN1:5; then
A23: G|I is_differentiable_on_interval I by A16,A15,A7,A14,A17
,FDIFF_12:19; then
A24: G is_differentiable_on_interval I by Th15; then
A25: dom(G`\I) = I by FDIFF_12:def 2;
now let x be Element of REAL;
assume
A26: x in dom(G`\I); then
A27: (G0`\I).x = 0 by A13,A25,A5,A7,FDIFF_12:15;
G`\I = (G|I)`\I by A24,Th16; then
(G`\I).x = ((F|I)`\I).x + (G0`\I).x
by A22,A25,A26,A16,A15,A7,A17,A14,FDIFF_12:19;
hence (G`\I).x = (f|I).x by A27,A2,Th16;
end;
hence G is_antiderivative_of f,I by A23,A18,A25,Th15,PARTFUN1:5;
end;
theorem Th42:
for f,F be PartFunc of REAL,REAL, I,J be non empty Interval st
inf I < sup I & I c= J & F is_antiderivative_of f,J holds
F is_antiderivative_of f,I
proof
let f,F be PartFunc of REAL,REAL, I,J be non empty Interval;
assume that
A1: inf I < sup I and
A2: I c= J and
A3: F is_antiderivative_of f,J;
F is_differentiable_on_interval I by A1,A2,A3,FDIFF_12:38; then
A4: dom(F`\I) = I by FDIFF_12:def 2;
dom(f|J) = J by A3,FDIFF_12:def 2; then
dom f /\ J = J by RELAT_1:61; then
A5: dom(f|I) = I by A2,XBOOLE_1:18,RELAT_1:62;
now let x be Element of REAL;
assume
A6: x in dom(F`\I); then
(F`\I).x = (f|J).x by A4,A3,A1,A2,FDIFF_12:38; then
(F`\I).x = ((f|J)|I).x by A6,A4,FUNCT_1:49;
hence (F`\I).x = (f|I).x by A2,RELAT_1:74;
end;
hence F is_antiderivative_of f,I by A4,A5,A1,A2,A3,FDIFF_12:38,PARTFUN1:5;
end;
Lm2:
for I,J be Subset of REAL st J c= I holds ].inf J,sup J.[ c= ].inf I,sup I.[
proof
let I,J be Subset of REAL;
assume J c= I; then
inf I <= inf J & sup J <= sup I by XXREAL_2:59,60;
hence ].inf J,sup J.[ c= ].inf I,sup I.[ by XXREAL_1:46;
end;
Lm3:
for I be non empty closed_interval Subset of REAL,
f be PartFunc of REAL,REAL, D be Division of I st
f is_differentiable_on_interval I & f`\I is bounded
holds lower_sum((f`\I)||I,D) <= f.(upper_bound I)-f.(lower_bound I) &
f.(upper_bound I)-f.(lower_bound I) <=upper_sum((f`\I)||I,D)
proof
let I be non empty closed_interval Subset of REAL,
f be PartFunc of REAL,REAL, D be Division of I;
assume that
A1: f is_differentiable_on_interval I and
A2: f`\I is bounded;
A3: f is_differentiable_on ].inf I,sup I.[ by A1,FDIFF_12:def 1;
reconsider k1 =len D - 1 as Element of NAT by ORDINAL1:def 12;
deffunc G(Nat)=In(f.(lower_bound divset(D,$1+1)),REAL);
deffunc F(Nat)
= In(f.(upper_bound divset(D,$1))-f.(lower_bound divset(D,$1)),REAL);
consider p being FinSequence of REAL such that
A4: len p = len D & for i be Nat st i in dom p holds p.i = F(i) from
FINSEQ_2:sch 1;
A5: I c= dom f by A1,FDIFF_12:def 1;
A6: for k be Nat st k in dom D holds ex r be Real st r in divset(D,k) &
f.(upper_bound divset(D,k))
-f.(lower_bound divset(D,k))=((f`\I).r)*vol(divset(D,k))
proof
let k be Nat;
assume
A7: k in dom D;
now per cases;
suppose
A8: lower_bound divset(D,k)=upper_bound divset(D,k);
consider r be Real such that
A9: r = upper_bound divset(D,k);
A10: r in divset(D,k)
proof
ex a,b be Real st a<=b & a=lower_bound divset(D,k) &
b=upper_bound divset(D,k) by SEQ_4:11;
hence thesis by A9,INTEGRA2:1;
end;
(f`\I).r * vol(divset(D,k)) = 0 by A8;
hence thesis by A8,A10;
end;
suppose
A11: lower_bound divset(D,k)<>upper_bound divset(D,k);
ex r1,r2 be 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|I is continuous by A1,FDIFF_12:37;
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= I by A7,INTEGRA1:8;
A17: ].lower_bound divset(D,k),upper_bound divset(D,k).[
c= ].lower_bound I,upper_bound I.[ by A7,Lm2,INTEGRA1:8;
then
f is_differentiable_on ].lower_bound divset(D,k),
upper_bound divset(D,k).[ by A3,FDIFF_1:26;
then consider r be Real such that
A18: r in ].lower_bound divset(D,k),upper_bound divset(D,k).[ and
A19: 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;
A20: r in I by A16,A15,A18;
A21: inf I <= lower_bound divset(D,k) & upper_bound divset(D,k) <= sup I
by A17,A12,XXREAL_1:63;
lower_bound divset(D,k) < r & r < upper_bound divset(D,k)
by A18,XXREAL_1:4; then
A22: diff(f,r) = (f`\I).r by A1,A20,A21,FDIFF_12:def 2;
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 A19,XCMPLX_1:87;
hence thesis by A22,A15,A18;
end;
end;
hence thesis;
end;
A23:dom p = Seg len D by A4,FINSEQ_1:def 3;
A24:for i be Nat st i in Seg k1 holds upper_bound divset(D,i)
= lower_bound divset(D,i+1)
proof
let i be Nat;
assume
A25: i in Seg k1;
then i <= k1 by FINSEQ_1:1;
then
A26: i+1 <= k1+1 by XREAL_1:7;
1+0 <= i+1 by XREAL_1:7;
then i+1 in Seg(len D) by A26,FINSEQ_1:1;
then
A27: i+1 in dom D by FINSEQ_1:def 3;
k1 + 1 = len D;
then Seg k1 c= Seg len D by FINSEQ_1:5,NAT_1:11;
then i in Seg (len D) by A25;
then
A28: i in dom D by FINSEQ_1:def 3;
A29: i+1-1=i;
now
per cases;
suppose
A30: i=1;
then upper_bound divset(D,i) = D.i by A28,INTEGRA1:def 4;
hence thesis by A27,A29,A30,INTEGRA1:def 4;
end;
suppose
A31: i<>1;
i >= 1 by A25,FINSEQ_1:1;
then i+1>=1+1 by XREAL_1:6;
then
A32: i+1 <> 1;
upper_bound divset(D,i) = D.i by A28,A31,INTEGRA1:def 4;
hence thesis by A27,A29,A32,INTEGRA1:def 4;
end;
end;
hence thesis;
end;
consider s2 being FinSequence of REAL such that
A33: len s2 = k1 & for i be Nat st i in dom s2 holds s2.i = G(i) from
FINSEQ_2:sch 1;
A34:for k be Nat st k in dom D holds
rng(((f`\I)||I)|divset(D,k)) is real-bounded
proof
A35: dom(f`\I) = I by A1,FDIFF_12:def 2;
then reconsider g=f`\I as PartFunc of I,REAL by RELSET_1:5;
let k be Nat;
assume k in dom D;
A36: (f`\I)|I = f`\I by A35;
consider r1 be Real such that
A37: for x being object st x in I /\ dom(f`\I) holds (f`\I).x <= r1 by A2,
A36,RFUNCT_1:70;
consider r2 be Real such that
A38: for x being object st x in I /\ dom(f`\I) holds (f`\I).x >= r2 by A2,
A36,RFUNCT_1:71;
for x being object st x in I /\ dom((f`\I)||I) holds ((f`\I)||I).x>=r2
proof
let x be object;
reconsider y=g.x as Real;
assume x in I /\ dom((f`\I)||I);
then y >= r2 by A38;
hence thesis;
end;
then (f`\I)||I|I is bounded_below by RFUNCT_1:71; then
A39: rng(((f`\I)||I)|divset(D,k)) is bounded_below by INTEGRA4:19;
for x being object st x in I /\ dom((f`\I)||I) holds ((f`\I)||I).x<=r1
proof
let x be object;
reconsider y=g.x as Real;
assume x in I /\ dom((f`\I)||I);
then y <= r1 by A37;
hence thesis;
end;
then (f`\I)||I|I is bounded_above by RFUNCT_1:70;
then rng(((f`\I)||I)|divset(D,k)) is bounded_above by INTEGRA4:18;
hence thesis by A39;
end;
deffunc F1(Nat)=In(f.(upper_bound divset(D,$1)),REAL);
consider s1 being FinSequence of REAL such that
A40: len s1 = k1 & for i be Nat st i in dom s1 holds s1.i = F1(i) from
FINSEQ_2:sch 1;
A41:dom s2 = Seg k1 by A33,FINSEQ_1:def 3;
reconsider flb = f.(lower_bound I), fub = f.(upper_bound I)
as Element of REAL by XREAL_0:def 1;
len (s1^<*f.(upper_bound I)*>) = len (<*f.(lower_bound I)*>^s2) &
len (s1^<*f.(upper_bound I)*>) = len p &
for i be Element of NAT st i in dom (s1^<*fub*>) holds
p.i=((s1^<*fub*>)/.i) - ((<*flb*>^s2)/.i)
proof
dom(<*f.(upper_bound I)*>)=Seg 1 by FINSEQ_1:def 8;
then len(<*f.(upper_bound I)*>)=1 by FINSEQ_1:def 3;
then
A42: len(s1^<*f.(upper_bound I)*>)=k1+1 by A40,FINSEQ_1:22;
dom(<*f.(lower_bound I)*>)=Seg 1 by FINSEQ_1:def 8;
then len(<*f.(lower_bound I)*>)=1 by FINSEQ_1:def 3;
hence
A43: len (s1^<*f.(upper_bound I)*>) = len (<*f.(lower_bound I)*>^s2)
by A33,A42,FINSEQ_1:22;
thus len (s1^<*f.(upper_bound I)*>) = len p by A4,A42;
let i be Element of NAT;
assume
A44: i in dom (s1^<*fub*>); then
A45: (s1^<*fub*>)/.i=(s1^<*f.(upper_bound I)*>).i
by PARTFUN1:def 6;
i in Seg(len (s1^<*f.(upper_bound I)*>)) by A44,FINSEQ_1:def 3;
then i in dom (<*f.(lower_bound I)*>^s2) by A43,FINSEQ_1:def 3;
then
A46: (<*flb*>^s2)/.i=(<*flb*>^s2).i by PARTFUN1:def 6;
A47:len D = 1 or len D is non trivial by NAT_2:def 1;
now per cases by A47,NAT_2:29;
suppose
A48: len D = 1;
then
A49: i in Seg 1 by A42,A44,FINSEQ_1:def 3;
then
A50: i = 1 by FINSEQ_1:2,TARSKI:def 1;
s1={} by A40,A48;
then s1^<*f.(upper_bound I)*> = <*f.(upper_bound I)*> by FINSEQ_1:34;
then
A51: (s1^<*fub*>)/.i=f.(upper_bound I)
by A45,A50;
A52: i in dom D by A48,A49,FINSEQ_1:def 3;
s2={} by A33,A48;
then <*f.(lower_bound I)*>^s2 = <*f.(lower_bound I)*> by FINSEQ_1:34;
then
A53: (<*flb*>^s2)/.i=f.(lower_bound I)
by A46,A50;
D.i=upper_bound I by A48,A50,INTEGRA1:def 2;
then
A54: upper_bound divset(D,i)=upper_bound I by A50,A52,INTEGRA1:def 4;
p.i = F(i) by A4,A23,A48,A49;
hence thesis by A50,A52,A51,A53,A54,INTEGRA1:def 4;
end;
suppose
A55: len D >= 2;
A56: 1 = 2 - 1;
now per cases;
suppose
A57: i=1; then
A58: i in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then i in dom <*f.(lower_bound I)*> by FINSEQ_1:def 8;
then (<*f.(lower_bound I)*>^s2).i=<*f.(lower_bound I)*>.i
by FINSEQ_1:def 7; then
A59: (<*f.(lower_bound I)*>^s2).i = f.(lower_bound I)
by A57;
Seg 1 c= Seg k1 by A56,A55,XREAL_1:9,FINSEQ_1:5;
then i in Seg k1 by A58; then
A60: i in dom s1 by A40,FINSEQ_1:def 3;
then (s1^<*f.(upper_bound I)*>).i=s1.i by FINSEQ_1:def 7; then
A61: (s1^<*f.(upper_bound I)*>).i = F1(i) by A40,A60;
A62: i in Seg 2 by A57,FINSEQ_1:2,TARSKI:def 2;
A63: Seg 2 c= Seg len D by A55,FINSEQ_1:5;
then i in Seg(len D) by A62;
then
A64: i in dom D by FINSEQ_1:def 3;
p.i= F(i) by A4,A23,A63,A62;
hence thesis by A45,A46,A57,A64,A61,A59,INTEGRA1:def 4;
end;
suppose
A65: i=len D;
then i-len s1 in Seg 1 by A40,FINSEQ_1:2,TARSKI:def 1;
then
A66: i-len s1 in dom <*f.(upper_bound I)*> by FINSEQ_1:def 8;
i=i-len s1 + len s1;
then (s1^<*f.(upper_bound I)*>).i=<*f.(upper_bound I)*>.(i-len s1)
by A66,FINSEQ_1:def 7; then
A67: (s1^<*fub*>)/.i=f.(upper_bound I)
by A40,A45,A65;
A68: len <*f.(lower_bound I)*> = 1 by FINSEQ_1:40;
A69: i<>1 by A55,A65;
i in Seg len D by A65,FINSEQ_1:3; then
A70: i in dom D by FINSEQ_1:def 3;
p.i = F(i) by A4,A23,A65,FINSEQ_1:3;
then p.i=f.(upper_bound divset(D,i))-f.(D.(i-1))
by A70,A69,INTEGRA1:def 4; then
A71: p.i=f.(D.i)-f.(D.(i-1)) by A70,A69,INTEGRA1:def 4;
i-1<>0 by A55,A65;
then
A72: i-1 in Seg k1 by A65,FINSEQ_1:3;
reconsider i1 = i-1 as Nat by A65;
A73: len <*f.(lower_bound I)*> + (i - len <*f.(lower_bound I)*>) = i &
i-len <*f.(lower_bound I)*> in dom s2 by A33,A68,FINSEQ_1:def 3,A72;
then (<*f.(lower_bound I)*>^s2).i = s2.(i1) by FINSEQ_1:def 7,A68;
then (<*f.(lower_bound I)*>^s2).i = G(i1) by A33,A68,A73;
then (<*f.(lower_bound I)*>^s2).i = f.(D.(i-1))
by A70,A69,INTEGRA1:def 4;
hence thesis by A46,A65,A67,A71,INTEGRA1:def 2;
end;
suppose
A74: i<>1 & i<>len D;
len s1+len <*f.(upper_bound I)*> = k1+1 by A40,FINSEQ_1:39;
then
A75: i in Seg(len D) by A44,FINSEQ_1:def 7;
A76: i in dom s1 & i in Seg k1 & i-1 in Seg k1 & i-1+1=i
& i-len <*f.(lower_bound I)*> in dom s2
proof
i <> 0 by A75,FINSEQ_1:1;
then i is non trivial by A74,NAT_2:def 1;
then i >= 1+1 by NAT_2:29; then
A77: i-1 >= 1 by XREAL_1:19;
A78: 1 <= i by A75,FINSEQ_1:1;
i <= len D by A75,FINSEQ_1:1; then
A79: i < k1 + 1 by A74,XXREAL_0:1; then
A80: i <= k1 by NAT_1:13;
then i in Seg(len s1) by A40,A78,FINSEQ_1:1;
hence i in dom s1 by FINSEQ_1:def 3;
thus i in Seg k1 by A78,A80,FINSEQ_1:1;
i <= k1 by A79,NAT_1:13;
then i-1 <= k1-1 by XREAL_1:9;
then
i-1+0 <= k1-1+1 by XREAL_1:7;
hence i-1 in Seg k1 by A77,A78,FINSEQ_1:1;
then
A81: i-len<*f.(lower_bound I)*> in Seg(len s2) by A33,FINSEQ_1:39;
thus i-1+1=i;
thus thesis by A81,FINSEQ_1:def 3;
end;
then
A82: i-len<*f.(lower_bound I)*> in Seg(len s2) by FINSEQ_1:def 3;
then
A83: i<=len<*f.(lower_bound I)*>+len s2 by XREAL_1:20,FINSEQ_1:1;
i >= 1 by A75, FINSEQ_1:1;
then reconsider i1=i-1 as Element of NAT by INT_1:5;
1 <= i-len<*f.(lower_bound I)*> by A82,FINSEQ_1:1;
then len<*f.(lower_bound I)*>+1<=i by XREAL_1:19;
then (<*f.(lower_bound I)*>^s2).i=s2.(i-len<*f.(lower_bound I)*>)
by A83,FINSEQ_1:23;
then (<*f.(lower_bound I)*>^s2).i=s2.(i-1) by FINSEQ_1:39; then
A84: (<*f.(lower_bound I)*>^s2).i= G(i1) by A33,A41,A76;
(s1^<*f.(upper_bound I)*>).i = s1.i by A76,FINSEQ_1:def 7; then
A85: (s1^<*f.(upper_bound I)*>).i = F1(i) by A40,A76;
p.i=F(i) by A4,A23,A75;
hence p.i= ((s1^<*fub*>)/.i) - ((<*flb*>^s2)/.i)
by A44,A46,A84,A85,PARTFUN1:def 6;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
then Sum p=Sum(s1^<*f.(upper_bound I)*>)-Sum(<*f.(lower_bound I)*>^s2)
by INTEGRA1:22;
then Sum p=Sum s1 + f.(upper_bound I) -Sum(<*f.(lower_bound I)*>^s2)
by RVSUM_1:74; then
A86: Sum p=Sum s1 + f.(upper_bound I) - (f.(lower_bound I) + Sum s2)
by RVSUM_1:76;
A87: dom s1 = Seg k1 by A40,FINSEQ_1:def 3;
for i being Nat st i in dom s1 holds s1.i = s2.i
proof
let i be Nat;
assume
A88: i in dom s1;
then s1.i = F1(i) by A40;
then s1.i= G(i) by A24,A87,A88;
hence thesis by A87,A33,A41,A88;
end;
then
A89: s1=s2 by A40,A33,FINSEQ_2:9;
A90:
for k be Element of NAT, r be Real st k in dom D & r in divset(D,k)
holds (f`\I).r in rng (((f`\I)||I)|divset(D,k))
proof
dom((f`\I)|I) = dom(f`\I) /\ I by RELAT_1:61; then
A91: dom((f`\I)|I) = I /\ I by A1,FDIFF_12:def 2;
let k be Element of NAT, r be Real;
assume that
A92: k in dom D and
A93: r in divset(D,k);
A94: divset(D,k) c= I by A92,INTEGRA1:8;
A95: (f`\I).r = ((f`\I)||I).r by A93,A94,A91,FUNCT_1:47;
dom(((f`\I)||I)|divset(D,k))= I /\ divset(D,k) by A91,RELAT_1:61; then
A96: dom(((f`\I)||I)|divset(D,k))=divset(D,k) by A92,INTEGRA1:8,XBOOLE_1:28;
then ((f`\I)||I)|divset(D,k).r in rng(((f`\I)||I)|divset(D,k))
by A93,FUNCT_1:def 3;
hence thesis by A95,A93,A96,FUNCT_1:47;
end;
A97: for k be Element of NAT st k in dom D
holds f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k))<=(
upper_volume((f`\I)||I,D)).k
proof
let k be Element of NAT;
A98: vol(divset(D,k)) >= 0 by INTEGRA1:9;
assume
A99: k in dom D;
then consider r be Real such that
A100: r in divset(D,k) and
A101: f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k))
=((f`\I).r)*vol(divset(D,k)) by A6;
A102: rng(((f`\I)||I)|divset(D,k)) is real-bounded by A34,A99;
(f`\I).r in rng(((f`\I)||I)|divset(D,k)) by A90,A99,A100;
then (f`\I).r <= upper_bound rng(((f`\I)||I)|divset(D,k))
by A102,SEQ_4:def 1;
then ((f`\I).r)*vol(divset(D,k)) <=
(upper_bound rng(((f`\I)||I)|divset(D,k)))*vol(
divset(D,k)) by A98,XREAL_1:64;
hence thesis by A99,A101,INTEGRA1:def 6;
end;
A103: f.(upper_bound I)-f.(lower_bound I)<=upper_sum((f`\I)||I,D)
proof
len upper_volume((f`\I)||I,D)=len D by INTEGRA1:def 6;
then reconsider
q=(upper_volume((f`\I)||I,D)) as Element of (len D)-tuples_on
REAL by FINSEQ_2:92;
A104: for k be Nat st k in Seg len D holds p.k <= (upper_volume((f`\I)||I,
D)).k
proof
let k be Nat;
assume
A105: k in Seg len D;
f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k)) = F(k); then
A106: f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k))
= p.k by A4,A23,A105;
k in dom D by FINSEQ_1:def 3,A105;
hence thesis by A97,A106;
end;
reconsider p as Element of (len D)-tuples_on REAL by A4,FINSEQ_2:92;
Sum p<=Sum q by A104,RVSUM_1:82;
hence thesis by A89,A86;
end;
A107: for k be Element of NAT st k in dom D
holds f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k))>=(
lower_volume((f`\I)||I,D)).k
proof
let k be Element of NAT;
assume
A108: k in dom D;
then
A109: vol(divset(D,k)) >= 0 & (lower_bound rng(((f`\I)||I)|divset(D,k)))*vol(
divset(D,k)) =(lower_volume((f`\I)||I,D)).k by INTEGRA1:9,def 7;
A110: rng(((f`\I)||I)|divset(D,k)) is real-bounded by A34,A108;
consider r be Real such that
A111: r in divset(D,k) and
A112: f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k))
=((f`\I).r)*vol(divset(D,k)) by A6,A108;
(f`\I).r in rng(((f`\I)||I)|divset(D,k)) by A90,A108,A111;
then (f`\I).r >= lower_bound rng(((f`\I)||I)|divset(D,k))
by A110,SEQ_4:def 2;
hence thesis by A112,A109,XREAL_1:64;
end;
f.(upper_bound I)-f.(lower_bound I)>=lower_sum((f`\I)||I,D)
proof
len lower_volume((f`\I)||I,D)=len D by INTEGRA1:def 7;
then reconsider
q=(lower_volume((f`\I)||I,D)) as Element of (len D)-tuples_on
REAL by FINSEQ_2:92;
A113: for k be Nat st k in Seg len D holds p.k >= (lower_volume((f`\I)||I,
D)).k
proof
let k be Nat;
assume
A114: k in Seg len D;
A115: f.(upper_bound divset(D,k))-f.(lower_bound divset(D,k)) = F(k)
.=p.k by A4,A23,A114;
k in dom D by FINSEQ_1:def 3,A114;
hence thesis by A107,A115;
end;
reconsider p as Element of (len D)-tuples_on REAL by A4,FINSEQ_2:92;
Sum q<=Sum p by A113,RVSUM_1:82;
hence thesis by A89,A86;
end;
hence thesis by A103;
end;
theorem Th43:
for a,b be Real, f be PartFunc of REAL,REAL, D be Division of ['a,b'] st
a < b & f is_differentiable_on_interval ['a,b'] & f`\['a,b'] is bounded
holds lower_sum((f`\['a,b'])||['a,b'],D) <= f.b-f.a &
f.b-f.a <=upper_sum((f`\['a,b'])||['a,b'],D)
proof
let a,b be Real, f be PartFunc of REAL,REAL, D be Division of ['a,b'];
assume that
A1: a < b and
A2: f is_differentiable_on_interval ['a,b'] and
A3: f`\['a,b'] is bounded;
reconsider I = ['a,b'] as non empty closed_interval Subset of REAL;
I = [.a,b.] by A1,INTEGRA5:def 3; then
lower_bound I = a & upper_bound I = b by A1,XXREAL_2:25,29;
hence thesis by A2,A3,Lm3;
end;
Lm4:
for a,b be Real, f be PartFunc of REAL,REAL st
a < b & f is_differentiable_on_interval ['a,b'] &
f`\['a,b'] is_integrable_on ['a,b'] & f`\['a,b'] is bounded
holds integral(f`\['a,b'],['a,b']) = f.b - f.a
proof
let a,b be Real, f be PartFunc of REAL,REAL;
assume that
A1: a < b and
A2: f is_differentiable_on_interval ['a,b'] and
A3: f`\['a,b'] is_integrable_on ['a,b'] and
A4: f`\['a,b'] is bounded;
reconsider I = ['a,b'] as non empty closed_interval Subset of REAL;
A5: (f`\I)||I is integrable by A3;
for r be Real st r in rng upper_sum_set((f`\I)||I) holds f.b-f.a <= r
proof
let r be Real;
assume r in rng upper_sum_set((f`\I)||I);
then consider D being Element of divs I such that
A6: D in dom upper_sum_set((f`\I)||I) & r=(upper_sum_set((f`\I)||I)).D
by PARTFUN1:3;
reconsider D as Division of I by INTEGRA1:def 3;
r=upper_sum((f`\I)||I,D) by A6,INTEGRA1:def 10;
hence thesis by A2,A4,A1,Th43;
end; then
A7: f.b-f.a <= lower_bound rng upper_sum_set((f`\I)||I) by SEQ_4:43;
for r be Real st r in rng lower_sum_set((f`\I)||I) holds r <= f.b-f.a
proof
let r be Real;
assume r in rng lower_sum_set((f`\I)||I);
then consider D being Element of divs I such that
A8: D in dom lower_sum_set((f`\I)||I) & r=(lower_sum_set((f`\I)||I)).D
by PARTFUN1:3;
reconsider D as Division of I by INTEGRA1:def 3;
r=lower_sum((f`\I)||I,D) by A8,INTEGRA1:def 11;
hence thesis by A2,A4,A1,Th43;
end; then
upper_bound rng lower_sum_set((f`\I)||I) <= f.b-f.a by SEQ_4:45;
hence thesis by A5,A7,XXREAL_0:1;
end;
theorem
for f be PartFunc of REAL,REAL, a,b be Real, I be non empty Interval
st a in I & b in I & a < b & f is_differentiable_on_interval I &
f`\I is_integrable_on ['a,b'] & f`\I is bounded holds
integral(f`\['a,b'],a,b) = f.b - f.a & integral(f`\I,a,b) = f.b - f.a
proof
let f be PartFunc of REAL,REAL, a,b be Real,
I be non empty Interval;
assume that
A1: a in I & b in I and
A2: a < b and
A3: f is_differentiable_on_interval I and
A4: f`\I is_integrable_on ['a,b'] and
A5: f`\I is bounded;
reconsider J = ['a,b'] as non empty closed_interval Subset of REAL;
A6: J = [.a,b.] by A2,INTEGRA5:def 3; then
A7: ['a,b'] c= I by A1,Th3;
A8:a = inf J & b = sup J by A2,A6,MEASURE6:10,14; then
A9:f is_differentiable_on_interval J by A3,A7,A2,FDIFF_12:38;
(f`\I)|J is_integrable_on J by A4; then
A10:f`\J is_integrable_on J by A3,A6,A1,Th3,A2,A8,Th17;
(f`\I)|J is bounded by A5; then
f`\J is bounded by A3,A6,A1,Th3,A2,A8,Th17; then
A11:integral(f`\['a,b'],['a,b']) = f.b - f.a by A2,A9,A10,Lm4;
hence integral(f`\['a,b'],a,b) = f.b - f.a by A2,INTEGRA5:def 4;
integral(f`\I,a,b) = integral(f`\I,J) by A2,INTEGRA5:def 4; then
integral(f`\I,a,b) = integral(((f`\I)|J)||J);
hence thesis by A11,A3,A6,A1,A2,A8,Th3,Th17;
end;
theorem
for f be PartFunc of REAL,REAL, a be Real, I be non empty Interval st
f is_differentiable_on_interval I & a in I holds integral(f`\I,a,a) = 0
proof
let f be PartFunc of REAL,REAL, a be Real,
I be non empty Interval;
assume that
A1: f is_differentiable_on_interval I and
A2: a in I;
A3: dom(f`\I) = I by A1,FDIFF_12:def 2;
A4: ['a,a'] = [.a,a.] by INTEGRA5:def 3; then
A5: ['a,a'] c= dom(f`\I) by A3,A2,Th3;
for x be Real st x in ['a,a'] holds (f`\I).x = (f`\I).a
proof
let x be Real;
assume x in ['a,a']; then
a <= x & x <= a by A4,XXREAL_1:1;
hence (f`\I).x = (f`\I).a by XXREAL_0:1;
end; then
integral(f`\I,a,a) = (f`\I).a * (a-a) by A5,INTEGRA6:26;
hence integral(f`\I,a,a) = 0;
end;
Lm5:
for f,F,G be PartFunc of REAL,REAL, I be non empty open_interval Subset of REAL
st F is_antiderivative_of f,I & G is_antiderivative_of f,I
ex c be Real st for x be Real st x in I holds F.x = G.x + c
proof
let f,F,G be PartFunc of REAL,REAL,
I be non empty open_interval Subset of REAL;
assume that
A1: F is_antiderivative_of f,I and
A2: G is_antiderivative_of f,I;
A3: I = ].inf I,sup I.[ by MEASURE6:16;
A4: F is_differentiable_on ].inf I,sup I.[ by A1,FDIFF_12:def 1;
A5: G is_differentiable_on ].inf I,sup I.[ by A2,FDIFF_12:def 1;
A6: inf I is R_eal & sup I is R_eal by XXREAL_0:def 1;
for x be Real st x in ].inf I,sup I.[ holds diff(F,x) = diff(G,x)
proof
let x be Real;
assume
A7: x in ].inf I,sup I.[; then
x <> inf I & x <> sup I by XXREAL_1:4; then
(F`\I).x = diff(F,x) & (G`\I).x = diff(G,x)
by A3,A1,A2,A7,FDIFF_12:def 2;
hence diff(F,x) = diff(G,x) by A1,A2;
end;
hence ex c be Real st for x be Real st x in I holds F.x = G.x + c
by A6,A3,A4,A5,Th20;
end;
theorem
for f,F,G be PartFunc of REAL,REAL, I be non empty Interval st
F is_antiderivative_of f,I & G is_antiderivative_of f,I
ex c be Real st for x be Real st x in I holds F.x = G.x + c
proof
let f,F,G be PartFunc of REAL,REAL,
I be non empty Interval;
assume that
A1: F is_antiderivative_of f,I and
A2: G is_antiderivative_of f,I;
A3: inf I < sup I by A1,FDIFF_12:def 1;
reconsider J = ].inf I,sup I.[ as non empty Subset of REAL
by A3,XXREAL_1:33;
inf I is R_eal & sup I is R_eal by XXREAL_0:def 1; then
reconsider J as non empty open_interval Subset of REAL
by MEASURE5:def 2;
J = ].inf J,sup J.[ by MEASURE6:16; then
inf J < sup J by XXREAL_1:28; then
F is_antiderivative_of f,J & G is_antiderivative_of f,J
by A1,A2,Th42,FDIFF_12:2; then
consider c be Real such that
A4: for x be Real st x in J holds F.x = G.x + c by Lm5;
take c;
I c= dom F & I c= dom G by A1,A2,FDIFF_12:def 1; then
A5: I = dom(F|I) & I = dom(G|I) by RELAT_1:62;
per cases by MEASURE5:1;
suppose I is open_interval; then
I = ].inf I,sup I.[ by MEASURE6:16;
hence for x be Real st x in I holds F.x = G.x + c by A4;
end;
suppose I is closed_interval; then
A6: I = [.inf I,sup I.] by MEASURE6:17; then
A7: inf I in I & sup I in I by A3,XXREAL_1:1;
A8: inf I = lower_bound I & sup I = upper_bound I
by A3,A6,Th1,Th2,XXREAL_1:1; then
(F|I) is_continuous_in lower_bound I &
(F|I) is_continuous_in upper_bound I &
(G|I) is_continuous_in lower_bound I &
(G|I) is_continuous_in upper_bound I
by A5,A7,A1,A2,FDIFF_12:37,FCONT_1:def 2; then
A9: (F|I) is_Rcontinuous_in lower_bound I &
(F|I) is_Lcontinuous_in upper_bound I &
(G|I) is_Rcontinuous_in lower_bound I &
(G|I) is_Lcontinuous_in upper_bound I by A5,A7,A8,FDIFF_12:26;
A10: for r be Real st r < upper_bound I
ex g be Real st r < g & g < upper_bound I & g in dom(F|I)
proof
let r be Real;
assume A11: r < upper_bound I;
set r1 = max(r,lower_bound I);
consider g be Real such that
A12: r1 < g & g < upper_bound I by A11,A8,A3,XXREAL_0:29,XREAL_1:5;
take g;
r <= r1 & lower_bound I <= r1 by XXREAL_0:25; then
r < g & lower_bound I < g by A12,XXREAL_0:2;
hence r < g & g < upper_bound I & g in dom(F|I)
by A12,A8,A6,A5,XXREAL_1:1;
end; then
A13: F|I is_left_convergent_in upper_bound I &
lim_left(F|I,upper_bound I) = (F|I).(upper_bound I)
by A9,FDIFF_12:30;
A14: G|I is_left_convergent_in upper_bound I &
lim_left(G|I,upper_bound I) = (G|I).(upper_bound I)
by A5,A9,A10,FDIFF_12:30;
for e be Real st 0 < e
ex x2 be Real st x2 < upper_bound I &
for x be Real st x2 < x & x < upper_bound I & x in dom(F|I) holds
|. (F|I).x - ((G|I).(upper_bound I)+c) .| < e
proof
let e be Real;
assume 0 < e; then
consider x1 be Real such that
A15: x1 < upper_bound I &
for x be Real st x1 < x & x < upper_bound I & x in dom(G|I) holds
|. (G|I).x - (G|I).(upper_bound I) .| < e by A14,LIMFUNC2:41;
set x2 = max(x1,lower_bound I);
take x2;
thus
x2 < upper_bound I by A15,A3,A8,XXREAL_0:29;
thus for x be Real st x2 < x & x < upper_bound I & x in dom(F|I) holds
|. (F|I).x - ((G|I).(upper_bound I)+c) .| < e
proof
let x be Real;
assume that
A16: x2 < x and
A17: x < upper_bound I and
A18: x in dom(F|I);
x1 <= x2 by XXREAL_0:25; then
A19: x1 < x by A16,XXREAL_0:2;
lower_bound I <= x2 by XXREAL_0:25; then
lower_bound I < x by A16,XXREAL_0:2; then
F.x = G.x + c by A4,A17,A8,XXREAL_1:4; then
(F|I).x = G.x + c by A18,FUNCT_1:47; then
(F|I).x = (G|I).x + c by A18,A5,FUNCT_1:47; then
(F|I).x - ((G|I).(upper_bound I)+c)
= (G|I).x - (G|I).(upper_bound I);
hence thesis by A15,A17,A18,A19,A5;
end;
end; then
(F|I).(upper_bound I) = (G|I).(upper_bound I) + c by A13,LIMFUNC2:41; then
A20: F.(upper_bound I) = (G|I).(upper_bound I) + c
by A6,A8,A3,XXREAL_1:1,FUNCT_1:49;
A21: for r be Real st lower_bound I < r
ex g be Real st g < r & lower_bound I < g & g in dom(F|I)
proof
let r be Real;
assume A22: lower_bound I < r;
set r1 = min(r,upper_bound I);
consider g be Real such that
A23: lower_bound I < g & g < r1 by A22,A8,A3,XXREAL_0:21,XREAL_1:5;
take g;
r1 <= r & r1 <= upper_bound I by XXREAL_0:17; then
g < r & g < upper_bound I by A23,XXREAL_0:2;
hence g < r & lower_bound I < g & g in dom(F|I)
by A6,A8,A5,A23,XXREAL_1:1;
end; then
A24: F|I is_right_convergent_in lower_bound I &
lim_right(F|I,lower_bound I) = (F|I).(lower_bound I)
by A9,FDIFF_12:31;
A25: G|I is_right_convergent_in lower_bound I &
lim_right(G|I,lower_bound I) = (G|I).(lower_bound I)
by A5,A9,A21,FDIFF_12:31;
for e be Real st 0 < e
ex x2 be Real st lower_bound I < x2 &
for x be Real st x < x2 & lower_bound I < x & x in dom(F|I) holds
|. (F|I).x - ((G|I).(lower_bound I)+c) .| < e
proof
let e be Real;
assume 0 < e; then
consider x1 be Real such that
A26: lower_bound I < x1 &
for x be Real st x < x1 & lower_bound I < x & x in dom(G|I) holds
|. (G|I).x - (G|I).(lower_bound I) .| < e by A25,LIMFUNC2:42;
set x2 = min(x1,upper_bound I);
take x2;
thus lower_bound I < x2 by A26,A3,A8,XXREAL_0:21;
thus for x be Real st x < x2 & lower_bound I < x & x in dom(F|I) holds
|. (F|I).x - ((G|I).(lower_bound I)+c) .| < e
proof
let x be Real;
assume that
A27: x < x2 and
A28: lower_bound I < x and
A29: x in dom(F|I);
x2 <= x1 by XXREAL_0:17; then
A30: x < x1 by A27,XXREAL_0:2;
x2 <= upper_bound I by XXREAL_0:17; then
x < upper_bound I by A27,XXREAL_0:2; then
F.x = G.x + c by A4,A28,A8,XXREAL_1:4; then
(F|I).x = G.x + c by A29,FUNCT_1:47; then
(F|I).x = (G|I).x + c by A29,A5,FUNCT_1:47; then
(F|I).x - ((G|I).(lower_bound I)+c)
= (G|I).x - (G|I).(lower_bound I);
hence thesis by A26,A28,A29,A30,A5;
end;
end; then
(F|I).(lower_bound I) = (G|I).(lower_bound I) + c by A24,LIMFUNC2:42; then
A31: F.(lower_bound I) = (G|I).(lower_bound I) + c
by A6,A8,A3,XXREAL_1:1,FUNCT_1:49;
hereby let x be Real;
assume x in I; then
A32: lower_bound I <= x & x <= upper_bound I by A6,A8,XXREAL_1:1;
now assume x <> lower_bound I & x <> upper_bound I; then
lower_bound I < x & x < upper_bound I by A32,XXREAL_0:1;
hence F.x = G.x + c by A4,A8,XXREAL_1:4;
end;
hence F.x = G.x + c by A20,A31,A6,A8,A3,XXREAL_1:1,FUNCT_1:49;
end;
end;
suppose I is left_open_interval; then
A33: I = ].inf I,sup I.] by MEASURE6:19; then
A34: sup I in I by A3,XXREAL_1:2;
A35: sup I = upper_bound I by A3,A33,Th2,XXREAL_1:2; then
(F|I) is_continuous_in upper_bound I &
(G|I) is_continuous_in upper_bound I
by A5,A34,A1,A2,FDIFF_12:37,FCONT_1:def 2; then
A36: (F|I) is_Lcontinuous_in upper_bound I &
(G|I) is_Lcontinuous_in upper_bound I by A5,A34,A35,FDIFF_12:26;
A37: for r be Real st r < upper_bound I
ex g be Real st r < g & g < upper_bound I & g in dom(F|I)
proof
let r be Real;
assume A38: r < upper_bound I;
set r1 = max(r,inf I);
r1 is R_eal & upper_bound I is R_eal by XXREAL_0:def 1; then
consider g be Real such that
A39: r1 < g & g < upper_bound I by A38,A35,A3,Th18,XXREAL_0:29;
take g;
r <= r1 & inf I <= r1 by XXREAL_0:25; then
r < g & inf I < g by A39,XXREAL_0:2;
hence r < g & g < upper_bound I & g in dom(F|I)
by A33,A35,A5,A39,XXREAL_1:2;
end; then
A40: F|I is_left_convergent_in upper_bound I &
lim_left(F|I,upper_bound I) = (F|I).(upper_bound I)
by A36,FDIFF_12:30;
A41: G|I is_left_convergent_in upper_bound I &
lim_left(G|I,upper_bound I) = (G|I).(upper_bound I)
by A5,A36,A37,FDIFF_12:30;
for e be Real st 0 < e
ex x2 be Real st x2 < upper_bound I &
for x be Real st x2 < x & x < upper_bound I & x in dom(F|I) holds
|. (F|I).x - ((G|I).(upper_bound I)+c) .| < e
proof
let e be Real;
assume 0 < e; then
consider x1 be Real such that
A42: x1 < upper_bound I &
for x be Real st x1 < x & x < upper_bound I & x in dom(G|I) holds
|. (G|I).x - (G|I).(upper_bound I) .| < e by A41,LIMFUNC2:41;
set x2 = max(x1,inf I);
A43: x1 <= x2 & x2 < upper_bound I by A42,A3,A35,XXREAL_0:25,29;
-infty < x1 & upper_bound I < +infty by XREAL_0:def 1,XXREAL_0:9,12; then
x2 in REAL by A43,XXREAL_0:14; then
reconsider x2 as Real;
take x2;
thus x2 < upper_bound I by A42,A3,A35,XXREAL_0:29;
thus for x be Real st x2 < x & x < upper_bound I & x in dom(F|I) holds
|. (F|I).x - ((G|I).(upper_bound I)+c) .| < e
proof
let x be Real;
assume that
A44: x2 < x and
A45: x < upper_bound I and
A46: x in dom(F|I);
x1 <= x2 by XXREAL_0:25; then
A47: x1 < x by A44,XXREAL_0:2;
inf I <= x2 by XXREAL_0:25; then
inf I < x by A44,XXREAL_0:2; then
F.x = G.x + c by A4,A45,A35,XXREAL_1:4; then
(F|I).x = G.x + c by A46,FUNCT_1:47; then
(F|I).x = (G|I).x + c by A46,A5,FUNCT_1:47; then
(F|I).x - ((G|I).(upper_bound I)+c)
= (G|I).x - (G|I).(upper_bound I);
hence thesis by A42,A45,A46,A47,A5;
end;
end; then
(F|I).(upper_bound I) = (G|I).(upper_bound I) + c by A40,LIMFUNC2:41; then
A48: F.(upper_bound I) = (G|I).(upper_bound I) + c
by A33,A35,A3,XXREAL_1:2,FUNCT_1:49;
hereby let x be Real;
assume x in I; then
A49: inf I < x & x <= upper_bound I by A33,A35,XXREAL_1:2;
now assume x <> upper_bound I; then
inf I < x & x < upper_bound I by A49,XXREAL_0:1;
hence F.x = G.x + c by A4,A35,XXREAL_1:4;
end;
hence F.x = G.x + c by A48,A33,A35,A3,XXREAL_1:2,FUNCT_1:49;
end;
end;
suppose I is right_open_interval; then
A50: I = [.inf I,sup I.[ by MEASURE6:18; then
A51: inf I in I by A3,XXREAL_1:3;
A52: inf I = lower_bound I by A50,A3,Th1,XXREAL_1:3; then
(F|I) is_continuous_in lower_bound I &
(G|I) is_continuous_in lower_bound I
by A5,A51,A1,A2,FDIFF_12:37,FCONT_1:def 2; then
A53: (F|I) is_Rcontinuous_in lower_bound I &
(G|I) is_Rcontinuous_in lower_bound I by A5,A51,A52,FDIFF_12:26;
A54: for r be Real st lower_bound I < r
ex g be Real st g < r & lower_bound I < g & g in dom(F|I)
proof
let r be Real;
assume A55: lower_bound I < r;
set r1 = min(r,sup I);
r1 is R_eal & lower_bound I is R_eal by XXREAL_0:def 1; then
consider g be Real such that
A56: lower_bound I < g & g < r1 by A55,A52,A3,Th18,XXREAL_0:21;
take g;
r1 <= r & r1 <= sup I by XXREAL_0:17; then
g < r & g < sup I by A56,XXREAL_0:2;
hence g < r & lower_bound I < g & g in dom(F|I)
by A52,A50,A5,A56,XXREAL_1:3;
end; then
A57: F|I is_right_convergent_in lower_bound I &
lim_right(F|I,lower_bound I) = (F|I).(lower_bound I)
by A53,FDIFF_12:31;
A58: G|I is_right_convergent_in lower_bound I &
lim_right(G|I,lower_bound I) = (G|I).(lower_bound I)
by A5,A53,A54,FDIFF_12:31;
for e be Real st 0 < e
ex x2 be Real st lower_bound I < x2 &
for x be Real st x < x2 & lower_bound I < x & x in dom(F|I) holds
|. (F|I).x - ((G|I).(lower_bound I)+c) .| < e
proof
let e be Real;
assume 0 < e; then
consider x1 be Real such that
A59: lower_bound I < x1 &
for x be Real st x < x1 & lower_bound I < x & x in dom(G|I) holds
|. (G|I).x - (G|I).(lower_bound I) .| < e by A58,LIMFUNC2:42;
set x2 = min(x1,sup I);
A60: x2 <= x1 & lower_bound I < x2 by A59,A3,A52,XXREAL_0:17,21;
x1 < +infty & lower_bound I > -infty by XREAL_0:def 1,XXREAL_0:9,12; then
x2 in REAL by A60,XXREAL_0:14; then
reconsider x2 as Real;
take x2;
thus lower_bound I < x2 by A59,A3,A52,XXREAL_0:21;
thus for x be Real st x < x2 & lower_bound I < x & x in dom(F|I) holds
|. (F|I).x - ((G|I).(lower_bound I)+c) .| < e
proof
let x be Real;
assume that
A61: x < x2 and
A62: lower_bound I < x and
A63: x in dom(F|I);
x2 <= x1 by XXREAL_0:17; then
A64: x < x1 by A61,XXREAL_0:2;
x2 <= sup I by XXREAL_0:17; then
x < sup I by A61,XXREAL_0:2; then
F.x = G.x + c by A4,A62,A52,XXREAL_1:4; then
(F|I).x = G.x + c by A63,FUNCT_1:47; then
(F|I).x = (G|I).x + c by A63,A5,FUNCT_1:47; then
(F|I).x - ((G|I).(lower_bound I)+c)
= (G|I).x - (G|I).(lower_bound I);
hence thesis by A59,A62,A63,A64,A5;
end;
end; then
(F|I).(lower_bound I) = (G|I).(lower_bound I) + c by A57,LIMFUNC2:42; then
A65: F.(lower_bound I) = (G|I).(lower_bound I) + c
by A50,A52,A3,XXREAL_1:3,FUNCT_1:49;
hereby let x be Real;
assume x in I; then
A66: lower_bound I <= x & x < sup I by A50,A52,XXREAL_1:3;
now assume x <> lower_bound I; then
lower_bound I < x & x < sup I by A66,XXREAL_0:1;
hence F.x = G.x + c by A4,A52,XXREAL_1:4;
end;
hence F.x = G.x + c by A65,A50,A52,A3,XXREAL_1:3,FUNCT_1:49;
end;
end;
end;
:: Integration by substitution
theorem
for a,b,p,q be Real, f,g be PartFunc of REAL,REAL st
a < b & p < q & [.a,b.] c= dom f & f|['a,b'] is continuous &
g is_differentiable_on_interval ['p,q'] &
g`\['p,q'] is_integrable_on ['p,q'] & g`\['p,q'] is bounded &
rng(g|['p,q']) c= ['a,b'] & g.p = a & g.q = b
holds integral(f,a,b) = integral((f*g)(#)(g`\['p,q']),p,q)
proof
let a,b,p,q be Real, f,g be PartFunc of REAL,REAL;
assume that
A1: a < b and
A2: p < q and
A3: [.a,b.] c= dom f and
A4: f|['a,b'] is continuous and
A5: g is_differentiable_on_interval ['p,q'] and
A6: g`\['p,q'] is_integrable_on ['p,q'] and
A7: g`\['p,q'] is bounded and
A8: rng(g|['p,q']) c= ['a,b'] and
A9: g.p = a and
A10: g.q = b;
A11:['a,b'] = [.a,b.] & ['p,q'] = [.p,q.] by A1,A2,INTEGRA5:def 3;
reconsider I = ['a,b'], J = ['p,q'] as non empty closed_interval
Subset of REAL;
consider F be PartFunc of REAL,REAL such that
A12: dom F = REAL &
for x be Real st x in I holds F.x = integral(f,a,x) by Lm1;
A13:F is_differentiable_on_interval I & F`\I = f|I by A1,A11,A4,A3,A12,Th37;
A14: g.:J = rng(g|J) by RELAT_1:115; then
A15: F*g is_differentiable_on_interval J &
(F*g)`\J = ((F`\I)*g)(#)(g`\J) by A8,A13,A5,FDIFF_12:52;
A16:g|J is continuous by A5,FDIFF_12:37;
A17:J c= dom g by A5,FDIFF_12:def 1;
A18: dom(f|I) = I by A3,A11,RELAT_1:62; then
A19: J c= dom((f|I)*g) by A8,A14,A17,FUNCT_1:101;
A20:J = dom(g`\J) by A5,FDIFF_12:def 2; then
A21: (g`\J)|J = g`\J;
A22: (g`\J)|J is bounded by A7;
(f|I)*(g|J) is continuous by A4,A16; then
((f|I)*g)|J is continuous by RELAT_1:83; then
A23: ((f|I)*g)|J is bounded by A19,INTEGRA5:10; then
(((f|I)*g)(#)(g`\J))|(J /\ J) is bounded by A22,RFUNCT_1:84; then
A24: (F*g)`\J is bounded by A13,A15,A21,RFUNCT_1:45;
(f|I)|(g.:J) is continuous by A4; then
(f|I)*g is_integrable_on J by A19,A16,FCONT_1:25,INTEGRA5:11; then
A25:integral(((f|I)*g)(#)(g`\J),J) = (F*g).q - (F*g).p
by A6,A19,A20,A23,A7,A13,A2,A15,A24,Lm4,INTEGRA6:14;
f is_integrable_on I by A3,A4,A11,INTEGRA5:11; then
A26: f|I is_integrable_on I;
integral(f|I,I) = F.b - F.a
by A3,A4,A11,A1,A26,A13,Lm4,INTEGRA5:10; then
A27: integral(f,I) = F.b - F.a;
(f|I)*(g|J) = f*(g|J) by A18,A8,RELAT_1:165; then
A28: ((f|I)*g)|J = f*(g|J) by RELAT_1:83;
integral(((f|I)*g)(#)(g`\J),J)
= integral( ((((f|I)*g)(#)(g`\J))|J)||J)
.= integral( ((((f|I)*g)|J) (#)(g`\J))||J) by RFUNCT_1:45
.= integral( (((f*g)|J) (#)(g`\J))||J) by A28,RELAT_1:83
.= integral( (((f*g)(#)(g`\J)) |J) ||J) by RFUNCT_1:45; then
A29: integral(((f|I)*g)(#)(g`\J),J) = integral((f*g)(#)(g`\J),J);
p in dom g & q in dom g by A11,A17,A2,XXREAL_1:1; then
(F*g).q = F.b & (F*g).p = F.a by A9,A10,FUNCT_1:13; then
integral(((f|I)*g)(#)(g`\J),J) = integral(f,a,b)
by A27,A11,A25,INTEGRA5:19;
hence integral(f,a,b) = integral((f*g)(#)(g`\['p,q']),p,q)
by A11,A29,INTEGRA5:19;
end;
:: Integration by parts
theorem
for a,b be Real, f,g be PartFunc of REAL,REAL st
a < b & f is_differentiable_on_interval ['a,b'] &
g is_differentiable_on_interval ['a,b'] &
f`\['a,b'] is_integrable_on ['a,b'] & f`\['a,b'] is bounded &
g`\['a,b'] is_integrable_on ['a,b'] & g`\['a,b'] is bounded holds
integral((f`\['a,b'])(#)g,a,b)
= f.b * g.b - f.a * g.a - integral(f(#)(g`\['a,b']),a,b)
proof
let a,b be Real, f,g be PartFunc of REAL,REAL;
assume that
A1: a < b and
A2: f is_differentiable_on_interval ['a,b'] and
A3: g is_differentiable_on_interval ['a,b'] and
A4: f`\['a,b'] is_integrable_on ['a,b'] and
A5: f`\['a,b'] is bounded and
A6: g`\['a,b'] is_integrable_on ['a,b'] and
A7: g`\['a,b'] is bounded;
reconsider I = ['a,b'] as non empty closed_interval Subset of REAL;
f(#)g is_differentiable_on_interval I by A2,A3,FDIFF_12:24; then
A8: dom((f(#)g)`\I) = I by FDIFF_12:def 2;
A9: (f(#)g)`\I = (f`\I)(#)g + f(#)(g`\I) by A2,A3,FDIFF_12:24;
A10:I c= dom f & I c= dom g by A2,A3,FDIFF_12:def 1; then
A11:f||I is Function of I,REAL & g||I is Function of I,REAL
by INTEGRA5:6,FUNCT_2:68;
A12:f is_integrable_on I & g is_integrable_on I
by A10,A2,A3,FDIFF_12:37,INTEGRA5:11;
A13:I = dom(f`\I) & I = dom(g`\I) by A2,A3,FDIFF_12:def 2; then
A14:(f`\I)||I is Function of I,REAL & (g`\I)||I is Function of I,REAL
by INTEGRA5:6,FUNCT_2:68;
A15: (f`\I)|I is bounded & (g`\I)|I is bounded by A5,A7;
f|I is bounded & g|I is bounded by A2,A10,A3,FDIFF_12:37,INTEGRA5:10; then
A16:(f(#)(g`\I))|(I /\ I) is bounded & ((f`\I)(#)g)|(I /\ I) is bounded
by A15,RFUNCT_1:84; then
A17:(f(#)(g`\I))||I|I is bounded & ((f`\I)(#)g)||I|I is bounded;
A18: (g`\I)||I is integrable & (g`\I)||I|I is bounded by A6,A7;
A19: (f`\I)||I is integrable & (f`\I)||I|I is bounded by A4,A5;
dom ((f`\I)(#)g) = dom (f`\I) /\ dom g &
dom (f(#)(g`\I)) = dom f /\ dom (g`\I) by VALUED_1:def 4; then
I = dom((f`\I)(#)g) & I = dom(f(#)(g`\I)) by A10,A13,XBOOLE_1:28; then
A20:((f`\I)(#)g)||I is Function of I, REAL &
(f(#)(g`\I))||I is Function of I,REAL by INTEGRA5:6,FUNCT_2:68;
((f`\I)(#)g + f(#)(g`\I))|(I /\ I) is bounded by A16,RFUNCT_1:83; then
A21: ((f(#)g)`\I)|I is bounded by A2,A3,FDIFF_12:24;
A22: (f(#)g).b = f.b * g.b & (f(#)g).a = f.a * g.a by VALUED_1:5;
f||I|I is bounded & g||I|I is bounded
by A2,A10,A3,FDIFF_12:37,INTEGRA5:10; then
(f||I)(#)((g`\I)||I) is integrable & ((f`\I)||I)(#)(g||I) is integrable
by A14,A18,A12,A11,A19,INTEGRA4:29; then
(f(#)(g`\I))||I is integrable & ((f`\I)(#)g)||I is integrable
by INTEGRA5:4; then
((f`\I)(#)g)||I+(f(#)(g`\I))||I is integrable &
integral(((f`\I)(#)g)||I + (f(#)(g`\I))||I) =integral(((f`\I)(#)g)||I)
+ integral((f(#)(g`\I))||I) by A20,A17,INTEGRA1:57; then
A23:(f(#)g)`\I is_integrable_on I &
integral(((f`\I)(#)g+f(#)(g`\I))||I) = integral((f`\I)(#)g,I)
+ integral(f(#)(g`\I),I) by A9,INTEGRA5:5; then
integral((f(#)g)`\I,I) = (f(#)g).b - (f(#)g).a
by A1,A2,A3,A8,A21,Lm4,FDIFF_12:24; then
integral((f`\['a,b'])(#)g,a,b) = f.b * g.b - f.a * g.a
- integral(f(#)(g`\['a,b']),I) by A1,A9,A22,A23,INTEGRA5:def 4;
hence thesis by A1,INTEGRA5:def 4;
end;