:: The {T}aylor Expansions
:: by Yasunari Shidama
::
:: Received February 24, 2004
:: Copyright (c) 2004-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, INT_1, RAT_1, PARTFUN1, PREPOWER, FUNCT_1, REAL_1,
SUBSET_1, ARYTM_3, RELAT_1, CARD_1, NEWTON, COMPLEX1, XXREAL_0, FDIFF_1,
ARYTM_1, RCOMP_1, TARSKI, XBOOLE_0, VALUED_1, SIN_COS, SEQ_2, ORDINAL2,
FCONT_1, FUNCT_2, POWER, SERIES_1, REALSET1, NAT_1, CARD_3, LIMFUNC1,
SEQFUNC, SEQ_1, XXREAL_1, TAYLOR_1, IRRAT_1, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
IRRAT_1, LIMFUNC1, RCOMP_1, FCONT_1, XCMPLX_0, XXREAL_0, XREAL_0,
COMPLEX1, RAT_1, ORDINAL1, NUMBERS, REAL_1, INT_1, NAT_1, NEWTON,
VALUED_1, PARTFUN2, SEQ_1, SEQ_2, SERIES_1, FDIFF_1, SEQFUNC, PREPOWER,
POWER, SIN_COS;
constructors PARTFUN1, ARYTM_0, REAL_1, NAT_1, SEQ_2, RCOMP_1, PARTFUN2,
RFUNCT_2, FCONT_1, LIMFUNC1, FDIFF_1, SEQFUNC, PREPOWER, COMSEQ_3,
SIN_COS, XXREAL_2, SERIES_1, VALUED_1, POWER, RELSET_1, ABIAN, COMSEQ_2;
registrations XBOOLE_0, RELSET_1, PARTFUN1, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
INT_1, RAT_1, MEMBERED, RCOMP_1, NEWTON, PREPOWER, SIN_COS, VALUED_0,
VALUED_1, FUNCT_2, XXREAL_2, ORDINAL1, SEQ_4, FCONT_3;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities SUBSET_1, LIMFUNC1;
expansions FUNCT_2;
theorems XBOOLE_1, ABSVALUE, TARSKI, XBOOLE_0, PARTFUN1, PARTFUN2, XCMPLX_1,
RELAT_1, CARD_4, RCOMP_1, SEQ_1, SEQ_2, SIN_COS, SERIES_1, FUNCT_1,
NAT_1, INT_1, NEWTON, RAT_1, IRRAT_1, POWER, FCONT_1, FDIFF_1, FDIFF_2,
ROLLE, SEQ_4, PREPOWER, FUNCT_2, XREAL_0, XREAL_1, XXREAL_0, ORDINAL1,
VALUED_1, XXREAL_1, XXREAL_2;
schemes SEQ_1, RECDEF_1, NAT_1, INT_1, PARTFUN2, FUNCT_2;
begin :: The Logarithmic differentiation method
reserve n for Nat,
i for Integer,
p, x, x0, y for Real,
q for Rational,
f for PartFunc of REAL,REAL;
definition
let q be Integer;
func #Z q -> Function of REAL, REAL means
:Def1:
for x be Real holds it.x = x #Z q;
existence
proof
deffunc U(Real) = In($1 #Z q,REAL);
consider f being Function of REAL,REAL such that
A1: for d be Element of REAL holds f.d = U(d) from FUNCT_2:sch 4;
take f;
let d be Real;
d in REAL by XREAL_0:def 1;
then f.d = U(d) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of REAL, REAL;
assume that
A2: for d be Real holds f1.d=d #Z q and
A3: for d be Real holds f2.d=d #Z q;
for d being Element of REAL holds f1.d = f2.d
proof
let d be Element of REAL;
thus f1.d=d #Z q by A2
.=f2.d by A3;
end;
hence f1=f2;
end;
end;
theorem Th1:
for m,n be Nat holds x #Z (n+m) = (x #Z n) * (x #Z m)
proof
let m,n be Nat;
per cases;
suppose
x <> 0;
hence thesis by PREPOWER:44;
end;
suppose
A1: x = 0;
thus thesis
proof
A2: 0 #Z (n+m) = 0|^|.n+m.| by PREPOWER:def 3
.= 0|^(n+m) by ABSVALUE:def 1
.= 0|^n*0|^m by NEWTON:8;
per cases;
suppose
A3: n = 0 & m = 0;
x #Z (0+0) = 1 * (x #Z 0) .= (x #Z 0) * (x #Z 0) by PREPOWER:34;
hence thesis by A3;
end;
suppose
n <> 0;
then
A4: 0+1 <= n by NAT_1:13;
A5: (0 #Z n) *(0 #Z m) = (0 |^ |.n.|) * (0 #Z m) by PREPOWER:def 3
.= (0 |^ n) * (0 #Z m) by ABSVALUE:def 1
.= 0 * (0 #Z m) by A4,NEWTON:11;
0 #Z (n+m) = 0*0|^m by A2,A4,NEWTON:11;
hence thesis by A1,A5;
end;
suppose
m <> 0;
then
A6: 0+1 <= m by NAT_1:13;
A7: (0 #Z n) *(0 #Z m) = (0 |^ |.m.|) * (0 #Z n) by PREPOWER:def 3
.= (0 |^ m) * (0 #Z n) by ABSVALUE:def 1
.= 0 * (0 #Z n) by A6,NEWTON:11;
0 #Z (n+m) = 0*0|^n by A2,A6,NEWTON:11;
hence thesis by A1,A7;
end;
end;
end;
end;
theorem Th2:
#Z n is_differentiable_in x & diff(( #Zn),x) = n * x #Z (n-1)
proof
defpred P[Nat] means for x be Real holds #Z $1
is_differentiable_in x & diff( ( #Z $1),x) = $1 * x #Z ($1 -1);
A1: for k be Nat st P[k] holds P[k+1]
proof
A2: now
let x be Real such that
x in REAL;
thus ( #Z 1).x=x #Z 1 by Def1
.=1*x + 0 by PREPOWER:35;
end;
A3: [#]REAL is open Subset of REAL;
A4: REAL c= dom ( #Z 1) by FUNCT_2:def 1;
then
A5: ( #Z 1) is_differentiable_on REAL by A2,A3,FDIFF_1:23;
A6: for x be Real holds ( #Z 1) is_differentiable_in x & diff(( #Z
1), x)=1
proof
let x be Real;
A7: x in REAL by XREAL_0:def 1;
hence ( #Z 1) is_differentiable_in x by A3,A5,FDIFF_1:9;
thus diff(( #Z 1), x)=( ( #Z 1)`|REAL).x by A5,A7,FDIFF_1:def 7
.=1 by A2,A4,A3,A7,FDIFF_1:23;
end;
let k be Nat such that
A8: P[k];
now
per cases;
case
A9: k = 0;
thus P[k+1]
proof
let x be Real;
thus #Z (k+1) is_differentiable_in x by A6,A9;
thus diff(( #Z (k+1)), x)=1 by A6,A9
.=(k+1)*x #Z ((k+1)-1) by A9,PREPOWER:34;
end;
end;
case
k<> 0;
then 1 <= k by NAT_1:14;
then 1-1 <=k-1 by XREAL_1:13;
then reconsider k1=k-1 as Element of NAT by INT_1:3;
let x be Real;
A10: REAL = dom( #Z (k+1)) by FUNCT_2:def 1;
A11: x is Real & ( #Z k) is_differentiable_in x by A8;
A12: for x be object st x in dom( #Z (k+1)) holds ( #Z (k+1)).x=( #Z k).x
* ( #Z 1).x
proof
let x be object;
assume x in dom( #Z (k+1));
then reconsider x1 = x as Real;
thus ( #Z (k+1)).x = x1 #Z (k+1) by Def1
.=(x1 #Z k) * (x1 #Z 1) by Th1
.=( #Z k).x * x1 #Z (1) by Def1
.=( #Z k).x *( #Z 1).x by Def1;
end;
A13: ( #Z 1) is_differentiable_in x by A6;
A14: dom(( #Z k)) /\ dom(( #Z 1)) =[#]REAL /\ dom(( #Z 1)) by FUNCT_2:def 1
.=[#]REAL /\ REAL by FUNCT_2:def 1;
then ( #Z (k+1)) = ( #Z k) (#) ( #Z 1) by A10,A12,VALUED_1:def 4;
hence #Z (k+1) is_differentiable_in x by A11,A13,FDIFF_1:16;
thus diff(( #Z (k+1)), x) = diff( ( #Z k) (#) ( #Z 1),x) by A14,A10,A12
,VALUED_1:def 4
.= ( #Z k).x *diff(( #Z 1),x)+diff(( #Z k),x)*( #Z 1).x by A11,A13,
FDIFF_1:16
.= ( #Z k).x*1 + diff( #Z k,x)*( #Z 1).x by A6
.= (x #Z k)*1 + diff( #Z k,x)*( #Z 1).x by Def1
.= (x #Z k)*1 + diff( #Z k,x)*(x #Z 1) by Def1
.= (x #Z k)+k*(x #Z k1)*(x #Z 1) by A8
.= (x #Z k)+k*((x #Z k1)*(x #Z 1))
.= (x #Z k)+k*(x #Z (k1+1)) by Th1
.= (k+1) * x #Z ((k+1)-1);
end;
end;
hence thesis;
end;
A15: P[0]
proof
let x be Real;
set f= #Z 0;
now
dom(f)=REAL by FUNCT_2:def 1;
then consider x be object such that
A16: x in dom(f) by XBOOLE_0:def 1;
reconsider x1=x as Real by A16;
let y be object such that
A17: y in {1};
f.x=x1 #Z 0 by Def1
.=1 by PREPOWER:34
.=y by A17,TARSKI:def 1;
hence y in rng f by A16,FUNCT_1:def 3;
end;
then
A18: {1} c= rng f by TARSKI:def 3;
now
let y be object;
assume y in rng f;
then consider x be object such that
A19: x in dom(f) and
A20: y=f.x by FUNCT_1:def 3;
reconsider x as Real by A19;
f.x =x #Z 0 by Def1
.=1 by PREPOWER:34;
hence y in {1} by A20,TARSKI:def 1;
end;
then rng(f) c= {1} by TARSKI:def 3;
then
A21: rng(f) = {1} by A18,XBOOLE_0:def 10;
A22: dom(f)=[#]REAL by FUNCT_2:def 1;
then
A23: f is_differentiable_on dom(f) by A21,FDIFF_1:11;
A24: x in REAL by XREAL_0:def 1;
then (f`|dom(f)) .x = 0 by A21,A22,FDIFF_1:11;
hence f is_differentiable_in x & diff(f,x)= 0 * x #Z (0-1) by A24,A23,A22,
FDIFF_1:9,def 7;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A15,A1);
hence thesis;
end;
theorem
f is_differentiable_in x0 implies ( #Z n) *f is_differentiable_in x0 &
diff( ( #Z n) *f,x0) = n * (f.x0) #Z (n-1) *diff(f,x0)
proof
assume
A1: f is_differentiable_in x0;
A2: ( #Z n) is_differentiable_in f.x0 & x0 is Real by Th2;
hence ( #Z n)*f is_differentiable_in x0 by A1,FDIFF_2:13;
thus diff(( #Z n)*f,x0) = diff(( #Z n),f.x0)*diff(f,x0) by A1,A2,FDIFF_2:13
.=n * (f.x0) #Z (n-1) *diff(f,x0) by Th2;
end;
Lm1: (exp_R(x)) #R n = exp_R(n*x)
proof
reconsider x as Real;
defpred P[Nat] means (exp_R(x)) #R $1 = exp_R ($1 * x);
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
thus (exp_R(x)) #R (k+1) = (exp_R(x)) #R k * (exp_R(x)) #R 1 by PREPOWER:75
,SIN_COS:55
.= (exp_R(x)) #R k * exp_R(x) by PREPOWER:72,SIN_COS:55
.=exp_R(k1*x+x) by A2,SIN_COS:50
.=exp_R((k+1)*x);
end;
A3: P[0] by PREPOWER:71,SIN_COS:51,55;
for n be Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th4:
exp_R(-x) = 1/exp_R(x)
proof
reconsider x as Real;
exp_R(-x)*exp_R(x)=exp_R((-x)+x) by SIN_COS:50
.=1 by SIN_COS:51;
hence thesis by XCMPLX_1:73;
end;
Lm2: (exp_R(x)) #R i =exp_R(i*x)
proof
consider n be Nat such that
A1: i = n or i = - n by INT_1:2;
now
per cases by A1;
case
i = n;
hence thesis by Lm1;
end;
case
A2: i = -n;
hence exp_R(i*x) =exp_R(-(n*x)) .=1/(exp_R(n*x)) by Th4
.=1/( (exp_R(x)) #R n ) by Lm1
.=(exp_R(x)) #R i by A2,PREPOWER:76,SIN_COS:55;
end;
end;
hence thesis;
end;
theorem Th5:
(exp_R(x)) #R (1/i) = exp_R(x/i)
proof
set n = i;
per cases;
suppose
A1: n <> 0;
then exp_R(x) =exp_R((x/n)*n) by XCMPLX_1:87
.=(exp_R(x/n)) #R n by Lm2;
hence (exp_R(x)) #R (1/n) =(exp_R(x/n)) #R (n* (1/n) ) by PREPOWER:91
,SIN_COS:55
.=(exp_R(x/n)) #R 1 by A1,XCMPLX_1:106
.=exp_R(x/n) by PREPOWER:72,SIN_COS:55;
end;
suppose
A2: n = 0;
(exp_R(x)) #R (1/0) = exp_R(0) by PREPOWER:71,SIN_COS:51,55
.= exp_R(x/0) by XCMPLX_1:49;
hence thesis by A2;
end;
end;
theorem Th6:
for m,n be Integer holds (exp_R(x)) #R (m/n) = exp_R(m/n*x)
proof
let m,n be Integer;
thus exp_R(m/n*x) = exp_R(x/n*m) by XCMPLX_1:75
.=(exp_R(x/n)) #R m by Lm2
.=((exp_R(x)) #R (1/n)) #R m by Th5
.=(exp_R(x)) #R ((1/n)*m) by PREPOWER:91,SIN_COS:55
.=(exp_R(x)) #R ((m/n)*1) by XCMPLX_1:75
.=(exp_R(x)) #R (m/n);
end;
Lm3: (exp_R(x)) #R q = exp_R(q*x)
proof
ex m be Integer,n be Nat st n > 0 & q=m/n by RAT_1:8;
hence thesis by Th6;
end;
theorem Th7:
(exp_R(x)) #Q q = exp_R(q*x)
proof
thus (exp_R(x)) #Q q = (exp_R(x)) #R q by PREPOWER:74,SIN_COS:55
.= exp_R(q*x) by Lm3;
end;
theorem Th8:
(exp_R(x)) #R p = exp_R(p*x)
proof
exp_R(x) > 0 by SIN_COS:55;
then consider s being Rational_Sequence such that
A1: s is convergent & lim s = p and
(exp_R(x)) #Q s is convergent and
A2: lim (exp_R(x)) #Q s = (exp_R(x)) #R p by PREPOWER:def 7;
A3: exp_R is_continuous_in x*p & rng (x(#)s) c= dom (exp_R) by FDIFF_1:24
,SIN_COS:47,65;
A4: now
let ii be object;
assume ii in NAT;
then reconsider i=ii as Element of NAT;
A5: rng (x(#)s) c= dom (exp_R) by SIN_COS:47;
thus ( (exp_R(x)) #Q s ).ii =(exp_R(x)) #Q (s.i) by PREPOWER:def 6
.=exp_R((s.i)*x) by Th7
.=exp_R((x(#)s).i) by SEQ_1:9
.=exp_R.((x(#)s).i) by SIN_COS:def 23
.=(exp_R/*(x(#)s)).ii by A5,FUNCT_2:108;
end;
x(#)s is convergent & lim (x(#)s) = x*p by A1,SEQ_2:7,8;
then lim((exp_R/*(x(#)s)) ) = exp_R.(x*p) by A3,FCONT_1:def 1
.= exp_R(p*x) by SIN_COS:def 23;
hence thesis by A2,A4,FUNCT_2:12;
end;
theorem Th9:
(exp_R(1)) #R x =exp_R(x) & (exp_R(1)) to_power x = exp_R(x) &
number_e to_power x = exp_R(x) & number_e #R x = exp_R(x)
proof
thus
A1: exp_R(x) =exp_R(x*1) .= (exp_R(1)) #R x by Th8;
exp_R(1) > 0 by SIN_COS:55;
hence thesis by A1,IRRAT_1:def 7,POWER:def 2;
end;
theorem
(exp_R.1) #R x =exp_R.x & (exp_R.1) to_power x = exp_R.x & number_e
to_power x = exp_R.x & number_e #R x =exp_R.x
proof
thus (exp_R.1) #R x =(exp_R(1)) #R x by SIN_COS:def 23
.=exp_R(x) by Th9
.=exp_R.x by SIN_COS:def 23;
thus (exp_R.1) to_power x=(exp_R(1)) to_power x by SIN_COS:def 23
.=exp_R(x) by Th9
.=exp_R.x by SIN_COS:def 23;
thus number_e to_power x = exp_R(x) by Th9
.=exp_R.x by SIN_COS:def 23;
thus number_e #R x =exp_R(x) by Th9
.=exp_R.x by SIN_COS:def 23;
end;
theorem
number_e > 2
proof
A1: number_e is irrational by IRRAT_1:41;
A5: for n be Element of NAT st 1<= n holds Partial_Sums(1 rExpSeq).n>=2
proof
defpred X[Integer] means Partial_Sums(1 rExpSeq).$1>=2;
A6: for ni be Integer st 1 <= ni holds X[ni] implies X[ni+1]
proof
let ni be Integer;
assume 1 <=ni;
then reconsider n=ni as Element of NAT by INT_1:3;
A7: Partial_Sums(1 rExpSeq).(n+1) =Partial_Sums(1 rExpSeq).n+(1 rExpSeq
).(n+1) by SERIES_1:def 1
.=Partial_Sums(1 rExpSeq).n+1 |^(n+1)/((n+1)!) by SIN_COS:def 5;
A8: Partial_Sums(1 rExpSeq).n+1 |^(n+1)/((n+1)!)> Partial_Sums(1
rExpSeq).n by XREAL_1:29,139;
assume Partial_Sums(1 rExpSeq).ni>=2;
hence thesis by A7,A8,XXREAL_0:2;
end;
Partial_Sums(1 rExpSeq).1 =Partial_Sums(1 rExpSeq).0+(1 rExpSeq).(0+1)
by SERIES_1:def 1
.=(1 rExpSeq).0+(1 rExpSeq).1 by SERIES_1:def 1
.=(1 rExpSeq).0 + (1 |^ 1 /(1!)) by SIN_COS:def 5
.=1 |^ 0 /(0!) + (1 |^ 1 /(1!)) by SIN_COS:def 5
.=1 + (1 |^ 1 /(1!)) by NEWTON:12
.=1 + 1/1 by NEWTON:13
.=2;
then
A9: X[1];
for n be Integer st 1<=n holds X[n] from INT_1:sch 2(A9,A6);
hence thesis;
end;
A10: for n be Nat holds (Partial_Sums(1 rExpSeq)^\1).n>=2
proof
let n be Nat;
(Partial_Sums(1 rExpSeq)^\1).n = Partial_Sums(1 rExpSeq).(n+1) by
NAT_1:def 3;
hence thesis by A5,NAT_1:11;
end;
(1 rExpSeq) is summable by SIN_COS:45;
then
A11: Partial_Sums(1 rExpSeq) is convergent by SERIES_1:def 2;
lim(Partial_Sums(1 rExpSeq))=Sum(1 rExpSeq) by SERIES_1:def 3;
then lim(Partial_Sums(1 rExpSeq)^\1)=Sum(1 rExpSeq) by A11,SEQ_4:20;
then Sum(1 rExpSeq)>=2 by A10,A11,SIN_COS:38;
then exp_R.1 >=2 by SIN_COS:def 22;
then number_e >= 2 by IRRAT_1:def 7,SIN_COS:def 23;
then number_e > 2 or number_e = 2 by XXREAL_0:1;
hence thesis by A1;
end;
then
Lm4: number_e > 1 by XXREAL_0:2;
registration
cluster number_e -> positive;
coherence by Lm4;
end;
theorem Th12:
log(number_e,exp_R(x)) = x
proof
exp_R(x) > 0 & number_e to_power x =exp_R(x) by Th9,SIN_COS:55;
hence thesis by Lm4,POWER:def 3;
end;
theorem Th13:
log(number_e,exp_R.x) = x
proof
thus log(number_e,exp_R.x) =log(number_e,exp_R(x)) by SIN_COS:def 23
.=x by Th12;
end;
theorem Th14:
y > 0 implies exp_R(log(number_e,y)) = y
proof
assume y > 0;
then number_e to_power log(number_e,y) = y by Lm4,POWER:def 3;
hence thesis by Th9;
end;
theorem Th15:
y > 0 implies exp_R.(log(number_e,y)) = y
proof
assume
A1: y > 0;
thus exp_R.(log(number_e,y)) = exp_R(log(number_e,y)) by SIN_COS:def 23
.= y by A1,Th14;
end;
theorem Th16:
exp_R is one-to-one & exp_R is_differentiable_on REAL & exp_R
is_differentiable_on [#](REAL) &
(for x be Real holds diff(exp_R,x)=exp_R.x) &
(for x be Real holds 0 < diff(exp_R,x)) &
dom(exp_R)=[#]REAL & rng(exp_R)=right_open_halfline(0)
proof
now
let x1,x2 be object such that
A1: x1 in dom exp_R and
A2: x2 in dom exp_R and
A3: exp_R.x1=exp_R.x2;
reconsider p2=x2 as Real by A2;
reconsider p1=x1 as Real by A1;
thus x1=log(number_e,exp_R.p1) by Th13
.=log(number_e,exp_R.p2) by A3
.=x2 by Th13;
end;
hence exp_R is one-to-one by FUNCT_1:def 4;
thus exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#](REAL)
by SIN_COS:66;
thus for x be Real holds diff(exp_R,x)=exp_R.x by SIN_COS:66;
hereby
let x be Real;
diff(exp_R,x)=exp_R.x by SIN_COS:66;
hence diff(exp_R,x) > 0 by SIN_COS:54;
end;
thus dom(exp_R)=[#]REAL by SIN_COS:47;
now
let y be object;
assume y in rng exp_R;
then consider x be object such that
A4: x in dom(exp_R) and
A5: y=exp_R.x by FUNCT_1:def 3;
reconsider y1=y as Real by A5;
reconsider x as Real by A4;
exp_R.x > 0 by SIN_COS:54;
then y1 in {g where g is Real : 0<g} by A5;
hence y in right_open_halfline(0) by XXREAL_1:230;
end;
then
A6: rng(exp_R) c= right_open_halfline(0) by TARSKI:def 3;
now
let y be object;
assume y in right_open_halfline(0);
then y in {g where g is Real : 0<g} by XXREAL_1:230;
then
A7: ex g be Real st y=g & 0 < g;
then reconsider y1=y as Real;
A8: log(number_e,y1) in REAL by XREAL_0:def 1;
y1=exp_R.(log(number_e,y1) ) by A7,Th15;
hence y in rng(exp_R) by FUNCT_1:def 3,SIN_COS:47,A8;
end;
then right_open_halfline(0) c= rng(exp_R) by TARSKI:def 3;
hence rng(exp_R)=right_open_halfline(0) by A6,XBOOLE_0:def 10;
end;
registration
cluster exp_R -> one-to-one;
coherence by Th16;
end;
theorem Th17:
exp_R" is_differentiable_on dom (exp_R") & for x be Real
st x in dom (exp_R") holds diff(((exp_R)"),x) = 1/x
proof
thus exp_R" is_differentiable_on dom (exp_R") by Th16,FDIFF_2:45;
let x be Real such that
A1: x in dom ((exp_R)");
A2: x in rng (exp_R) by A1,FUNCT_1:33;
diff(exp_R, ((exp_R)").x)=exp_R.( ((exp_R)").x) by Th16
.=x by A2,FUNCT_1:35;
hence thesis by A1,Th16,FDIFF_2:45;
end;
registration
cluster right_open_halfline(0) -> non empty;
coherence
proof
1 in {g where g is Real: 0<g};
hence thesis by XXREAL_1:230;
end;
end;
definition
let a be Real;
func log_ a -> PartFunc of REAL,REAL means
:Def2:
dom it =
right_open_halfline(0) & for d be Element of right_open_halfline(0) holds it.d
= log(a,d);
existence
proof
defpred X[set] means $1 in right_open_halfline(0);
reconsider a as Real;
deffunc U(Real) = In(log(a,$1),REAL);
consider f being PartFunc of REAL, REAL such that
A1: for d be Element of REAL holds d in dom f iff X[d] and
A2: for d be Element of REAL st d in dom f holds f/.d = U(d) from
PARTFUN2:sch 2;
take f;
for x be object st x in right_open_halfline(0) holds x in dom f by A1;
then
A3: right_open_halfline(0) c=dom(f) by TARSKI:def 3;
for x be object st x in dom f holds x in right_open_halfline(0) by A1;
then dom(f) c= right_open_halfline(0) by TARSKI:def 3;
hence
A4: dom(f)=right_open_halfline(0) by A3,XBOOLE_0:def 10;
let d be Element of right_open_halfline(0);
f/.d = U(d) by A2,A4;
hence thesis by A4,PARTFUN1:def 6;
end;
uniqueness
proof
let f1,f2 be PartFunc of REAL, REAL;
assume that
A5: dom f1= right_open_halfline(0) and
A6: for d being Element of right_open_halfline(0) holds f1.d=log(a,d) and
A7: dom f2= right_open_halfline(0) and
A8: for d being Element of right_open_halfline(0) holds f2.d=log(a,d);
for d being Element of REAL st d in right_open_halfline(0) holds f1.d
= f2.d
proof
let d be Element of REAL such that
A9: d in right_open_halfline(0);
thus f1.d=log(a,d) by A6,A9
.=f2.d by A8,A9;
end;
hence f1=f2 by A5,A7,PARTFUN1:5;
end;
end;
definition
func ln -> PartFunc of REAL, REAL equals
log_number_e;
correctness;
end;
theorem Th18:
ln=(exp_R)" & ln is one-to-one & dom ln = right_open_halfline(0)
& rng ln = REAL & ln is_differentiable_on right_open_halfline(0) & (for x be
Real st x > 0 holds ln is_differentiable_in x) & (for x be Element of
right_open_halfline(0) holds diff(ln,x)=1/x) & for x be Element of
right_open_halfline(0) holds 0 < diff(ln,x)
proof
A1: for d being Element of REAL st d in right_open_halfline(0) holds ((exp_R
)").d = ln.d
proof
let d be Element of REAL such that
A2: d in right_open_halfline(0);
((exp_R)").d=log(number_e,d)
proof
A3: log(number_e,d) in REAL by XREAL_0:def 1;
d in {g where g is Real: 0<g} by A2,XXREAL_1:230;
then ex g be Real st g=d & g > 0;
then d=exp_R.(log(number_e,d)) by Th15;
hence thesis by Th16,FUNCT_1:32,A3;
end;
hence thesis by A2,Def2;
end;
A4: dom ((exp_R)") = right_open_halfline(0) by Th16,FUNCT_1:33;
then dom ((exp_R)") = dom ln by Def2;
hence
A5: ln=(exp_R)" by A4,A1,PARTFUN1:5;
A6: for x be Real st x > 0 holds ln is_differentiable_in x
proof
let x be Real;
assume x > 0;
then x in {g where g is Real: 0<g};
then x in right_open_halfline(0) by XXREAL_1:230;
hence thesis by A4,A5,Th17,FDIFF_1:9;
end;
A7: for x be Element of right_open_halfline(0) holds 0 < diff(ln,x)
proof
let x be Element of right_open_halfline(0);
x in right_open_halfline(0);
then x in {g where g is Real: 0<g} by XXREAL_1:230;
then
A8: ex g be Real st x=g & 0 < g;
1/x = x" by XCMPLX_1:215;
hence thesis by A4,A5,A8,Th17;
end;
thus ln is one-to-one by A5,FUNCT_1:40;
dom ln = right_open_halfline(0) by Def2;
hence thesis by A5,A6,A7,Th16,Th17,FUNCT_1:33;
end;
theorem
f is_differentiable_in x0 implies exp_R*f is_differentiable_in x0 &
diff(exp_R*f,x0) = exp_R.(f.x0)*diff(f,x0)
proof
assume
A1: f is_differentiable_in x0;
A2: x0 is Real & exp_R is_differentiable_in f.x0 by Th16,FDIFF_1:9
,XREAL_0:def 1;
hence exp_R*f is_differentiable_in x0 by A1,FDIFF_2:13;
thus diff(exp_R*f,x0) = diff(exp_R,f.x0)*diff(f,x0) by A1,A2,FDIFF_2:13
.=exp_R.(f.x0) *diff(f,x0) by Th16;
end;
theorem
f is_differentiable_in x0 & f.x0 > 0 implies ln *f
is_differentiable_in x0 & diff( ln *f,x0) = diff(f,x0)/(f.x0)
proof
assume that
A1: f is_differentiable_in x0 and
A2: f.x0 > 0;
f.x0 in {g where g is Real: 0<g} by A2;
then
A3: f.x0 in right_open_halfline(0) by XXREAL_1:230;
then
A4: ln is_differentiable_in f.x0 by Th18,FDIFF_1:9;
thus ln *f is_differentiable_in x0 by A1,A4,FDIFF_2:13;
thus diff(ln *f,x0) = diff(ln,f.x0)*diff(f,x0) by A1,A4,FDIFF_2:13
.=(1/(f.(x0))) *diff(f,x0) by A3,Th18
.=diff(f,x0)/(f.(x0)) *1 by XCMPLX_1:75
.=diff(f,x0)/(f.(x0));
end;
definition
let p be Real;
func #R p -> PartFunc of REAL,REAL means
:Def4:
dom it = right_open_halfline
(0) & for d be Element of right_open_halfline(0) holds it.d= d #R p;
existence
proof
defpred X[set] means $1 in right_open_halfline(0);
reconsider p as Real;
deffunc U(Real) = In($1 #R p,REAL);
consider f being PartFunc of REAL, REAL such that
A1: for d be Element of REAL holds d in dom f iff X[d] and
A2: for d be Element of REAL st d in dom f holds f/.d = U(d) from
PARTFUN2:sch 2;
take f;
for x be object st x in right_open_halfline(0) holds x in dom f by A1;
then
A3: right_open_halfline(0) c=dom(f) by TARSKI:def 3;
for x be object st x in dom f holds x in right_open_halfline(0) by A1;
then dom(f) c= right_open_halfline(0) by TARSKI:def 3;
hence
A4: dom(f)=right_open_halfline(0) by A3,XBOOLE_0:def 10;
let d be Element of right_open_halfline(0);
f/.d = U(d) by A2,A4;
hence thesis by A4,PARTFUN1:def 6;
end;
uniqueness
proof
let f1,f2 be PartFunc of REAL, REAL;
assume that
A5: dom f1= right_open_halfline(0) and
A6: for d being Element of right_open_halfline(0) holds f1.d=d #R p and
A7: dom f2= right_open_halfline(0) and
A8: for d being Element of right_open_halfline(0) holds f2.d=d #R p;
for d being Element of REAL st d in right_open_halfline(0) holds f1.d
= f2.d
proof
let d be Element of REAL such that
A9: d in right_open_halfline(0);
thus f1.d=d #R p by A6,A9
.=f2.d by A8,A9;
end;
hence f1=f2 by A5,A7,PARTFUN1:5;
end;
end;
theorem Th21:
x > 0 implies ( #R p) is_differentiable_in x & diff(( #R p),x)=p
*(x #R (p-1))
proof
set f= #R p;
A1: for x be Real st 0 < x holds exp_R*(p(#)ln) is_differentiable_in x &
diff(exp_R*(p(#)ln),x) =p*(x #R (p-1))
proof
let x be Real such that
A2: x > 0;
A3: ln is_differentiable_in x by A2,Th18;
then
A4: p(#)ln is_differentiable_in x by FDIFF_1:15;
x in {g where g is Real: 0<g} by A2;
then
A5: x in right_open_halfline(0) by XXREAL_1:230;
then
A6: x in dom (p(#)ln) by Th18,VALUED_1:def 5;
A7: diff((p(#)ln),x) =p*diff(ln,x) by A3,FDIFF_1:15
.=p*(1/x) by A5,Th18;
A8: exp_R is_differentiable_in (p(#)ln).x by SIN_COS:65;
hence exp_R*(p(#)ln) is_differentiable_in x by A4,FDIFF_2:13;
diff(exp_R,(p(#)ln).x) = exp_R.((p(#)ln).x) by Th16
.=exp_R.(p*ln.x ) by A6,VALUED_1:def 5
.=exp_R.(p*log(number_e,x)) by A5,Def2
.=exp_R.(log(number_e,x to_power p)) by A2,Lm4,POWER:55
.=x to_power p by A2,Th15,POWER:34;
hence diff(exp_R*(p(#)ln),x) =(x to_power p) *(p*(1/x) ) by A4,A8,A7,
FDIFF_2:13
.=p*((x to_power p) *(1/x) )
.=p*((x to_power p) *(1/(x to_power 1) ) ) by POWER:25
.=p*((x to_power p) *(x to_power (-1) ) ) by A2,POWER:28
.=p*( x to_power (p+(-1))) by A2,POWER:27
.=p*(x #R (p-1)) by A2,POWER:def 2;
end;
rng (p(#)ln) c= dom exp_R by Th16;
then
A9: dom (exp_R*(p(#)ln)) = dom (p(#)ln) by RELAT_1:27
.=right_open_halfline(0) by Th18,VALUED_1:def 5;
A10: for d being Element of REAL st d in right_open_halfline(0) holds (exp_R
*(p(#)ln)).d = f.d
proof
let d be Element of REAL such that
A11: d in right_open_halfline(0);
A12: d in dom (p(#)ln) by A11,Th18,VALUED_1:def 5;
d in {g where g is Real: 0<g} by A11,XXREAL_1:230;
then
A13: ex g be Real st g=d & g > 0;
thus (exp_R*(p(#)ln)).d = (exp_R*(p(#)ln))/.d by A9,A11,PARTFUN1:def 6
.= exp_R/.((p(#)ln)/.d) by A9,A11,PARTFUN2:3
.= exp_R.((p(#)ln).d) by A12,PARTFUN1:def 6
.=exp_R.(p*ln.d ) by A12,VALUED_1:def 5
.=exp_R.(p*log(number_e,d)) by A11,Def2
.=exp_R.(log(number_e,d to_power p)) by A13,Lm4,POWER:55
.=d to_power p by A13,Th15,POWER:34
.=(d #R p) by A13,POWER:def 2
.=f.d by A11,Def4;
end;
dom(f)=right_open_halfline(0) by Def4;
then x is Real & exp_R*(p(#)ln) = f by A9,A10,PARTFUN1:5;
hence thesis by A1;
end;
theorem
f is_differentiable_in x0 & f.x0 > 0 implies ( #R p) *f
is_differentiable_in x0 & diff( ( #R p) *f,x0) = p*( (f.x0) #R (p-1)) * diff(f,
x0)
proof
assume that
A1: f is_differentiable_in x0 and
A2: f.x0 > 0;
A3: ( #R p) is_differentiable_in f.x0 by A2,Th21;
hence ( #R p) *f is_differentiable_in x0 by A1,FDIFF_2:13;
thus diff( ( #R p) *f,x0) = diff( ( #R p),f.x0)*diff(f,x0) by A1,A3,
FDIFF_2:13
.=p*( (f.x0) #R (p-1))*diff(f,x0) by A2,Th21;
end;
begin :: The Taylor expansions
definition
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
func diff(f,Z) -> Functional_Sequence of REAL,REAL means
:Def5:
it.0 = f|Z & for i be Nat holds it.(i+1) = (it.i) `| Z;
existence
proof
reconsider fZ = f|Z as Element of PFuncs(REAL,REAL) by PARTFUN1:45;
defpred R[set,set,set] means ex h being PartFunc of REAL, REAL st $2 = h &
$3 = h `| Z;
A1: for n being Nat for x being Element of PFuncs(REAL,REAL) ex
y being Element of PFuncs(REAL,REAL) st R[n,x,y]
proof
let n be Nat;
let x be Element of PFuncs (REAL,REAL);
reconsider x9 = x as PartFunc of REAL, REAL by PARTFUN1:46;
reconsider y = x9 `| Z as Element of PFuncs (REAL,REAL) by PARTFUN1:45;
ex h being PartFunc of REAL, REAL st x = h & y = h `| Z;
hence thesis;
end;
consider g be sequence of PFuncs (REAL,REAL) such that
A2: g.0 = fZ & for n being Nat holds R[n,g.n,g.(n+1)] from
RECDEF_1:sch 2(A1);
reconsider g as Functional_Sequence of REAL,REAL;
take g;
thus g.0 = f|Z by A2;
let i be Nat;
R[i,g.i,g.(i+1)] by A2;
hence thesis;
end;
uniqueness
proof
let seq1,seq2 be Functional_Sequence of REAL,REAL;
assume that
A3: seq1.0=f|Z and
A4: for n be Nat holds seq1.(n+1)=( seq1.n )`|Z and
A5: seq2.0=f|Z and
A6: for n be Nat holds seq2.(n+1)=( seq2.n )`|Z;
defpred P[Nat] means seq1.$1 = seq2.$1;
A7: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A8: P[k];
thus seq1.(k+1) = ( seq1.k )`|Z by A4
.= seq2.(k+1) by A6,A8;
end;
A9: P[0] by A3,A5;
for n be Nat holds P[n] from NAT_1:sch 2(A9,A7);
hence seq1 = seq2;
end;
end;
definition
let f be PartFunc of REAL,REAL;
let n be Nat;
let Z be Subset of REAL;
pred f is_differentiable_on n, Z means
for i be Nat st i <= n-1 holds diff(f,Z).i is_differentiable_on Z;
end;
theorem Th23:
for f be PartFunc of REAL,REAL, Z be Subset of REAL, n be
Nat st f is_differentiable_on n,Z for m be Nat st m <= n
holds f is_differentiable_on m, Z
proof
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
let n be Nat such that
A1: f is_differentiable_on n, Z;
let m be Nat such that
A2: m <=n;
now
A3: m-1 <=n-1 by A2,XREAL_1:13;
let i be Nat;
assume i <=m-1;
then i <=n-1 by A3,XXREAL_0:2;
hence diff(f,Z).i is_differentiable_on Z by A1;
end;
hence thesis;
end;
definition
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
let a,b be Real;
func Taylor(f,Z,a,b) -> Real_Sequence means
:Def7:
for n be Nat holds it.n = (diff(f,Z).n).a * (b-a) |^ n / (n!);
existence
proof
deffunc F(Nat)=(diff(f,Z).$1).a * (b-a) |^ $1 /($1!);
consider seq be Real_Sequence such that
A1: for n be Nat holds seq.n=F(n) from SEQ_1:sch 1;
take seq;
let n be Nat;
thus thesis by A1;
end;
uniqueness
proof
deffunc F(Nat)=(diff(f,Z).$1).a * (b-a) |^ $1 /($1!);
let s1,s2 be Real_Sequence such that
A2: for n be Nat holds s1.n=F(n) and
A3: for n be Nat holds s2.n=F(n);
now
let x be object;
assume x in NAT;
then reconsider n=x as Element of NAT;
thus s1.x = F(n) by A2
.=s2.x by A3;
end;
hence thesis;
end;
end;
Lm5: for b be Real
ex g be PartFunc of REAL,REAL st (dom(g)=[#]REAL &
for x be Real holds g.x=(b-x) &
for x be Real holds g is_differentiable_in x & diff(g,x)=-1 )
proof
defpred X[set] means $1 in REAL;
let b be Real;
deffunc U(Real) = In(b-$1,REAL);
consider g being PartFunc of REAL,REAL such that
A1: for d be Element of REAL holds d in dom g iff X[d] and
A2: for d be Element of REAL st d in dom g holds g/.d = U(d) from
PARTFUN2:sch 2;
take g;
for x be object st x in REAL holds x in dom g by A1;
then
A3: REAL c=dom(g) by TARSKI:def 3;
then
A4: dom(g)=[#]REAL by XBOOLE_0:def 10;
A5: for d be Real holds g.d = b-d
proof
let d be Real;
reconsider d as Element of REAL by XREAL_0:def 1;
g/.d = U(d) by A2,A4;
hence thesis by A4,PARTFUN1:def 6;
end;
A6: for d be Real st d in REAL holds g.d = (-1)*d + b
proof
let d be Real;
assume d in REAL;
thus g.d=b-d by A5
.= (-1)*d + b;
end;
then
A7: g is_differentiable_on dom(g) by A4,FDIFF_1:23;
for x be Real holds g is_differentiable_in x & diff(g,x)=-1
proof
let dd be Real;
reconsider d=dd as Element of REAL by XREAL_0:def 1;
g is_differentiable_in d by A4,A7,FDIFF_1:9;
hence g is_differentiable_in dd;
thus diff(g,dd)=(g`|dom(g)).d by A4,A7,FDIFF_1:def 7
.= -1 by A4,A6,FDIFF_1:23;
end;
hence thesis by A3,A5,XBOOLE_0:def 10;
end;
Lm6: for n be Nat for l,b be Real
ex g be PartFunc of REAL,REAL st dom(g)=[#]REAL &
(for x be Real holds g.x=l*(b-x) |^ (n+1) / ((n+1)!)) &
for x be Real
holds g is_differentiable_in x & diff(g,x)=-l* (b-x) |^ (n) /((n)!)
proof
defpred X[set] means $1 in REAL;
let n be Nat;
let l,b be Real;
deffunc U(Real) = In(l*(b-$1) |^ (n+1) /((n+1)!),REAL);
consider g being PartFunc of REAL, REAL such that
A1: for d be Element of REAL holds d in dom g iff X[d] and
A2: for d be Element of REAL st d in dom g holds g/.d = U(d) from
PARTFUN2:sch 2;
take g;
consider f be PartFunc of REAL,REAL such that
A3: dom(f)=[#]REAL and
A4: for x be Real holds f.x=(b-x) and
A5: for x be Real holds f is_differentiable_in x & diff(f,x)=-1 by Lm5;
dom( #Z (n+1)) = REAL & rng (f) c= REAL by FUNCT_2:def 1;
then
A6: dom ( #Z (n+1) *f ) = dom(f) by RELAT_1:27;
for x be object st x in REAL holds x in dom g by A1;
then
A7: REAL c=dom(g) by TARSKI:def 3;
then
A8: dom(g)=[#]REAL by XBOOLE_0:def 10;
A9: for d be Real holds g.d = l*(b-d) |^ (n+1) /((n+1)!)
proof
let d be Real;
reconsider d as Element of REAL by XREAL_0:def 1;
g/.d = U(d) by A2,A8;
hence thesis by A8,PARTFUN1:def 6;
end;
A10: now
let x be Element of REAL;
assume x in dom (l/((n+1)!) (#) ( #Z (n+1) *f ) );
hence
(( l/((n+1)!)) (#) ( #Z (n+1) *f ) ).x = (l/((n+1)!))*( #Z (n+1) *f )
.x by VALUED_1:def 5
.= (l/((n+1)!))*( #Z (n+1) *f )/.x by A3,A6,PARTFUN1:def 6
.= (l/((n+1)!))* #Z (n+1)/.(f/.x) by A3,A6,PARTFUN2:3
.=l/((n+1)!)*( #Z (n+1).(f.x) ) by A3,PARTFUN1:def 6
.=l/((n+1)!)*( (f.x) #Z (n+1) ) by Def1
.=l/((n+1)!)*( (f.x) |^ (n+1) ) by PREPOWER:36
.=l/((n+1)!)*( (b-x) |^ (n+1) ) by A4
.=l*(b-x) |^ (n+1)/((n+1)!) by XCMPLX_1:74
.=g.x by A9;
end;
A11: for x be Real
holds ( #Z (n+1)) *f is_differentiable_in x & diff(( #Z (
n+1)) *f,x) =- (n+1) *(b-x) #Z n
proof
let xx be Real;
reconsider x=xx as Real;
A12: f is_differentiable_in x & #Z (n+1) is_differentiable_in f.x by A5,Th2;
hence ( #Z (n+1)) *f is_differentiable_in xx by FDIFF_2:13;
diff(( #Z(n+1)),f.x) = (n+1) * (f.x) #Z ((n+1)-1) by Th2;
hence diff(( #Z (n+1)) *f,xx) = (n+1) *(f.x) #Z ((n+1)-1)*diff(f,x)
by A12,FDIFF_2:13
.= (n+1) *(f.x) #Z ((n+1)-1) *(-1) by A5
.= (n+1) *(b-x) #Z ((n+1)-1) *(-1) by A4
.=-(n+1)*(b-xx) #Z n;
end;
A13: now
let x be Real;
A14: (n+1) / ((n+1)!) = (1*(n+1))/ (n! * (n+1)) by NEWTON:15
.=1/(n!) by XCMPLX_1:91;
A15: ( #Z (n+1) *f) is_differentiable_in x by A11;
hence ( l/((n+1)!) ) (#) ( #Z (n+1) *f) is_differentiable_in x by
FDIFF_1:15;
thus diff((l/((n+1)!)) (#) ( #Z (n+1) *f),x) = (l/((n+1)!)) *diff( #Z (n+1
) *f,x) by A15,FDIFF_1:15
.= diff( #Z (n+1) *f,x)/((n+1)!)*l by XCMPLX_1:75
.=l *( (- (n+1) *(b-x) #Z n )/ ((n+1)!)) by A11
.=l *( (- (n+1) *(b-x) |^ n )/ ((n+1)!)) by PREPOWER:36
.=l * (- (n+1) *(b-x) |^ n )/ ((n+1)!) by XCMPLX_1:74
.=(-l) *((n+1) * (b-x) |^ n)/((n+1)!)
.=(-l) *(((n+1) *(b-x) |^ n )/ ((n+1)!)) by XCMPLX_1:74
.=(-l) *( (b-x) |^ n * ((n+1) / ((n+1)!)) ) by XCMPLX_1:74
.=(-l) *( (b-x) |^ n / (n!)) by A14,XCMPLX_1:99
.=-(l*( (b-x) |^ n / (n!)))
.=-(l*(b-x) |^ n / (n!)) by XCMPLX_1:74;
end;
dom (( l/((n+1)!)) (#) ( #Z (n+1) *f )) = dom(g) by A8,A3,A6,VALUED_1:def 5;
then ( l/((n+1)!)) (#) ( #Z (n+1) *f) =g by A10,PARTFUN1:5;
hence thesis by A7,A9,A13,XBOOLE_0:def 10;
end;
Lm7: for n be Nat for f be PartFunc of REAL,REAL for Z be Subset of
REAL for b be Real
ex g be PartFunc of REAL,REAL st ( dom(g)=Z & for x be
Real st x in Z holds g.x=f.b-Partial_Sums(Taylor(f,Z,x,b)).n )
proof
let n be Nat;
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
let b be Real;
defpred X[set] means $1 in Z;
deffunc U(Real) = In(f.b-Partial_Sums(Taylor(f,Z,$1,b)).n,REAL);
consider g being PartFunc of REAL, REAL such that
A1: for d be Element of REAL holds d in dom g iff X[d] and
A2: for d be Element of REAL st d in dom g holds g/.d = U(d) from
PARTFUN2:sch 2;
take g;
for x be object st x in dom g holds x in Z by A1;
then
A3: dom(g) c= Z by TARSKI:def 3;
for x be object st x in Z holds x in dom g by A1;
then
A4: Z c=dom(g) by TARSKI:def 3;
for d be Real st d in Z holds g.d =f.b-Partial_Sums(Taylor(f,Z,d,b)).n
proof
let d be Real such that
A5: d in Z;
g/.d = U(d) by A2,A4,A5
.= f.b-Partial_Sums(Taylor(f,Z,d,b)).n;
hence thesis by A4,A5,PARTFUN1:def 6;
end;
hence thesis by A3,A4,XBOOLE_0:def 10;
end;
theorem Th24:
for f be PartFunc of REAL,REAL, Z be Subset of REAL, n be Nat
st f is_differentiable_on n, Z
for a,b be Real st a < b & ].a,b
.[ c= Z holds diff(f,Z).n | ].a,b.[ = diff(f,].a,b.[).n
proof
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
defpred P[Nat] means f is_differentiable_on $1, Z implies
for a,b be Real st a < b & ].a,b.[ c= Z
holds diff(f,Z).$1 | ].a,b.[ = diff(f,].a,b.[).$1;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
assume
A3: f is_differentiable_on (k+1), Z;
let a,b be Real such that
A4: a < b and
A5: ].a,b.[ c= Z;
A6: (diff(f,Z).k) is_differentiable_on Z by A3;
then
A7: (diff(f,Z).k) is_differentiable_on ].a,b.[ by A5,FDIFF_1:26;
then
A8: dom((diff(f,Z).k)`| ].a,b.[) = ].a,b.[ by FDIFF_1:def 7;
A9: dom(((diff(f,Z).k)`|Z)| ].a,b.[) =dom((diff(f,Z).k)`|Z) /\ ].a,b.[ by
RELAT_1:61
.=Z /\ ].a,b.[ by A6,FDIFF_1:def 7
.=].a,b.[ by A5,XBOOLE_1:28;
A10: now
let x be Element of REAL such that
A11: x in dom(((diff(f,Z).k)`|Z)| ].a,b.[);
thus (((diff(f,Z).k)`|Z)| ].a,b.[).x =((diff(f,Z).k)`|Z).x by A9,A11,
FUNCT_1:49
.=diff((diff(f,Z).k),x) by A5,A6,A9,A11,FDIFF_1:def 7
.=((diff(f,Z).k)`|].a,b.[).x by A7,A9,A11,FDIFF_1:def 7;
end;
thus diff(f,Z).(k+1) | ].a,b.[ =((diff(f,Z).k)`|Z)| ].a,b.[ by Def5
.=(diff(f,Z).k)`| ].a,b.[ by A9,A8,A10,PARTFUN1:5
.= ((diff(f,Z).k)|].a,b.[) `| ].a,b.[ by A7,FDIFF_2:16
.=(diff(f,].a,b.[).k)`| ].a,b.[ by A2,A3,A4,A5,Th23,NAT_1:11
.=diff(f,].a,b.[).(k+1) by Def5;
end;
A12: P[0]
proof
assume f is_differentiable_on 0, Z;
let a,b be Real such that
a < b and
A13: ].a,b.[ c=Z;
thus (diff(f,Z).0) |].a,b.[ = (f|Z)|].a,b.[ by Def5
.=f|].a,b.[ by A13,FUNCT_1:51
.=diff(f,].a,b.[).0 by Def5;
end;
thus for k be Nat holds P[k] from NAT_1: sch 2(A12,A1);
end;
Lm8: for f be PartFunc of REAL,REAL, Z be Subset of REAL st Z c= dom f for n
be Nat st f is_differentiable_on n, Z
for a,b be Real st a < b & [.a
,b.] c= Z & (diff(f,Z).n)|[.a,b.] is continuous & f is_differentiable_on (n+1),
].a,b.[ for g be PartFunc of REAL,REAL st dom g=Z &
for x be Real st x in Z
holds g.x=f.b-Partial_Sums(Taylor(f,Z,x,b)).n holds g.b=0 & g|[.a,b.] is
continuous & g is_differentiable_on ].a,b.[ & for x be Real st x in ].a,b.[
holds diff(g,x)=-(diff(f,].a,b.[).(n+1)).x * (b-x) |^ n /(n!)
proof
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL such that
A1: Z c= dom f;
defpred P[Nat] means f is_differentiable_on $1, Z implies
for a,b be Real st a < b & [.a,b.] c=Z &
(diff(f,Z).$1)|[.a,b.] is continuous & f
is_differentiable_on ($1+1), ].a,b.[ for g be PartFunc of REAL,REAL st dom(g)=Z
& for x be Real st x in Z holds g.x=f.b-Partial_Sums(Taylor(f,Z,x,b)).$1 holds
g.b=0 & g|[.a,b.] is continuous & g is_differentiable_on ].a,b.[ & for x be
Real st x in ].a,b.[ holds diff(g,x)=-(diff(f,].a,b.[).($1+1)).x * (b-x) |^ $1
/ ( $1!);
A2: P[0]
proof
assume f is_differentiable_on 0, Z;
let a,b be Real such that
A3: a < b and
A4: [.a,b.] c= Z and
A5: (diff(f,Z).0)|[.a,b.] is continuous and
A6: f is_differentiable_on (0+1), ].a,b.[;
A7: ].a,b.[ c=[.a,b.] by XXREAL_1:25;
then
A8: ].a,b.[ c= Z by A4,XBOOLE_1:1;
let g be PartFunc of REAL,REAL such that
A9: dom(g)=Z and
A10: for x be Real st x in Z holds g.x=f.b-Partial_Sums(Taylor(f,Z,x,b) ).0;
A11: b in [.a,b.] by A3,XXREAL_1:1;
hence g.b=f.b-Partial_Sums(Taylor(f,Z,b,b)).(0) by A4,A10
.=f.b-Taylor(f,Z,b,b).0 by SERIES_1:def 1
.=f.b - (diff(f,Z).(0)).b * (b-b) |^ (0) /((0)!) by Def7
.=f.b - (f|Z).b * (b-b) |^ (0) /((0)!) by Def5
.=f.b - f.b * (b-b) |^ (0) /((0)!) by A4,A11,FUNCT_1:49
.=f.b - f.b * 1 by NEWTON:4,12
.=0;
consider y be PartFunc of REAL,REAL such that
A12: dom(y)=[#]REAL and
A13: for x be Real holds y.x=(f.b-x) and
A14: for x be Real holds y is_differentiable_in x & diff(y,x)=-1 by Lm5;
rng(f) c= REAL;
then
A15: dom(y*f) = dom(f) by A12,RELAT_1:27;
for x be Real st x in REAL holds y is_differentiable_in x by A14;
then y is_differentiable_on REAL by A12,FDIFF_1:9;
then y|REAL is continuous by FDIFF_1:25;
then
A16: y|(f.:[.a,b.]) is continuous by FCONT_1:16;
rng(f) c= dom(y) by A12;
then
A17: dom(y*f) = dom(f) by RELAT_1:27;
A18: [.a,b.] c= dom(f) by A1,A4,XBOOLE_1:1;
then
A19: ].a,b.[ c= dom(f) by A7,XBOOLE_1:1;
diff(f,].a,b.[).0 is_differentiable_on ].a,b.[ by A6;
then f|].a,b.[ is_differentiable_on ].a,b.[ by Def5;
then for x be Real st x in ].a,b.[
holds f|].a,b.[ is_differentiable_in x by FDIFF_1:9;
then
A20: f is_differentiable_on ].a,b.[ by A19,FDIFF_1:def 6;
A21: for x be Real st x in ].a,b.[ holds y *f is_differentiable_in x &
diff( y*f,x) =-diff(f,].a,b.[).(0+1).x * (b-x) |^ (0) / ( (0)!)
proof
A22: diff(f,].a,b.[).(0+1)=( diff(f,].a,b.[).0)`|].a,b.[ by Def5
.= (f|].a,b.[)`|].a,b.[ by Def5
.= f`|].a,b.[ by A20,FDIFF_2:16;
let x be Real such that
A23: x in ].a,b.[;
A24: f is_differentiable_in x by A20,A23,FDIFF_1:9;
A25: y is_differentiable_in f.x by A14;
hence y*f is_differentiable_in x by A24,FDIFF_2:13;
A26: (b-x) |^ (0) /((0)!)=1 by NEWTON:4,12;
thus diff( y*f,x) =diff(y, f.x)*diff(f,x) by A25,A24,FDIFF_2:13
.= diff(y,f.x)*(f`|].a,b.[).x by A20,A23,FDIFF_1:def 7
.= (-1)*diff(f,].a,b.[).(0+1).x by A14,A22
.=-diff(f,].a,b.[).(0+1).x*((b-x) |^ (0) /((0)!)) by A26
.=-diff(f,].a,b.[).(0+1).x*(b-x) |^ (0) /((0)!) by XCMPLX_1:74;
end;
then for x be Real st x in ].a,b.[
holds y *f is_differentiable_in x;
then
A27: y*f is_differentiable_on ].a,b.[ by A19,A17,FDIFF_1:9;
A28: dom((y*f)|[.a,b.])=dom(y*f) /\ [.a,b.] by RELAT_1:61
.=[.a,b.] by A1,A4,A15,XBOOLE_1:1,28
.=Z /\ [.a,b.] by A4,XBOOLE_1:28
.=dom(g|[.a,b.]) by A9,RELAT_1:61;
A29: now
let xx be object such that
A30: xx in dom(g|[.a,b.]);
reconsider x=xx as Real by A30;
dom(g|[.a,b.])=dom(g) /\ [.a,b.] by RELAT_1:61;
then dom(g|[.a,b.]) c= [.a,b.] by XBOOLE_1:17;
then
A31: x in [.a,b.] by A30;
A32: (b-x) |^ 0 /((0)!)=1 by NEWTON:4,12;
thus (g|[.a,b.]).xx =g.x by A30,FUNCT_1:47
.=f.b-Partial_Sums(Taylor(f,Z,x,b)).(0) by A4,A10,A31
.=f.b-Taylor(f,Z,x,b).0 by SERIES_1:def 1
.=f.b - (diff(f,Z).(0)).x * (b-x) |^ (0) /((0)!) by Def7
.=f.b - (f|Z).x * (b-x) |^ 0 /((0)!) by Def5
.=f.b - f.x * (b-x) |^ 0 /((0)!) by A4,A31,FUNCT_1:49
.=f.b - f.x * ((b-x) |^ 0 /((0)!)) by XCMPLX_1:74
.=y.(f.x) by A13,A32
.=(y*f).x by A18,A31,FUNCT_1:13
.=((y*f)|[.a,b.]).xx by A28,A30,FUNCT_1:47;
end;
f|Z|[.a,b.] is continuous by A5,Def5;
then (f|Z)| [.a,b.]|[.a,b.] is continuous by FCONT_1:15;
then (f|[.a,b.])|[.a,b.] is continuous by A4,FUNCT_1:51;
then f|[.a,b.] is continuous by FCONT_1:15;
then (y*f)|[.a,b.] is continuous by A16,FCONT_1:25;
hence g|[.a,b.] is continuous by A28,A29,FUNCT_1:2;
A33: dom((y*f)|].a,b.[) = dom(y*f) /\ ].a,b.[ by RELAT_1:61
.= ].a,b.[ by A7,A18,A17,XBOOLE_1:1,28
.= Z /\ ].a,b.[ by A4,A7,XBOOLE_1:1,28
.= dom(g|].a,b.[) by A9,RELAT_1:61;
now
let xx be object such that
A34: xx in dom(g|].a,b.[);
reconsider x=xx as Real by A34;
dom(g|].a,b.[)=dom(g) /\ ].a,b.[ by RELAT_1:61;
then dom(g|].a,b.[) c= ].a,b.[ by XBOOLE_1:17;
then
A35: x in ].a,b.[ by A34;
A36: (b-x) |^ (0) /((0)!) =1 by NEWTON:4,12;
thus (g|].a,b.[).xx =g.x by A34,FUNCT_1:47
.=f.b-Partial_Sums(Taylor(f,Z,x,b)).(0) by A10,A8,A35
.=f.b-Taylor(f,Z,x,b).0 by SERIES_1:def 1
.=f.b - (diff(f,Z).(0)).x * (b-x) |^ (0) /((0)!) by Def7
.=f.b - (f|Z).x * (b-x) |^ (0) /((0)!) by Def5
.=f.b - f.x * (b-x) |^ (0) /((0)!) by A8,A35,FUNCT_1:49
.=f.b - f.x * ((b-x) |^ (0) /((0)!)) by XCMPLX_1:74
.=y.(f.x) by A13,A36
.=(y*f).x by A19,A35,FUNCT_1:13
.=((y*f)|].a,b.[).xx by A33,A34,FUNCT_1:47;
end;
then
A37: g|].a,b.[=(y*f)|].a,b.[ by A33,FUNCT_1:2;
then g|].a,b.[ is_differentiable_on ].a,b.[ by A27,FDIFF_2:16;
then for x be Real st x in ].a,b.[
holds g|].a,b.[ is_differentiable_in x by FDIFF_1:9;
hence
A38: g is_differentiable_on ].a,b.[ by A9,A8,FDIFF_1:def 6;
now
let x be Real such that
A39: x in ].a,b.[;
thus g is_differentiable_in x by A38,A39,FDIFF_1:9;
thus diff(g,x) =(g`|].a,b.[).x by A38,A39,FDIFF_1:def 7
.=((g|].a,b.[)`|].a,b.[).x by A38,FDIFF_2:16
.= ((y*f)`|].a,b.[).x by A37,A27,FDIFF_2:16
.=diff( y*f,x) by A27,A39,FDIFF_1:def 7
.=-diff(f,].a,b.[).(0+1).x * (b-x) |^ (0) / ( (0)!) by A21,A39;
end;
hence thesis;
end;
A40: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A41: P[k];
assume
A42: f is_differentiable_on k+1, Z;
let a,b be Real such that
A43: a < b and
A44: [.a,b.] c=Z and
A45: (diff(f,Z).(k+1))|[.a,b.] is continuous and
A46: f is_differentiable_on ((k+1)+1), ].a,b.[;
diff(f,Z).k is_differentiable_on Z by A42;
then (diff(f,Z).k)|Z is continuous by FDIFF_1:25;
then
A47: (diff(f,Z).k)|[.a,b.] is continuous by A44,FCONT_1:16;
A48: ].a,b.[ c=[.a,b.] by XXREAL_1:25;
then
A49: ].a,b.[ c= Z by A44,XBOOLE_1:1;
consider gk be PartFunc of REAL,REAL such that
A50: dom(gk)=Z and
A51: for x be Real st x in Z holds gk.x=f.b-Partial_Sums(Taylor(f,Z,x,
b)).k by Lm7;
A52: f is_differentiable_on (k+1), ].a,b.[ by A46,Th23,NAT_1:11;
then
A53: gk is_differentiable_on ].a,b.[ by A41,A42,A43,A44,A47,A50,A51,Th23,
NAT_1:11;
A54: gk|[.a,b.] is continuous by A41,A42,A43,A44,A47,A52,A50,A51,Th23,NAT_1:11;
now
A55: diff(f,Z).k is_differentiable_on Z by A42;
k <=(k+1)+1-1 by NAT_1:11;
then
A56: diff(f,].a,b.[).k is_differentiable_on ].a,b.[ by A46;
A57: diff(f,Z).(k+1)=( diff(f,Z).k)`|Z by Def5;
let gk1 be PartFunc of REAL,REAL such that
A58: dom(gk1)=Z and
A59: for x be Real st x in Z holds gk1.x=f.b-Partial_Sums(Taylor(f,Z
,x,b)).(k+1);
A60: b in [.a,b.] by A43,XXREAL_1:1;
then gk1.b=f.b-Partial_Sums(Taylor(f,Z,b,b)).(k+1) by A44,A59
.=f.b-(Partial_Sums(Taylor(f,Z,b,b)).k+Taylor(f,Z,b,b).(k+1)) by
SERIES_1:def 1
.=(f.b-Partial_Sums(Taylor(f,Z,b,b)).k)-Taylor(f,Z,b,b).(k+1)
.=gk.b -Taylor(f,Z,b,b).(k+1) by A44,A51,A60
.=0 -Taylor(f,Z,b,b).(k+1) by A41,A42,A43,A44,A47,A52,A50,A51,Th23,
NAT_1:11
.=0 - (diff(f,Z).(k+1)).b * (b-b) |^ (k+1) /((k+1)!) by Def7
.=0 - (diff(f,Z).(k+1)).b * (0|^k*0) /((k+1)!) by NEWTON:6
.=0;
hence gk1.b=0;
consider h be PartFunc of REAL,REAL such that
A61: dom(h)=[#]REAL and
A62: for x be Real holds h.x=1*(b-x) |^ (k+1) /((k+1)!) and
A63: for x be Real
holds h is_differentiable_in x & diff(h,x)=-1* (b
-x) |^ (k) /((k)!) by Lm6;
A64: dom(diff(f,Z).(k+1) (#)h) = dom (diff(f,Z).(k+1)) /\ dom(h) by
VALUED_1:def 4
.= Z /\ REAL by A61,A57,A55,FDIFF_1:def 7
.= Z by XBOOLE_1:28;
A65: dom(gk-diff(f,Z).(k+1) (#)h) =dom(gk) /\ dom(diff(f,Z).(k+1) (#)h)
by VALUED_1:12
.=Z by A50,A64;
thus gk1|[.a,b.] is continuous
proof
set ghk=gk-((diff(f,Z).(k+1)) (#) h);
for x be Real st x in REAL holds h is_differentiable_in x
by A63;
then h is_differentiable_on REAL by A61,FDIFF_1:9;
then h|REAL is continuous by FDIFF_1:25;
then
A66: h|[.a,b.] is continuous by FCONT_1:16;
now
let x be Element of REAL such that
A67: x in Z;
thus gk1.x=f.b-Partial_Sums(Taylor(f,Z,x,b)).(k+1) by A59,A67
.=f.b-(Partial_Sums(Taylor(f,Z,x,b)).k+Taylor(f,Z,x,b).(k+1)) by
SERIES_1:def 1
.=f.b-Partial_Sums(Taylor(f,Z,x,b)).k-Taylor(f,Z,x,b).(k+1)
.=gk.x -Taylor(f,Z,x,b).(k+1) by A51,A67
.=gk.x - (diff(f,Z).(k+1)).x * (b-x) |^ (k+1) /((k+1)!) by Def7
.=gk.x - (diff(f,Z).(k+1)).x * (1*(b-x) |^ (k+1) /((k+1)!)) by
XCMPLX_1:74
.=gk.x - (diff(f,Z).(k+1)).x * h.x by A62
.=gk.x - ((diff(f,Z).(k+1)) (#) h).x by VALUED_1:5
.=(gk-((diff(f,Z).(k+1)) (#) h)).x by A65,A67,VALUED_1:13;
end;
then
A68: gk1= ghk by A58,A65,PARTFUN1:5;
[.a,b.] c= dom(diff(f,Z).(k+1)) by A44,A57,A55,FDIFF_1:def 7;
then ((diff(f,Z).(k+1)) (#) h)|([.a,b.] /\ [.a,b.]) is continuous by
A45,A61,A66,FCONT_1:19;
hence thesis by A44,A50,A54,A64,A68,FCONT_1:19;
end;
A69: diff(f,].a,b.[).(k+1)=( diff(f,].a,b.[).k)`|].a,b.[ by Def5;
set gfh=gk-diff(f,].a,b.[).(k+1) (#)h;
A70: dom(diff(f,].a,b.[).(k+1) (#)h) = dom (diff(f,].a,b.[).(k+1)) /\
dom(h) by VALUED_1:def 4
.= ].a,b.[ /\ REAL by A61,A69,A56,FDIFF_1:def 7
.= ].a,b.[ by XBOOLE_1:28;
then
A71: dom(gk-diff(f, ].a,b.[).(k+1) (#)h)=Z /\ ].a,b.[ by A50,VALUED_1:12
.= ].a,b.[ by A44,A48,XBOOLE_1:1,28;
A72: for x be Real st x in ].a,b.[ holds (gk-diff(f,Z).(k+1) (#)h).x =(
gk-diff(f,].a,b.[).(k+1) (#)h).x
proof
let x be Real such that
A73: x in ].a,b.[;
thus (gk-diff(f,].a,b.[).(k+1) (#)h).x =gk.x - (diff(f,].a,b.[).(k+1)
(#)h).x by A71,A73,VALUED_1:13
.=gk.x - (diff(f,].a,b.[).(k+1)).x * h.x by VALUED_1:5
.=gk.x - ((diff(f,Z).(k+1))|].a,b.[).x * h.x by A42,A43,A44,A48,Th24,
XBOOLE_1:1
.=gk.x - (diff(f,Z).(k+1)).x * h.x by A73,FUNCT_1:49
.=gk.x - ((diff(f,Z).(k+1)) (#)h).x by VALUED_1:5
.=(gk - ((diff(f,Z).(k+1)) (#)h)).x by A49,A65,A73,VALUED_1:13;
end;
A74: now
let xx be object such that
A75: xx in dom(gfh);
reconsider x=xx as Real by A75;
thus gk1.xx =f.b-Partial_Sums(Taylor(f,Z,x,b)).(k+1) by A49,A59,A71,A75
.=f.b-(Partial_Sums(Taylor(f,Z,x,b)).k + Taylor(f,Z,x,b).(k+1)) by
SERIES_1:def 1
.=f.b-Partial_Sums(Taylor(f,Z,x,b)).k -Taylor(f,Z,x,b).(k+1)
.=gk.x - Taylor(f,Z,x,b).(k+1) by A49,A51,A71,A75
.=gk.x - (diff(f,Z).(k+1)).x * (b-x) |^ (k+1) /((k+1)!) by Def7
.=gk.x - (diff(f,Z).(k+1)).x * (1*(b-x) |^ (k+1) /((k+1)!)) by
XCMPLX_1:74
.=gk.x - (diff(f,Z).(k+1)).x * h.x by A62
.=gk.x - (diff(f,Z).(k+1) (#)h).x by VALUED_1:5
.=(gk- (diff(f,Z).(k+1) (#)h)).x by A49,A65,A71,A75,VALUED_1:13
.=gfh.xx by A71,A72,A75;
end;
A76: diff(f,].a,b.[).(k+1) is_differentiable_on ].a,b.[ by A46;
for x be Real st x in ].a,b.[
holds h is_differentiable_in x by A63;
then
A77: h is_differentiable_on ].a,b.[ by A61,FDIFF_1:9;
then
A78: diff(f,].a,b.[).(k+1) (#)h is_differentiable_on ].a,b.[ by A70,A76,
FDIFF_1:21;
then
A79: gfh is_differentiable_on ].a,b.[ by A53,A71,FDIFF_1:19;
dom(gfh)=dom(gk1)/\ ].a,b.[ by A44,A48,A58,A71,XBOOLE_1:1,28;
then
A80: (gk1|].a,b.[)|].a,b.[= gfh|].a,b.[ by A74,FUNCT_1:46;
then gfh|].a,b.[=gk1|].a,b.[ by FUNCT_1:51;
then for x be Real st x in ].a,b.[ holds gk1|].a,b.[
is_differentiable_in x by A79,FDIFF_1:def 6;
hence
A81: gk1 is_differentiable_on ].a,b.[ by A49,A58,FDIFF_1:def 6;
now
let x be Real such that
A82: x in ].a,b.[;
thus diff(gk1,x)=(gk1`|].a,b.[).x by A81,A82,FDIFF_1:def 7
.=((gk1|].a,b.[)`|].a,b.[).x by A81,FDIFF_2:16
.=((gfh|].a,b.[)`|].a,b.[).x by A80,FUNCT_1:51
.=(gfh`|].a,b.[).x by A79,FDIFF_2:16
.=diff(gk,x) - diff(diff(f,].a,b.[).(k+1) (#)h,x) by A53,A71,A78,A82,
FDIFF_1:19
.=-(diff(f,].a,b.[).(k+1)).x * (b-x) |^ (k) /((k)!) -diff(diff(f,
].a,b.[).(k+1) (#)h,x) by A41,A42,A43,A44,A47,A52,A50,A51,A82,Th23,NAT_1:11
.=-(diff(f,].a,b.[).(k+1)).x * (b-x) |^ (k) /((k)!) - ((diff(f,].a
,b.[).(k+1) (#)h)`|].a,b.[).x by A78,A82,FDIFF_1:def 7
.= -(diff(f,].a,b.[).(k+1)).x * (b-x) |^ (k) /((k)!) - ((h.x)*diff
(diff(f,].a,b.[).(k+1),x) + (diff(f,].a,b.[).(k+1).x)*diff(h,x)) by A70,A76,A77
,A82,FDIFF_1:21
.= -(diff(f,].a,b.[).(k+1)).x * (b-x) |^ (k) /((k)!) - (h.x)*diff(
diff(f,].a,b.[).(k+1),x) -(diff(f,].a,b.[).(k+1).x)*diff(h,x)
.= -(diff(f,].a,b.[).(k+1)).x * (b-x) |^ (k) /((k)!) - (1*(b-x) |^
(k+1) /((k+1)!) ) *diff(diff(f,].a,b.[).(k+1),x) -(diff(f,].a,b.[).(k+1).x)*
diff(h,x) by A62
.= -(diff(f,].a,b.[).(k+1)).x * (b-x) |^ (k) /((k)!) - (b-x) |^ (k
+1) /((k+1)!) *diff(diff(f,].a,b.[).(k+1),x) -(diff(f,].a,b.[).(k+1).x) *(-1* (
b-x) |^ (k) /((k)!)) by A63
.= -(diff(f,].a,b.[).(k+1)).x * (b-x) |^ (k) /((k)!) +(diff(f,].a,
b.[).(k+1).x)*(1* (b-x) |^ (k) /((k)!)) - (b-x) |^ (k+1) /((k+1)!) *diff(diff(f
,].a,b.[).(k+1),x)
.= -(diff(f,].a,b.[).(k+1)).x * (b-x) |^ (k) /((k)!) +(diff(f,].a,
b.[).(k+1)).x* (b-x) |^ (k) /((k)!) - (b-x) |^ (k+1) /((k+1)!) *diff(diff(f,].a
,b.[).(k+1),x) by XCMPLX_1:74
.= - (b-x) |^ (k+1) /((k+1)!) *diff(diff(f,].a,b.[).(k+1),x)
.= - (b-x) |^ (k+1) /((k+1)!) *(diff(f,].a,b.[).(k+1)`|].a,b.[).x
by A76,A82,FDIFF_1:def 7
.= - (b-x) |^ (k+1) /((k+1)!) * (diff(f,].a,b.[).((k+1)+1)).x by Def5
.= - (diff(f,].a,b.[).((k+1)+1)).x * (b-x) |^ (k+1) /((k+1)!) by
XCMPLX_1:74;
end;
hence
for x be Real st x in ].a,b.[ holds diff(gk1,x) =-(diff(f,].a,b.[).
((k+1)+1)).x * (b-x) |^ ((k+1)) /((k+1)!);
end;
hence thesis;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A2,A40);
hence thesis;
end;
Lm9: for n be Nat for f be PartFunc of REAL,REAL for Z be Subset of
REAL st Z c= dom f & f is_differentiable_on n, Z
for a,b be Real st a < b & [.a
,b.] c= Z & (diff(f,Z).n)|[.a,b.] is continuous & f is_differentiable_on (n+1),
].a,b.[ ex g be PartFunc of REAL,REAL st dom(g)=Z &
(for x be Real st x in Z
holds g.x=f.b-Partial_Sums(Taylor(f,Z,x,b)).n) & g.b=0 & g|[.a,b.] is
continuous & g is_differentiable_on ].a,b.[ & for x be Real st x in ].a,b.[
holds diff(g,x)=-(diff(f,].a,b.[).(n+1)).x * (b-x) |^ (n) /(n!)
proof
let n be Nat;
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL such that
A1: Z c= dom f & f is_differentiable_on n, Z;
let a,b be Real such that
A2: a < b & [.a,b.] c= Z & (diff(f,Z).n)|[.a,b.] is continuous & f
is_differentiable_on (n+1), ].a,b.[;
consider g be PartFunc of REAL,REAL such that
A3: dom(g)=Z & for x be Real st x in Z holds g.x=f.b-Partial_Sums(Taylor
(f,Z,x,b )).n by Lm7;
take g;
thus thesis by A1,A2,A3,Lm8;
end;
theorem Th25:
for n be Nat, f be PartFunc of REAL,REAL, Z be Subset
of REAL st Z c= dom f & f is_differentiable_on n,Z
for a,b be Real st a < b &
[.a,b.] c=Z & (diff(f,Z).n)|[.a,b.] is continuous &
f is_differentiable_on (n+1), ].a,b.[
for l be Real, g be PartFunc of REAL,REAL st dom(g)=[#]REAL &
(for x be Real
holds g.x=f.b-Partial_Sums(Taylor(f,Z,x,b)).n -l*(b-x) |^ (n+1)
/ ((n+1)!)) & f.b-Partial_Sums(Taylor(f,Z,a,b)).n -l*(b-a) |^ (n+1) / ((n+1)!)
= 0 holds g is_differentiable_on ].a,b.[ & g.a=0 & g.b=0 & g|[.a,b.] is
continuous & for x be Real st x in ].a,b.[ holds diff(g,x) = -(diff(f,].a,b.[).
(n+1)).x * (b-x) |^ n /(n!) +l* (b-x) |^ n /(n!)
proof
let n be Nat;
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL such that
A1: Z c= dom f & f is_differentiable_on n, Z;
let a,b be Real such that
A2: a < b and
A3: [.a,b.] c=Z and
A4: (diff(f,Z).n)|[.a,b.] is continuous & f is_differentiable_on (n+1),
].a,b.[;
let l be Real;
consider p be PartFunc of REAL,REAL such that
A5: dom(p)=[#]REAL and
A6: for x be Real holds p.x=l*(b-x) |^ (n+1) /((n+1)!) and
A7: for x be Real holds p is_differentiable_in x & diff(p,x)=-l* (b-x)
|^ (n) /((n)!) by Lm6;
consider h be PartFunc of REAL,REAL such that
A8: dom(h)=Z and
A9: for x be Real st x in Z
holds h.x=f.b-Partial_Sums(Taylor(f,Z,x,b)) . n and
A10: h.b=0 and
A11: h|[.a,b.] is continuous and
A12: h is_differentiable_on ].a,b.[ and
A13: for x be Real st x in ].a,b.[ holds diff(h,x)=-(diff(f,].a,b.[).(n+
1 )).x * (b-x) |^ (n) /(n!) by A1,A2,A3,A4,Lm9;
A14: [.a,b.] c= dom h /\ dom p by A3,A8,A5,XBOOLE_1:19;
let g be PartFunc of REAL,REAL such that
A15: dom g=[#]REAL and
A16: for x be Real
holds g.x=f.b-Partial_Sums(Taylor(f,Z,x,b)).n -l*(b-x)
|^ (n+1) /((n+1)!) and
A17: f.b-Partial_Sums(Taylor(f,Z,a,b)).n -l*(b-a) |^ (n+1) /((n+1)!) =0;
set hp=h-p;
A18: dom(hp)=dom(h) /\ dom(p) by VALUED_1:12
.=Z by A8,A5,XBOOLE_1:28;
A19: for x be object st x in dom(hp) holds hp.x=g.x
proof
let x be object such that
A20: x in dom(hp);
reconsider xx=x as Real by A20;
thus hp.x=h.xx-p.xx by A20,VALUED_1:13
.=(f.b-Partial_Sums(Taylor(f,Z,xx,b)).n) -p.xx by A9,A18,A20
.=(f.b-Partial_Sums(Taylor(f,Z,xx,b)).n) -(l*(b-xx) |^ (n+1)/((n+1)!))
by A6
.=g.x by A16;
end;
for x be Real st x in REAL holds p is_differentiable_in x by A7;
then p is_differentiable_on REAL by A5,FDIFF_1:9;
then p|REAL is continuous by FDIFF_1:25;
then
A21: p|[.a,b.] is continuous by FCONT_1:16;
].a,b.[ c=[.a,b.] by XXREAL_1:25;
then
A22: ].a,b.[ c= Z by A3,XBOOLE_1:1;
A23: dom(hp)=dom(g) /\ Z by A15,A18,XBOOLE_1:28;
then
A24: hp|].a,b.[ = (g|Z)|].a,b.[ by A19,FUNCT_1:46
.= g|].a,b.[ by A22,FUNCT_1:51;
A25: for x be Real st x in ].a,b.[ holds hp is_differentiable_in x & diff(hp
,x)=-(diff(f,].a,b.[).(n+1)).x * (b-x) |^ (n) /(n!) +l* (b-x) |^ (n) /((n)!)
proof
let x be Real such that
A26: x in ].a,b.[;
A27: h is_differentiable_in x by A12,A26,FDIFF_1:9;
A28: p is_differentiable_in x by A7;
hence hp is_differentiable_in x by A27,FDIFF_1:14;
thus diff(hp,x)=diff(h,x)-diff(p,x) by A27,A28,FDIFF_1:14
.=-(diff(f,].a,b.[).(n+1)).x * (b-x) |^ (n) /(n!) -diff(p,x) by A13,A26
.=-(diff(f,].a,b.[).(n+1)).x * (b-x) |^ (n) /(n!) -(-l* (b-x) |^ (n) /
((n)!)) by A7
.=-(diff(f,].a,b.[).(n+1)).x * (b-x) |^ (n) /(n!) +l* (b-x) |^ n /((n)
!);
end;
then for x be Real st x in ].a,b.[ holds hp is_differentiable_in x;
then
A29: hp is_differentiable_on ].a,b.[ by A18,A22,FDIFF_1:9;
then for x be Real st x in ].a,b.[
holds hp|].a,b.[ is_differentiable_in x by FDIFF_1:def 6;
hence
A30: g is_differentiable_on ].a,b.[ by A15,A24,FDIFF_1:def 6;
reconsider aa=a as Real;
g.aa=0 by A16,A17;
hence g.a=0;
A31: b in [.a,b.] by A2,XXREAL_1:1;
then g.b=hp.b by A3,A18,A19
.=h.b-p.b by A3,A18,A31,VALUED_1:13
.=0-(l*(b-b) |^ (n+1)/((n+1)!)) by A10,A6
.=0-(l*(0|^ n*0)/((n+1)!)) by NEWTON:6
.=0;
hence g.b=0;
hp|[.a,b.] = (g|Z)|[.a,b.] by A23,A19,FUNCT_1:46
.= g|[.a,b.] by A3,FUNCT_1:51;
hence g|[.a,b.] is continuous by A11,A14,A21,FCONT_1:18;
thus for x be Real st x in ].a,b.[ holds diff(g,x) =-(diff(f,].a,b.[).(n+1))
.x * (b-x) |^ (n) /((n)!) +l* (b-x) |^ (n) /((n)!)
proof
let x be Real such that
A32: x in ].a,b.[;
thus diff(g,x) = (g`|].a,b.[).x by A30,A32,FDIFF_1:def 7
.=((g|].a,b.[)`|].a,b.[).x by A30,FDIFF_2:16
.=(hp`|].a,b.[).x by A24,A29,FDIFF_2:16
.=diff(hp,x) by A29,A32,FDIFF_1:def 7
.=-(diff(f,].a,b.[).(n+1)).x * (b-x) |^ (n) /(n!) +l* (b-x) |^ (n) /((
n)!) by A25,A32;
end;
end;
theorem Th26:
for n be Nat, f be PartFunc of REAL,REAL, Z be Subset
of REAL, b,l be Real
ex g be Function of REAL,REAL st for x be Real holds
g.x=f.b-Partial_Sums(Taylor(f,Z,x,b)).n -l*(b-x) |^ (n+1) /((n+1)!)
proof
let n be Nat;
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
let b,l be Real;
deffunc U(Real)
= In(f.b-Partial_Sums(Taylor(f,Z,$1,b)).n -l*(b-$1) |^ (n+1) /((n+1)!),
REAL);
consider g being Function of REAL, REAL such that
A1: for d be Element of REAL holds g.d = U(d) from FUNCT_2:sch 4;
take g;
let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
g.x= U(x) by A1;
hence thesis;
end;
theorem Th27:
for n be Nat, f be PartFunc of REAL,REAL, Z be Subset
of REAL st Z c= dom f & f is_differentiable_on n,Z
for a,b be Real st a < b &
[.a,b.] c=Z & (diff(f,Z).n)|[.a,b.] is continuous & f is_differentiable_on (n+1
), ].a,b.[
ex c be Real st c in ].a, b.[ & f.b = Partial_Sums(Taylor(f,Z,
a,b)).n + (diff(f,].a,b.[).(n+1)).c * (b-a) |^ (n+1) / ((n+1)!)
proof
let n be Nat;
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL such that
A1: Z c= dom f & f is_differentiable_on n, Z;
let a,b be Real such that
A2: a < b and
A3: [.a,b.] c=Z & (diff(f,Z).n)|[.a,b.] is continuous & f
is_differentiable_on (n+1), ].a,b.[;
b-a <> 0 by A2;
then
A4: (b-a) |^ (n+1) <> 0 by CARD_4:3;
deffunc F(Real) =In(f.b-Partial_Sums(Taylor(f,Z,$1,b)).n,REAL);
reconsider l=F(a)/(((b-a) |^ (n+1))/((n+1)!)) as Real;
consider g be Function of REAL,REAL such that
A5: for x be Real
holds g.x=f.b-Partial_Sums(Taylor(f,Z,x,b)).n -l*(b-x)
|^ (n+1) /((n+1)!) by Th26;
A6: f.b-Partial_Sums(Taylor(f,Z,a,b)).n -l*(b-a) |^ (n+1) /((n+1)!) =F(a)-(
F(a)/(((b-a) |^ (n+1))/((n+1)!))) *((b-a) |^ (n+1)/((n+1)!)) by XCMPLX_1:74
.=F(a)-F(a) by A4,XCMPLX_1:50,87
.=0;
then
A7: g.a=0 by A5;
A8: dom g = REAL by FUNCT_2:def 1;
then
A9: g|[.a,b.] is continuous by A1,A2,A3,A5,A6,Th25;
g is_differentiable_on ].a,b.[ & g.b=0 by A1,A2,A3,A5,A6,A8,Th25;
then consider c be Real such that
A10: c in ].a,b.[ and
A11: diff(g,c)=0 by A2,A8,A7,A9,ROLLE:1;
c in {r where r is Real: a<r & r<b } by A10,RCOMP_1:def 2;
then ex r be Real st c = r & a < r & r < b;
then b-c <> 0;
then
A12: (b-c) |^ n <> 0 by CARD_4:3;
dom g = REAL by FUNCT_2:def 1;
then
-(diff(f,].a,b.[).(n+1)).c * (b-c) |^ (n) /((n)!) +l* (b-c) |^ (n) /((n
)!) =0 by A1,A2,A3,A5,A6,A10,A11,Th25;
then
(diff(f,].a,b.[).(n+1)).c * (b-c) |^ n /((n)!)*(n!) -l* (b-c) |^ n /(n!
)*(n!) =0;
then (diff(f,].a,b.[).(n+1)).c * (b-c) |^ n -l* (b-c) |^ n /(n!)*((n)!) =0
by XCMPLX_1:87;
then
((diff(f,].a,b.[).(n+1)).c * (b-c) |^ n -l* (b-c) |^ n)/((b-c) |^ n) =0
/((b-c) |^ n) by XCMPLX_1:87;
then
(diff(f,].a,b.[).(n+1)).c * (b-c) |^ (n)/((b-c) |^ (n)) -l* (b-c) |^ n/
((b-c) |^ n) =0 by XCMPLX_1:120;
then (diff(f,].a,b.[).(n+1)).c -l* (b-c) |^ n/((b-c) |^ n) =0 by A12,
XCMPLX_1:89;
then f.b-Partial_Sums(Taylor(f,Z,a,b)).n -((diff(f,].a,b.[).(n+1)).c)*(b-a)
|^ (n+1) /((n+1)!) =0 by A6,A12,XCMPLX_1:89;
then
f.b =((diff(f,].a,b.[).(n+1)).c)*(b-a) |^ (n+1) /((n+1)!) +Partial_Sums
(Taylor(f,Z,a,b)).n;
hence thesis by A10;
end;
Lm10: for f be PartFunc of REAL,REAL for Z be Subset of REAL st Z c= dom f for
n be Nat st f is_differentiable_on n, Z
for a,b be Real st a < b &
[.a,b.] c= Z & (diff(f,Z).n)|[.a,b.] is continuous & f is_differentiable_on (n+
1), ].a,b.[ for g be PartFunc of REAL,REAL st dom(g)=Z & for x be Real st x in
Z holds g.x=f.a-Partial_Sums(Taylor(f,Z,x,a)).n holds g.a=0 & g|[.a,b.] is
continuous & g is_differentiable_on ].a,b.[ & for x be Real st x in ].a,b.[
holds diff(g,x)=-(diff(f,].a,b.[).(n+1)).x * (a-x) |^ (n) /(n!)
proof
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL such that
A1: Z c= dom f;
defpred P[Nat] means f is_differentiable_on $1, Z implies
for a,b be Real
st a < b & [.a,b.] c=Z & (diff(f,Z).$1)|[.a,b.] is continuous & f
is_differentiable_on ($1+1), ].a,b.[ for g be PartFunc of REAL,REAL st dom(g)=Z
& for x be Real st x in Z holds g.x=f.a-Partial_Sums(Taylor(f,Z,x,a)).$1 holds
g.a=0 & g|[.a,b.] is continuous & g is_differentiable_on ].a,b.[ & for x be
Real st x in ].a,b.[ holds diff(g,x)=-(diff(f,].a,b.[).($1+1)).x * (a-x) |^ ($1
) / ( ($1)!);
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
assume
A4: f is_differentiable_on k+1, Z;
let a,b be Real such that
A5: a < b and
A6: [.a,b.] c=Z and
A7: (diff(f,Z).(k+1))|[.a,b.] is continuous and
A8: f is_differentiable_on ((k+1)+1), ].a,b.[;
diff(f,Z).k is_differentiable_on Z by A4;
then (diff(f,Z).k)|Z is continuous by FDIFF_1:25;
then
A9: (diff(f,Z).k)|[.a,b.] is continuous by A6,FCONT_1:16;
A10: ].a,b.[ c=[.a,b.] by XXREAL_1:25;
then
A11: ].a,b.[ c= Z by A6,XBOOLE_1:1;
consider gk be PartFunc of REAL,REAL such that
A12: dom(gk)=Z and
A13: for x be Real st x in Z holds gk.x=f.a-Partial_Sums(Taylor(f,Z,x,
a)).k by Lm7;
A14: f is_differentiable_on (k+1), ].a,b.[ by A8,Th23,NAT_1:11;
then
A15: gk is_differentiable_on ].a,b.[ by A3,A4,A5,A6,A9,A12,A13,Th23,NAT_1:11;
A16: gk|[.a,b.] is continuous by A3,A4,A5,A6,A9,A14,A12,A13,Th23,NAT_1:11;
now
A17: diff(f,Z).k is_differentiable_on Z by A4;
k <=(k+1)+1-1 by NAT_1:11;
then
A18: diff(f,].a,b.[).k is_differentiable_on ].a,b.[ by A8;
A19: diff(f,Z).(k+1)=( diff(f,Z).k)`|Z by Def5;
let gk1 be PartFunc of REAL,REAL such that
A20: dom(gk1)=Z and
A21: for x be Real st x in Z holds gk1.x=f.a-Partial_Sums(Taylor(f,Z
,x,a)).(k+1);
A22: a in [.a,b.] by A5,XXREAL_1:1;
then gk1.a=f.a- Partial_Sums(Taylor(f,Z,a,a)).(k+1) by A6,A21
.=f.a- (Partial_Sums(Taylor(f,Z,a,a)).k+Taylor(f,Z,a,a).(k+1)) by
SERIES_1:def 1
.=f.a- Partial_Sums(Taylor(f,Z,a,a)).k-Taylor(f,Z,a,a).(k+1)
.=gk.a -Taylor(f,Z,a,a).(k+1) by A6,A13,A22
.=0 -Taylor(f,Z,a,a).(k+1) by A3,A4,A5,A6,A9,A14,A12,A13,Th23,NAT_1:11
.=0 - (diff(f,Z).(k+1)).a * (a-a) |^ (k+1) /((k+1)!) by Def7
.=0 - (diff(f,Z).(k+1)).a * (0|^k*0) /((k+1)!) by NEWTON:6
.=0;
hence gk1.a=0;
consider h be PartFunc of REAL,REAL such that
A23: dom(h)=[#]REAL and
A24: for x be Real holds h.x=1*(a-x) |^ (k+1) /((k+1)!) and
A25: for x be Real holds h is_differentiable_in x & diff(h,x)=-1* (a
-x) |^ (k) /((k)!) by Lm6;
A26: dom(diff(f,Z).(k+1) (#)h) = dom (diff(f,Z).(k+1)) /\ dom(h) by
VALUED_1:def 4
.= Z /\ REAL by A23,A19,A17,FDIFF_1:def 7
.= Z by XBOOLE_1:28;
A27: dom(gk-diff(f,Z).(k+1) (#)h) =dom(gk) /\ dom(diff(f,Z).(k+1) (#)h)
by VALUED_1:12
.=Z by A12,A26;
thus gk1|[.a,b.] is continuous
proof
set ghk=gk-((diff(f,Z).(k+1)) (#) h);
for x be Real st x in REAL
holds h is_differentiable_in x by A25;
then h is_differentiable_on REAL by A23,FDIFF_1:9;
then h|REAL is continuous by FDIFF_1:25;
then
A28: h|[.a,b.] is continuous by FCONT_1:16;
now
let x be Element of REAL such that
A29: x in Z;
thus gk1.x=f.a-Partial_Sums(Taylor(f,Z,x,a)).(k+1) by A21,A29
.=f.a- (Partial_Sums(Taylor(f,Z,x,a)).k+Taylor(f,Z,x,a).(k+1))
by SERIES_1:def 1
.=f.a-Partial_Sums(Taylor(f,Z,x,a)).k-Taylor(f,Z,x,a).(k+1)
.=gk.x -Taylor(f,Z,x,a).(k+1) by A13,A29
.=gk.x - (diff(f,Z).(k+1)).x * (a-x) |^ (k+1) /((k+1)!) by Def7
.=gk.x - (diff(f,Z).(k+1)).x * (1*(a-x) |^ (k+1) /((k+1)!)) by
XCMPLX_1:74
.=gk.x - (diff(f,Z).(k+1)).x * h.x by A24
.=gk.x - ((diff(f,Z).(k+1)) (#) h).x by VALUED_1:5
.=(gk-((diff(f,Z).(k+1)) (#) h)).x by A27,A29,VALUED_1:13;
end;
then
A30: gk1= ghk by A20,A27,PARTFUN1:5;
[.a,b.] c= dom(diff(f,Z).(k+1)) by A6,A19,A17,FDIFF_1:def 7;
then ((diff(f,Z).(k+1)) (#) h)|([.a,b.] /\ [.a,b.]) is continuous by A7
,A23,A28,FCONT_1:19;
hence thesis by A6,A12,A16,A26,A30,FCONT_1:19;
end;
A31: diff(f,].a,b.[).(k+1)=( diff(f,].a,b.[).k)`|].a,b.[ by Def5;
set gfh=gk-diff(f,].a,b.[).(k+1) (#)h;
A32: dom(diff(f,].a,b.[).(k+1) (#)h) = dom (diff(f,].a,b.[).(k+1)) /\
dom(h) by VALUED_1:def 4
.= ].a,b.[ /\ REAL by A23,A31,A18,FDIFF_1:def 7
.= ].a,b.[ by XBOOLE_1:28;
A33: dom(gk-diff(f, ].a,b.[).(k+1) (#)h)= Z /\ dom(diff(f, ].a,b.[).(k+
1) (#)h) by A12,VALUED_1:12
.= ].a,b.[ by A6,A10,A32,XBOOLE_1:1,28;
A34: for x be Real st x in ].a,b.[ holds (gk-diff(f,Z).(k+1) (#)h).x =(
gk-diff(f,].a,b.[).(k+1) (#)h).x
proof
let x be Real such that
A35: x in ].a,b.[;
thus (gk-diff(f,].a,b.[).(k+1) (#)h).x =gk.x - (diff(f,].a,b.[).(k+1)
(#)h).x by A33,A35,VALUED_1:13
.=gk.x - (diff(f,].a,b.[).(k+1)).x * h.x by VALUED_1:5
.=gk.x - ((diff(f,Z).(k+1))|].a,b.[).x * h.x by A4,A5,A6,A10,Th24,
XBOOLE_1:1
.=gk.x - (diff(f,Z).(k+1)).x * h.x by A35,FUNCT_1:49
.=gk.x - ((diff(f,Z).(k+1)) (#)h).x by VALUED_1:5
.=(gk - ((diff(f,Z).(k+1)) (#)h)).x by A11,A27,A35,VALUED_1:13;
end;
A36: now
let xx be object such that
A37: xx in dom(gfh);
reconsider x=xx as Real by A37;
thus gk1.xx =f.a-Partial_Sums(Taylor(f,Z,x,a)).(k+1) by A11,A21,A33,A37
.=f.a- (Partial_Sums(Taylor(f,Z,x,a)).k + Taylor(f,Z,x,a).(k+1))
by SERIES_1:def 1
.=f.a-Partial_Sums(Taylor(f,Z,x,a)).k -Taylor(f,Z,x,a).(k+1)
.=gk.x - Taylor(f,Z,x,a).(k+1) by A11,A13,A33,A37
.=gk.x - (diff(f,Z).(k+1)).x * (a-x) |^ (k+1) /((k+1)!) by Def7
.=gk.x - (diff(f,Z).(k+1)).x * (1*(a-x) |^ (k+1) /((k+1)!)) by
XCMPLX_1:74
.=gk.x - (diff(f,Z).(k+1)).x * h.x by A24
.=gk.x - (diff(f,Z).(k+1) (#)h).x by VALUED_1:5
.=(gk- (diff(f,Z).(k+1) (#)h)).x by A11,A27,A33,A37,VALUED_1:13
.=gfh.xx by A33,A34,A37;
end;
A38: diff(f,].a,b.[).(k+1) is_differentiable_on ].a,b.[ by A8;
for x be Real st x in ].a,b.[
holds h is_differentiable_in x by A25;
then
A39: h is_differentiable_on ].a,b.[ by A23,FDIFF_1:9;
then
A40: diff(f,].a,b.[).(k+1) (#)h is_differentiable_on ].a,b.[ by A32,A38,
FDIFF_1:21;
then
A41: gfh is_differentiable_on ].a,b.[ by A15,A33,FDIFF_1:19;
dom(gfh)=dom(gk1)/\ ].a,b.[ by A6,A10,A20,A33,XBOOLE_1:1,28;
then
A42: (gk1|].a,b.[)|].a,b.[= gfh|].a,b.[ by A36,FUNCT_1:46;
then gfh|].a,b.[=gk1|].a,b.[ by FUNCT_1:51;
then for x be Real st x in ].a,b.[ holds gk1|].a,b.[
is_differentiable_in x by A41,FDIFF_1:def 6;
hence
A43: gk1 is_differentiable_on ].a,b.[ by A11,A20,FDIFF_1:def 6;
now
let x be Real such that
A44: x in ].a,b.[;
thus diff(gk1,x)=(gk1`|].a,b.[).x by A43,A44,FDIFF_1:def 7
.=((gk1|].a,b.[)`|].a,b.[).x by A43,FDIFF_2:16
.=((gfh|].a,b.[)`|].a,b.[).x by A42,FUNCT_1:51
.=(gfh`|].a,b.[).x by A41,FDIFF_2:16
.=diff(gk,x) - diff(diff(f,].a,b.[).(k+1) (#)h,x) by A15,A33,A40,A44,
FDIFF_1:19
.=-(diff(f,].a,b.[).(k+1)).x * (a-x) |^ (k) /((k)!) -diff(diff(f,
].a,b.[).(k+1) (#)h,x) by A3,A4,A5,A6,A9,A14,A12,A13,A44,Th23,NAT_1:11
.=-(diff(f,].a,b.[).(k+1)).x * (a-x) |^ (k) /((k)!) - ((diff(f,].a
,b.[).(k+1) (#)h)`|].a,b.[).x by A40,A44,FDIFF_1:def 7
.= -(diff(f,].a,b.[).(k+1)).x * (a-x) |^ (k) /((k)!) - ((h.x)*diff
(diff(f,].a,b.[).(k+1),x) + (diff(f,].a,b.[).(k+1).x)*diff(h,x)) by A32,A38,A39
,A44,FDIFF_1:21
.= -(diff(f,].a,b.[).(k+1)).x * (a-x) |^ (k) /((k)!) - (h.x)*diff(
diff(f,].a,b.[).(k+1),x) -(diff(f,].a,b.[).(k+1).x)*diff(h,x)
.= -(diff(f,].a,b.[).(k+1)).x * (a-x) |^ (k) /((k)!) - (1*(a-x) |^
(k+1) /((k+1)!) ) *diff(diff(f,].a,b.[).(k+1),x) -(diff(f,].a,b.[).(k+1).x)*
diff(h,x) by A24
.= -(diff(f,].a,b.[).(k+1)).x * (a-x) |^ (k) /((k)!) - (a-x) |^ (k
+1) /((k+1)!) *diff(diff(f,].a,b.[).(k+1),x) -(diff(f,].a,b.[).(k+1).x) *(-1* (
a-x) |^ (k) /((k)!)) by A25
.= -(diff(f,].a,b.[).(k+1)).x * (a-x) |^ (k) /((k)!) +(diff(f,].a,
b.[).(k+1).x)*(1* (a-x) |^ (k) /((k)!)) - (a-x) |^ (k+1) /((k+1)!) *diff(diff(f
,].a,b.[).(k+1),x)
.= -(diff(f,].a,b.[).(k+1)).x * (a-x) |^ (k) /((k)!) +(diff(f,].a,
b.[).(k+1)).x* (a-x) |^ (k) /((k)!) - (a-x) |^ (k+1) /((k+1)!) *diff(diff(f,].a
,b.[).(k+1),x) by XCMPLX_1:74
.= - (a-x) |^ (k+1) /((k+1)!) *diff(diff(f,].a,b.[).(k+1),x)
.= - (a-x) |^ (k+1) /((k+1)!) *(diff(f,].a,b.[).(k+1)`|].a,b.[).x
by A38,A44,FDIFF_1:def 7
.= - (a-x) |^ (k+1) /((k+1)!) * (diff(f,].a,b.[).((k+1)+1)).x by Def5
.= - (diff(f,].a,b.[).((k+1)+1)).x * (a-x) |^ (k+1) /((k+1)!) by
XCMPLX_1:74;
end;
hence
for x be Real st x in ].a,b.[ holds diff(gk1,x) =-(diff(f,].a,b.[).
((k+1)+1)).x * (a-x) |^ ((k+1)) /((k+1)!);
end;
hence thesis;
end;
A45: P[0]
proof
assume f is_differentiable_on 0, Z;
let a,b be Real such that
A46: a < b and
A47: [.a,b.] c= Z and
A48: (diff(f,Z).0)|[.a,b.] is continuous and
A49: f is_differentiable_on (0+1), ].a,b.[;
A50: ].a,b.[ c=[.a,b.] by XXREAL_1:25;
then
A51: ].a,b.[ c= Z by A47,XBOOLE_1:1;
let g be PartFunc of REAL,REAL such that
A52: dom(g)=Z and
A53: for x be Real st x in Z holds g.x=f.a-Partial_Sums(Taylor(f,Z,x,a) ).0;
A54: a in [.a,b.] by A46,XXREAL_1:1;
hence g.a=f.a-Partial_Sums(Taylor(f,Z,a,a)).(0) by A47,A53
.=f.a-Taylor(f,Z,a,a).0 by SERIES_1:def 1
.=f.a - (diff(f,Z).(0)).a * (a-a) |^ (0) /((0)!) by Def7
.=f.a - (f|Z).a * (a-a) |^ (0) /((0)!) by Def5
.=f.a - f.a * (a-a) |^ (0) /((0)!) by A47,A54,FUNCT_1:49
.=f.a - f.a * 1 by NEWTON:4,12
.=0;
consider y be PartFunc of REAL,REAL such that
A55: dom(y)=[#]REAL and
A56: for x be Real holds y.x=(f.a-x) and
A57: for x be Real holds y is_differentiable_in x & diff(y,x)=-1 by Lm5;
rng(f) c= REAL;
then
A58: dom(y*f) = dom(f) by A55,RELAT_1:27;
for x be Real st x in REAL holds y is_differentiable_in x by A57;
then y is_differentiable_on REAL by A55,FDIFF_1:9;
then y|REAL is continuous by FDIFF_1:25;
then
A59: y|(f.:[.a,b.]) is continuous by FCONT_1:16;
rng(f) c= dom(y) by A55;
then
A60: dom(y*f) = dom(f) by RELAT_1:27;
A61: [.a,b.] c= dom(f) by A1,A47,XBOOLE_1:1;
then
A62: ].a,b.[ c= dom(f) by A50,XBOOLE_1:1;
diff(f,].a,b.[).0 is_differentiable_on ].a,b.[ by A49;
then f|].a,b.[ is_differentiable_on ].a,b.[ by Def5;
then for x be Real st x in ].a,b.[
holds f|].a,b.[ is_differentiable_in x by FDIFF_1:9;
then
A63: f is_differentiable_on ].a,b.[ by A62,FDIFF_1:def 6;
A64: for x be Real st x in ].a,b.[ holds y *f is_differentiable_in x &
diff( y*f,x) =-diff(f,].a,b.[).(0+1).x * (a-x) |^ (0) / ( (0)!)
proof
A65: diff(f,].a,b.[).(0+1) = ( diff(f,].a,b.[).0)`|].a,b.[ by Def5
.= (f|].a,b.[)`|].a,b.[ by Def5
.= f`|].a,b.[ by A63,FDIFF_2:16;
let x be Real such that
A66: x in ].a,b.[;
A67: f is_differentiable_in x by A63,A66,FDIFF_1:9;
A68: y is_differentiable_in f.x by A57;
hence y*f is_differentiable_in x by A67,FDIFF_2:13;
A69: (a-x) |^ (0) /((0)!) = 1 by NEWTON:4,12;
thus diff( y*f,x) = diff(y, f.x)*diff(f,x) by A68,A67,FDIFF_2:13
.= diff(y,f.x)*(f`|].a,b.[).x by A63,A66,FDIFF_1:def 7
.= (-1)*diff(f,].a,b.[).(0+1).x by A57,A65
.=-diff(f,].a,b.[).(0+1).x *((a-x) |^ (0) /((0)!)) by A69
.=-diff(f,].a,b.[).(0+1).x *(a-x) |^ (0) /((0)!) by XCMPLX_1:74;
end;
then for x be Real st x in ].a,b.[
holds y *f is_differentiable_in x;
then
A70: y*f is_differentiable_on ].a,b.[ by A62,A60,FDIFF_1:9;
A71: dom((y*f)|[.a,b.])=dom(y*f) /\ [.a,b.] by RELAT_1:61
.=[.a,b.] by A1,A47,A58,XBOOLE_1:1,28
.=Z /\ [.a,b.] by A47,XBOOLE_1:28
.=dom(g|[.a,b.]) by A52,RELAT_1:61;
A72: now
let xx be object such that
A73: xx in dom(g|[.a,b.]);
reconsider x=xx as Real by A73;
dom(g|[.a,b.])=dom(g) /\ [.a,b.] by RELAT_1:61;
then dom(g|[.a,b.]) c= [.a,b.] by XBOOLE_1:17;
then
A74: x in [.a,b.] by A73;
thus (g|[.a,b.]).xx =g.x by A73,FUNCT_1:47
.=f.a-Partial_Sums(Taylor(f,Z,x,a)).(0) by A47,A53,A74
.=f.a-Taylor(f,Z,x,a).0 by SERIES_1:def 1
.=f.a - (diff(f,Z).(0)).x * (a-x) |^ (0) /((0)!) by Def7
.=f.a - (f|Z).x * (a-x) |^ (0) /((0)!) by Def5
.=f.a - f.x * (a-x) |^ (0) /((0)!) by A47,A74,FUNCT_1:49
.=f.a - f.x * 1 by NEWTON:4,12
.=y.(f.x) by A56
.=(y*f).x by A61,A74,FUNCT_1:13
.=((y*f)|[.a,b.]).xx by A71,A73,FUNCT_1:47;
end;
f|Z|[.a,b.] is continuous by A48,Def5;
then (f|Z)| [.a,b.]|[.a,b.] is continuous by FCONT_1:15;
then (f|[.a,b.])|[.a,b.] is continuous by A47,FUNCT_1:51;
then f|[.a,b.] is continuous by FCONT_1:15;
then (y*f)|[.a,b.] is continuous by A59,FCONT_1:25;
hence g|[.a,b.] is continuous by A71,A72,FUNCT_1:2;
A75: dom((y*f)|].a,b.[)=dom(y*f) /\ ].a,b.[ by RELAT_1:61
.=].a,b.[ by A50,A61,A60,XBOOLE_1:1,28
.=Z /\ ].a,b.[ by A47,A50,XBOOLE_1:1,28
.=dom(g|].a,b.[) by A52,RELAT_1:61;
now
let xx be object such that
A76: xx in dom(g|].a,b.[);
reconsider x=xx as Real by A76;
dom(g|].a,b.[)=dom(g) /\ ].a,b.[ by RELAT_1:61;
then dom(g|].a,b.[) c= ].a,b.[ by XBOOLE_1:17;
then
A77: x in ].a,b.[ by A76;
A78: (a-x) |^ (0) /((0)!)=1 by NEWTON:4,12;
thus (g|].a,b.[).xx = g.x by A76,FUNCT_1:47
.=f.a-Partial_Sums(Taylor(f,Z,x,a)).0 by A53,A51,A77
.=f.a- Taylor(f,Z,x,a).0 by SERIES_1:def 1
.=f.a - (diff(f,Z).(0)).x * (a-x) |^ 0 /(0!) by Def7
.=f.a - (f|Z).x * (a-x) |^ 0 /((0)!) by Def5
.=f.a - f.x * (a-x) |^ 0 /(0!) by A51,A77,FUNCT_1:49
.=f.a - f.x * ((a-x) |^ 0 /(0!)) by XCMPLX_1:74
.=y.(f.x) by A56,A78
.=(y*f).x by A62,A77,FUNCT_1:13
.=((y*f)|].a,b.[).xx by A75,A76,FUNCT_1:47;
end;
then
A79: g|].a,b.[=(y*f)|].a,b.[ by A75,FUNCT_1:2;
then g|].a,b.[ is_differentiable_on ].a,b.[ by A70,FDIFF_2:16;
then for x be Real st x in ].a,b.[
holds g|].a,b.[ is_differentiable_in x by FDIFF_1:9;
hence
A80: g is_differentiable_on ].a,b.[ by A52,A51,FDIFF_1:def 6;
now
let x be Real such that
A81: x in ].a,b.[;
thus g is_differentiable_in x by A80,A81,FDIFF_1:9;
thus diff(g,x) = (g`|].a,b.[).x by A80,A81,FDIFF_1:def 7
.=((g|].a,b.[)`|].a,b.[).x by A80,FDIFF_2:16
.= ((y*f)`|].a,b.[).x by A79,A70,FDIFF_2:16
.=diff( y*f,x) by A70,A81,FDIFF_1:def 7
.=-diff(f,].a,b.[).(0+1).x * (a-x) |^ 0 / (0!) by A64,A81;
end;
hence thesis;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A45,A2);
hence thesis;
end;
Lm11: for n be Nat for f be PartFunc of REAL,REAL for Z be Subset
of REAL st Z c= dom f & f is_differentiable_on n, Z
for a,b be Real st a < b &
[.a,b.] c= Z & (diff(f,Z).n)|[.a,b.] is continuous & f is_differentiable_on (n+
1), ].a,b.[ ex g be PartFunc of REAL,REAL st (dom(g)=Z & (for x be Real st x in
Z holds g.x=f.a-Partial_Sums(Taylor(f,Z,x,a)).n) & g.a=0 & g|[.a,b.] is
continuous & g is_differentiable_on ].a,b.[ & for x be Real st x in ].a,b.[
holds diff(g,x)=-(diff(f,].a,b.[).(n+1)).x * (a-x) |^ (n) /(n!))
proof
let n be Nat;
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL such that
A1: Z c= dom f & f is_differentiable_on n, Z;
let a,b be Real such that
A2: a < b & [.a,b.] c= Z & (diff(f,Z).n)|[.a,b.] is continuous & f
is_differentiable_on (n+1), ].a,b.[;
consider g be PartFunc of REAL,REAL such that
A3: dom(g)=Z & for x be Real st x in Z holds g.x=f.a-Partial_Sums(Taylor
(f,Z,x,a )).n by Lm7;
take g;
thus thesis by A1,A2,A3,Lm10;
end;
theorem Th28:
for n be Nat, f be PartFunc of REAL,REAL, Z be Subset
of REAL st Z c= dom f & f is_differentiable_on n,Z
for a,b be Real st a < b &
[.a,b.] c=Z & (diff(f,Z).n)|[.a,b.] is continuous & f is_differentiable_on (n+1
), ].a,b.[ holds for l be Real, g be PartFunc of REAL,REAL st dom(g)=[#]REAL &
( for x be Real
holds g.x = f.a-Partial_Sums(Taylor(f,Z,x,a)).n -l*(a-x) |^ (n+
1) /((n+1)!) ) & f.a-Partial_Sums(Taylor(f,Z,b,a)).n-l*(a-b) |^ (n+1)/((n+1)!)
=0 holds g is_differentiable_on ].a,b.[ & g.b=0 & g.a=0 & g|[.a,b.] is
continuous & for x be Real st x in ].a,b.[ holds diff(g,x) = -(diff(f,].a,b.[).
(n+1)).x * (a-x) |^ n /(n!) +l* (a-x) |^ n /((n)!)
proof
let n be Nat;
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL such that
A1: Z c= dom f & f is_differentiable_on n, Z;
let a,b be Real such that
A2: a < b and
A3: [.a,b.] c=Z and
A4: (diff(f,Z).n)|[.a,b.] is continuous & f is_differentiable_on (n+1),
].a,b.[;
let l be Real;
consider p be PartFunc of REAL,REAL such that
A5: dom(p)=[#]REAL and
A6: for x be Real holds p.x=l*(a-x) |^ (n+1) /((n+1)!) and
A7: for x be Real holds p is_differentiable_in x & diff(p,x)=-l* (a-x)
|^ (n) /((n)!) by Lm6;
consider h be PartFunc of REAL,REAL such that
A8: dom(h)=Z and
A9: for x be Real st x in Z holds h.x=f.a-Partial_Sums(Taylor(f,Z,x,a)) . n and
A10: h.a=0 and
A11: h|[.a,b.] is continuous and
A12: h is_differentiable_on ].a,b.[ and
A13: for x be Real st x in ].a,b.[ holds diff(h,x)=-(diff(f,].a,b.[).(n+
1 )).x * (a-x) |^ (n) /(n!) by A1,A2,A3,A4,Lm11;
A14: [.a,b.] c= dom h /\ dom p by A3,A8,A5,XBOOLE_1:19;
let g be PartFunc of REAL,REAL such that
A15: dom(g)=[#]REAL and
A16: for x be Real
holds g.x=f.a-Partial_Sums(Taylor(f,Z,x,a)).n -l*(a-x)
|^ (n+1) /((n+1)!) and
A17: f.a-Partial_Sums(Taylor(f,Z,b,a)).n -l*(a-b) |^ (n+1) /((n+1)!) =0;
set hp=h-p;
A18: dom(hp)=dom(h) /\ dom(p) by VALUED_1:12
.=Z by A8,A5,XBOOLE_1:28;
A19: for x be object st x in dom(hp) holds hp.x=g.x
proof
let x be object such that
A20: x in dom(hp);
reconsider xx=x as Real by A20;
thus hp.x=h.xx-p.xx by A20,VALUED_1:13
.=(f.a-Partial_Sums(Taylor(f,Z,xx,a)).n) -p.xx by A9,A18,A20
.=(f.a-Partial_Sums(Taylor(f,Z,xx,a)).n) -(l*(a-xx) |^ (n+1)/((n+1)!))
by A6
.=g.x by A16;
end;
for x be Real st x in REAL holds p is_differentiable_in x by A7;
then p is_differentiable_on REAL by A5,FDIFF_1:9;
then p|REAL is continuous by FDIFF_1:25;
then
A21: p|[.a,b.] is continuous by FCONT_1:16;
].a,b.[ c=[.a,b.] by XXREAL_1:25;
then
A22: ].a,b.[ c= Z by A3,XBOOLE_1:1;
A23: dom(hp)=dom(g) /\ Z by A15,A18,XBOOLE_1:28;
then
A24: hp|].a,b.[ = (g|Z)|].a,b.[ by A19,FUNCT_1:46
.= g|].a,b.[ by A22,FUNCT_1:51;
A25: for x be Real st x in ].a,b.[ holds hp is_differentiable_in x & diff(hp
,x)=-(diff(f,].a,b.[).(n+1)).x * (a-x) |^ n /(n!) +l* (a-x) |^ n /(n!)
proof
let x be Real such that
A26: x in ].a,b.[;
A27: h is_differentiable_in x by A12,A26,FDIFF_1:9;
A28: p is_differentiable_in x by A7;
hence hp is_differentiable_in x by A27,FDIFF_1:14;
thus diff(hp,x)=diff(h,x)-diff(p,x) by A27,A28,FDIFF_1:14
.=-(diff(f,].a,b.[).(n+1)).x * (a-x) |^ (n) /(n!) -diff(p,x) by A13,A26
.=-(diff(f,].a,b.[).(n+1)).x * (a-x) |^ (n) /(n!) -(-l* (a-x) |^ (n) /
((n)!)) by A7
.=-(diff(f,].a,b.[).(n+1)).x * (a-x) |^ (n) /(n!) +l* (a-x) |^ (n) /((
n)!);
end;
then for x be Real st x in ].a,b.[ holds hp is_differentiable_in x;
then
A29: hp is_differentiable_on ].a,b.[ by A18,A22,FDIFF_1:9;
then for x be Real st x in ].a,b.[
holds hp|].a,b.[ is_differentiable_in x by FDIFF_1:def 6;
hence
A30: g is_differentiable_on ].a,b.[ by A15,A24,FDIFF_1:def 6;
thus g.b=0 by A16,A17;
A31: a in [.a,b.] by A2,XXREAL_1:1;
then g.a=hp.a by A3,A18,A19
.=h.a-p.a by A3,A18,A31,VALUED_1:13
.=0-(l*(a-a) |^ (n+1)/((n+1)!)) by A10,A6
.=0-(l*(0|^ n*0)/((n+1)!)) by NEWTON:6
.=0;
hence g.a=0;
hp|[.a,b.] = (g|Z)|[.a,b.] by A23,A19,FUNCT_1:46
.= g|[.a,b.] by A3,FUNCT_1:51;
hence g|[.a,b.] is continuous by A11,A14,A21,FCONT_1:18;
thus for x be Real st x in ].a,b.[ holds diff(g,x) = -(diff(f,].a,b.[).(n+1)
).x * (a-x) |^ n /((n)!)+l* (a-x) |^ n /((n)!)
proof
let x be Real such that
A32: x in ].a,b.[;
thus diff(g,x) = (g`|].a,b.[).x by A30,A32,FDIFF_1:def 7
.=((g|].a,b.[)`|].a,b.[).x by A30,FDIFF_2:16
.=(hp`|].a,b.[).x by A24,A29,FDIFF_2:16
.=diff(hp,x) by A29,A32,FDIFF_1:def 7
.=-(diff(f,].a,b.[).(n+1)).x * (a-x) |^ (n) /(n!) +l* (a-x) |^ (n) /((
n)!) by A25,A32;
end;
end;
theorem Th29:
for n be Nat, f be PartFunc of REAL,REAL, Z be Subset
of REAL st Z c= dom f & f is_differentiable_on n,Z
for a,b be Real st a < b &
[.a,b.] c=Z & (diff(f,Z).n)|[.a,b.] is continuous & f is_differentiable_on (n+1
), ].a,b.[ holds ex c be Real st c in ].a, b.[ & f.a = Partial_Sums(Taylor(f,Z,
b,a)).n + (diff(f,].a,b.[).(n+1)).c * (a-b) |^ (n+1) /((n+1)!)
proof
let n be Nat;
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL such that
A1: Z c= dom f & f is_differentiable_on n, Z;
let a,b be Real such that
A2: a < b and
A3: [.a,b.] c=Z & (diff(f,Z).n)|[.a,b.] is continuous & f
is_differentiable_on (n+1), ].a,b.[;
reconsider aa=a, bb=b as Real;
a-b <> 0 by A2;
then
A4: (a-b) |^ (n+1) <> 0 by CARD_4:3;
deffunc F(Real) =In(f.a-Partial_Sums(Taylor(f,Z,$1,a)).n,REAL);
reconsider l=F(bb)/(((a-b) |^ (n+1))/((n+1)!)) as Real;
consider g be Function of REAL,REAL such that
A5: for x be Real
holds g.x=f.a-Partial_Sums(Taylor(f,Z,x,a)).n -l*(a-x)|^ (n+1) /((n+1)!)
by Th26;
A6: f.a-Partial_Sums(Taylor(f,Z,b,a)).n -l*(a-b) |^ (n+1) /((n+1)!)
=F(bb)-(
F(bb)/(((a-b) |^ (n+1))/((n+1)!))) *((a-b) |^ (n+1)/((n+1)!)) by XCMPLX_1:74
.=F(bb)-F(bb) by A4,XCMPLX_1:50,87
.=0;
then
A7: g.b=0 by A5;
A8: dom g = REAL by FUNCT_2:def 1;
then
A9: g|[.a,b.] is continuous by A1,A2,A3,A5,A6,Th28;
g is_differentiable_on ].a,b.[ & g.a=0 by A1,A2,A3,A5,A6,A8,Th28;
then consider c be Real such that
A10: c in ].a,b.[ and
A11: diff(g,c)=0 by A2,A8,A7,A9,ROLLE:1;
c in {r where r is Real: a<r & r<b } by A10,RCOMP_1:def 2;
then ex r be Real st c = r & a < r & r < b;
then a-c <> 0;
then
A12: (a-c) |^ (n) <> 0 by CARD_4:3;
dom g = REAL by FUNCT_2:def 1;
then
-(diff(f,].a,b.[).(n+1)).c * (a-c) |^ (n) /((n)!) +l* (a-c) |^ (n) /((n
)!) =0 by A1,A2,A3,A5,A6,A10,A11,Th28;
then
(diff(f,].a,b.[).(n+1)).c * (a-c) |^ (n) /((n)!)*((n)!) -l* (a-c) |^ (n
) /((n)!)*((n)!) =0;
then
(diff(f,].a,b.[).(n+1)).c * (a-c) |^ (n) -l* (a-c) |^ (n) /((n)!)*((n)!
) =0 by XCMPLX_1:87;
then
((diff(f,].a,b.[).(n+1)).c * (a-c) |^ (n) -l* (a-c) |^ (n))/((a-c) |^ (
n)) =0/((a-c) |^ (n)) by XCMPLX_1:87;
then
(diff(f,].a,b.[).(n+1)).c * (a-c) |^ (n)/((a-c) |^ (n)) -l* (a-c) |^ (n
)/((a-c) |^ n)=0 by XCMPLX_1:120;
then (diff(f,].a,b.[).(n+1)).c -l* (a-c) |^ (n)/((a-c) |^ n)=0 by A12,
XCMPLX_1:89;
then (diff(f,].a,b.[).(n+1)).c = l by A12,XCMPLX_1:89;
then
f.a =((diff(f,].a,b.[).(n+1)).c)*(a-b) |^ (n+1) /((n+1)!) +Partial_Sums
(Taylor(f,Z,b,a)).n by A6;
hence thesis by A10;
end;
theorem Th30:
for f be PartFunc of REAL,REAL, Z be Subset of REAL, Z1 be open
Subset of REAL st Z1 c= Z for n be Nat st f is_differentiable_on n,Z
holds diff(f,Z).n | Z1 = diff(f,Z1).n
proof
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
let Z1 be open Subset of REAL such that
A1: Z1 c= Z;
defpred P[Nat] means
f is_differentiable_on $1,Z implies diff(f,Z
).$1 | Z1 = diff(f,Z1).$1;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
assume
A4: f is_differentiable_on (k+1), Z;
A5: (diff(f,Z).k) is_differentiable_on Z by A4;
then
A6: (diff(f,Z).k) is_differentiable_on Z1 by A1,FDIFF_1:26;
then
A7: dom((diff(f,Z).k)`| Z1) = Z1 by FDIFF_1:def 7;
A8: dom(((diff(f,Z).k)`|Z)| Z1) =dom((diff(f,Z).k)`|Z) /\ Z1 by RELAT_1:61
.=Z /\ Z1 by A5,FDIFF_1:def 7
.=Z1 by A1,XBOOLE_1:28;
A9: now
let x be Element of REAL such that
A10: x in dom(((diff(f,Z).k)`|Z)| Z1);
thus (((diff(f,Z).k)`|Z)| Z1).x =((diff(f,Z).k)`|Z).x by A8,A10,
FUNCT_1:49
.=diff((diff(f,Z).k),x) by A1,A5,A8,A10,FDIFF_1:def 7
.=((diff(f,Z).k)`|Z1).x by A6,A8,A10,FDIFF_1:def 7;
end;
thus diff(f,Z).(k+1) | Z1 =((diff(f,Z).k)`|Z)| Z1 by Def5
.=(diff(f,Z).k)`| Z1 by A8,A7,A9,PARTFUN1:5
.=(diff(f,Z1).k)`| Z1 by A3,A4,A6,Th23,FDIFF_2:16,NAT_1:11
.=diff(f,Z1).(k+1) by Def5;
end;
A11: P[0]
proof
assume f is_differentiable_on 0, Z;
thus (diff(f,Z).0) |Z1 =(f|Z)|Z1 by Def5
.=f|Z1 by A1,FUNCT_1:51
.=diff(f,Z1).0 by Def5;
end;
thus for k be Nat holds P[k] from NAT_1: sch 2(A11,A2);
end;
theorem Th31:
for f be PartFunc of REAL,REAL, Z be Subset of REAL, Z1 be open
Subset of REAL st Z1 c= Z for n be Nat st f is_differentiable_on n+1
,Z holds f is_differentiable_on n+1, Z1
proof
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
let Z1 be open Subset of REAL such that
A1: Z1 c= Z;
let n be Nat such that
A2: f is_differentiable_on n+1, Z;
now
let k be Nat such that
A3: k <= (n+1)-1;
(diff(f,Z).k) is_differentiable_on Z by A2,A3;
then (diff(f,Z).k) is_differentiable_on Z1 by A1,FDIFF_1:26;
then
A4: (diff(f,Z).k)|Z1 is_differentiable_on Z1 by FDIFF_2:16;
n <= n+1 by NAT_1:11;
then k <= n+1 by A3,XXREAL_0:2;
hence (diff(f,Z1).k) is_differentiable_on Z1 by A1,A2,A4,Th23,Th30;
end;
hence thesis;
end;
theorem Th32:
for f be PartFunc of REAL,REAL, Z be Subset of REAL, x be Real
st x in Z for n be Nat holds f.x = Partial_Sums(Taylor(f,Z,x,x)).n
proof
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
let x be Real such that
A1: x in Z;
defpred P[Nat] means f.x=Partial_Sums(Taylor(f, Z,x,x)).$1;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
thus Partial_Sums(Taylor(f, Z,x,x)).(k+1) =Partial_Sums(Taylor(f, Z,x,x)).
k +Taylor(f, Z,x,x).(k+1) by SERIES_1:def 1
.=f.x +(diff(f,Z).(k+1)).x * (x-x) |^ (k+1) /((k+1)!) by A3,Def7
.=f.x + (diff(f,Z).(k+1)).x * (0|^k*0) /((k+1)!) by NEWTON:6
.=f.x;
end;
Partial_Sums(Taylor(f, Z,x,x)).0 =Taylor(f, Z,x,x).0 by SERIES_1:def 1
.=(diff(f,Z).0).x * (x-x) |^ 0 /(0!) by Def7
.=(f|Z).x * (x-x) |^ 0 /(0!) by Def5
.=(f|Z).x * 1/1 by NEWTON:4,12
.=f.x by A1,FUNCT_1:49;
then
A4: P[0];
for k be Nat holds P[k] from NAT_1: sch 2(A4,A2);
hence thesis;
end;
::$N Taylor's Theorem
::$L https://en.wikipedia.org/wiki/Taylor's_theorem Taylor's Theorem
theorem
for n be Nat, f be PartFunc of REAL,REAL, x0,r be Real st
].x0-r,x0+r.[ c= dom f & 0 < r & f is_differentiable_on n+1, ].x0-r,x0+r.[
for x be Real st x in ].x0-r, x0+r.[
ex s be Real st 0 < s & s < 1 & f.x=
Partial_Sums(Taylor(f, ].x0-r,x0+r.[,x0,x)).n + (diff(f,].x0-r,x0+r.[).(n+1)).(
x0+s*(x-x0)) * (x-x0) |^ (n+1) / ((n+1)!)
proof
let n be Nat;
let f be PartFunc of REAL,REAL;
let x0,r be Real such that
A1: ].x0-r,x0+r.[ c= dom f and
A2: 0 < r and
A3: f is_differentiable_on n+1, ].x0-r,x0+r.[;
let x be Real such that
A4: x in ].x0-r, x0+r.[;
now
per cases by XXREAL_0:1;
case
A5: x < x0;
|.x0-x0.|=0 by ABSVALUE:2;
then x0 in ].x0-r, x0+r.[ by A2,RCOMP_1:1;
then
A6: [.x,x0.] c= ].x0-r,x0+r.[ by A4,XXREAL_2:def 12;
diff(f,].x0-r,x0+r.[).n is_differentiable_on ].x0-r,x0+r.[ by A3;
then (diff(f,].x0-r,x0+r.[).n)|].x0-r,x0+r.[ is continuous by FDIFF_1:25;
then
A7: (diff(f,].x0-r,x0+r.[).n)|[.x,x0.] is continuous by A6,FCONT_1:16;
A8: f is_differentiable_on n, ].x0-r,x0+r.[ by A3,Th23,NAT_1:11;
set t= x0-x;
A9: t > 0 by A5,XREAL_1:50;
A10: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25;
then f is_differentiable_on n+1, ].x,x0.[ by A3,A6,Th31,XBOOLE_1:1;
then consider c be Real such that
A11: c in ].x,x0.[ and
A12: f.x=Partial_Sums(Taylor(f, ].x0-r,x0+r.[,x0,x)).n + (diff(f,].x
,x0.[).(n+1)).c * (x-x0) |^ (n+1) /((n+1)!) by A1,A5,A6,A8,A7,Th29;
take s=(x0-c)/t;
A13: x0+s*(x-x0) =x0-((x0-c)/t)*t .=x0-(x0-c) by A9,XCMPLX_1:87
.=c;
c in {p where p is Real : x0-t<p & p<x0} by A11,RCOMP_1:def 2;
then
A14: ex g be Real st g=c & x0-t<g & g<x0;
then 0<x0-c by XREAL_1:50;
then 0/t < (x0-c)/t by A9,XREAL_1:74;
hence 0<s;
x0-t+t < c+t by A14,XREAL_1:8;
then x0-c < t by XREAL_1:19;
then (x0-c)/t<t/t by A9,XREAL_1:74;
hence s<1 by A9,XCMPLX_1:60;
diff(f,].x,x0.[).(n+1).c = (diff(f,].x0-r,x0+r.[).(n+1) |].x,x0.[).
c by A3,A6,A10,Th30,XBOOLE_1:1
.= (diff(f,].x0-r,x0+r.[).(n+1)).c by A11,FUNCT_1:49;
hence
f.x=Partial_Sums(Taylor(f, ].x0-r,x0+r.[,x0,x)).n + (diff(f,].x0-r,
x0+r.[).(n+1)).(x0+s*(x-x0)) * (x-x0) |^ (n+1) /((n+1)!) by A12,A13;
end;
case
A15: x = x0;
set s=1/2;
take s;
thus 0 < s & s < 1;
set c = x0+s*(x-x0);
thus Partial_Sums(Taylor(f, ].x0-r,x0+r.[,x0,x)).n + (diff(f,].x0-r,x0+r
.[).(n+1)).(x0+s*(x-x0)) * (x-x0) |^ (n+1) /((n+1)!) =f.x + (diff(f,].x0-r,x0+r
.[).(n+1)).c * (x-x) |^ (n+1) /((n+1)!) by A4,A15,Th32
.=f.x + (diff(f,].x0-r,x0+r.[).(n+1)).c * (0|^n*0) /((n+1)!) by
NEWTON:6
.=f.x;
end;
case
A16: x > x0;
set t= x-x0;
A17: f is_differentiable_on n, ].x0-r,x0+r.[ by A3,Th23,NAT_1:11;
|.x0-x0.|=0 by ABSVALUE:2;
then x0 in ].x0-r, x0+r.[ by A2,RCOMP_1:1;
then
A18: [.x0,x.] c= ].x0-r,x0+r.[ by A4,XXREAL_2:def 12;
diff(f,].x0-r,x0+r.[).n is_differentiable_on ].x0-r,x0+r.[ by A3;
then (diff(f,].x0-r,x0+r.[).n)|].x0-r,x0+r.[ is continuous by FDIFF_1:25;
then
A19: (diff(f,].x0-r,x0+r.[).n)|[.x0,x.] is continuous by A18,FCONT_1:16;
A20: ].x0,x.[ c= [.x0,x.] by XXREAL_1:25;
then f is_differentiable_on n+1, ].x0,x.[ by A3,A18,Th31,XBOOLE_1:1;
then consider c be Real such that
A21: c in ].x0,x.[ and
A22: f.x=Partial_Sums(Taylor(f, ].x0-r,x0+r.[,x0,x)).n + (diff(f,].
x0,x.[).(n+1)).c * (x-x0) |^ (n+1) /((n+1)!) by A1,A16,A18,A17,A19,Th27;
take s=(c-x0)/t;
A23: t > 0 by A16,XREAL_1:50;
then
A24: x0+s*(x-x0) = x0+(c-x0) by XCMPLX_1:87
.=c;
c in {p where p is Real : x0<p & p<x0+t} by A21,RCOMP_1:def 2;
then
A25: ex g be Real st g=c & x0<g & g<x0+t;
then 0<c-x0 by XREAL_1:50;
then 0/t < (c-x0)/t by A23,XREAL_1:74;
hence 0<s;
c-x0<t by A25,XREAL_1:19;
then (c-x0)/t<t/t by A23,XREAL_1:74;
hence s<1 by A23,XCMPLX_1:60;
diff(f,].x0,x.[).(n+1).c = (diff(f,].x0-r,x0+r.[).(n+1) |].x0,x.[).
c by A3,A18,A20,Th30,XBOOLE_1:1
.= (diff(f,].x0-r,x0+r.[).(n+1)).c by A21,FUNCT_1:49;
hence
f.x=Partial_Sums(Taylor(f, ].x0-r,x0+r.[,x0,x)).n + (diff(f,].x0-r,
x0+r.[).(n+1)).(x0+s*(x-x0)) * (x-x0) |^ (n+1) /((n+1)!) by A22,A24;
end;
end;
hence thesis;
end;