:: The {M}aclaurin Expansions
:: by Akira Nishino and Yasunari Shidama
::
:: Received July 6, 2005
:: Copyright (c) 2005-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, RCOMP_1, SUBSET_1, REAL_1, COMPLEX1, NEWTON, ARYTM_3,
RELAT_1, CARD_1, PARTFUN1, SEQ_1, TAYLOR_1, XXREAL_1, ARYTM_1, TARSKI,
FDIFF_1, FUNCT_1, SERIES_1, REALSET1, XBOOLE_0, SIN_COS, XXREAL_0,
VALUED_0, VALUED_1, SEQ_2, ORDINAL2, CARD_3, ABIAN, TAYLOR_2, NAT_1;
notations TARSKI, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, RFUNCT_2, RCOMP_1,
XXREAL_0, XCMPLX_0, XREAL_0, ORDINAL1, NUMBERS, COMPLEX1, REAL_1, NAT_1,
FUNCT_2, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SERIES_1, FDIFF_1, SEQFUNC,
NEWTON, SIN_COS, TAYLOR_1, ABIAN;
constructors ARYTM_0, REAL_1, NAT_1, SEQ_2, RCOMP_1, RFUNCT_2, LIMFUNC1,
FDIFF_1, COMSEQ_3, SIN_COS, ABIAN, TAYLOR_1, SEQFUNC, SERIES_1, VALUED_1,
RELSET_1, COMSEQ_2;
registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RCOMP_1, XBOOLE_0,
VALUED_0, VALUED_1, FUNCT_2, NEWTON, SIN_COS, INT_1, ORDINAL1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TAYLOR_1;
equalities VALUED_1, SUBSET_1;
expansions TAYLOR_1;
theorems XBOOLE_1, ABSVALUE, PARTFUN1, XCMPLX_1, RELAT_1, RCOMP_1, SEQ_1,
SEQ_2, SIN_COS, SERIES_1, FUNCT_1, RFUNCT_2, NAT_1, NEWTON, POWER,
FDIFF_1, FDIFF_2, TAYLOR_1, SIN_COS2, XREAL_1, RFUNCT_1, ABIAN, COMPLEX1,
XXREAL_0, VALUED_1, FUNCT_2, XREAL_0, ORDINAL1;
schemes NAT_1;
begin
reserve Z for open Subset of REAL;
theorem Th1:
for x be Real, n be Nat holds |.x |^ n.| = |.x.| |^ n
proof
let x be Real, n be Nat;
defpred P[Nat] means |.x |^ $1.| = |.x.| |^ $1;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
|.x |^ (k+1).| = |.x * x |^ k.| by NEWTON:6
.= |.x.| * |.x |^ k.| by COMPLEX1:65
.= |.x.| |^ (k+1) by A2,NEWTON:6;
hence thesis;
end;
|.x |^ 0.| = |.1.| by NEWTON:4
.= 1 by ABSVALUE:def 1;
then
A3: P[0] by NEWTON:4;
for n be Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
definition
let f be PartFunc of REAL,REAL, Z be Subset of REAL, a be Real;
func Maclaurin(f,Z,a) -> Real_Sequence equals
Taylor(f,Z,0,a);
coherence;
end;
theorem Th2:
for n be Nat, f be PartFunc of REAL,REAL, r be Real st
0 < r & ].-r,r.[ c= dom f & f is_differentiable_on n+1,].-r,r.[
for x be Real st x in ].-r, r.[
ex s be Real st 0 < s & s < 1 & f.x = Partial_Sums(
Maclaurin(f,].-r,r.[,x)).n + (diff(f,].-r,r.[).(n+1)).(s*x) * x |^ (n+1) / ((n+
1)!)
proof
let n be Nat, f be PartFunc of REAL,REAL,
r be Real such that
A1: 0 < r & ].-r,r.[ c= dom f & f is_differentiable_on n+1, ].-r,r.[;
let x be Real;
assume x in ].-r, r.[;
then consider s be Real such that
A2: 0 < s & s < 1 & f.x=Partial_Sums(Taylor(f, ].0-r,0+r.[,0,x)).n + (
diff(f,].0-r,0+r.[).(n+1)).(0+s*(x-0)) * (x-0) |^ (n+1) / ((n+1)!) by A1,
TAYLOR_1:33;
take s;
thus thesis by A2;
end;
theorem
for n be Nat, f be PartFunc of REAL,REAL, x0,
r be Real st
0 < r & ].x0-r,x0+r.[ c= dom f & 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: 0 < r & ].x0-r,x0+r.[ c= dom f & f is_differentiable_on n+1, ].x0-r,
x0+r .[;
let x be Real;
assume x in ].x0-r,x0+r.[;
then 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)!) by A1,TAYLOR_1:33;
hence thesis;
end;
theorem Th4:
for n be Nat, f be PartFunc of REAL,REAL, r be Real st
0 < r & ].-r,r.[ c= dom f & f is_differentiable_on n+1, ].-r,r.[
for x be Real st x in ].-r, r.[
ex s be Real st 0 < s & s < 1 & |.f.x-Partial_Sums(
Maclaurin(f,].-r,r.[,x)).n.| = |. (diff(f,].-r,r.[).(n+1)).(s*x) * x |^ (n+1)
/ ((n+1)!).|
proof
let n be Nat;
let f be PartFunc of REAL,REAL;
let r be Real such that
A1: 0 < r & ].-r,r.[ c= dom f & f is_differentiable_on n+1, ].-r,r.[;
let x be Real;
assume x in ].-r,r.[;
then ex s be Real
st 0 < s & s < 1 & f.x=Partial_Sums( Maclaurin(f, ].-r,r.[,x
)).n + (diff(f,].-r,r.[).(n+1)).(s*x) * x |^ (n+1) / ((n +1)!) by A1,Th2;
hence thesis;
end;
Lm1: for f being Function of REAL, REAL holds dom (f | Z) = Z
proof
let f be Function of REAL, REAL;
A1: dom f = REAL by FUNCT_2:def 1;
thus dom (f|Z) = dom f /\ Z by RELAT_1:61
.= Z by A1,XBOOLE_1:28;
end;
theorem Th5:
exp_R `| Z = exp_R | Z & dom(exp_R | Z) = Z
proof
A1: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
A2: dom (exp_R | Z) = Z by Lm1;
A3: for x be Element of REAL st x in Z holds (exp_R `| Z).x=(exp_R | Z).x
proof
let x be Element of REAL such that
A4: x in Z;
thus (exp_R `| Z).x=diff(exp_R,x) by A1,A4,FDIFF_1:def 7
.=exp_R.x by TAYLOR_1:16
.=(exp_R | Z).x by A2,A4,FUNCT_1:47;
end;
dom (exp_R `| Z) = Z by A1,FDIFF_1:def 7;
hence thesis by A2,A3,PARTFUN1:5;
end;
theorem Th6:
for n be Nat holds diff(exp_R,Z).n=exp_R | Z
proof
let n be Nat;
defpred P[Nat] means diff(exp_R,Z).$1 = exp_R | Z;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
A3: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
diff(exp_R,Z).(k+1)=(diff(exp_R,Z).k) `| Z by TAYLOR_1:def 5
.=exp_R `| Z by A2,A3,FDIFF_2:16
.=exp_R | Z by Th5;
hence thesis;
end;
A4: P[0] by TAYLOR_1:def 5;
for n be Nat holds P[n] from NAT_1:sch 2(A4,A1);
hence thesis;
end;
theorem Th7:
for n be Nat, x be Real st x in Z holds (diff(exp_R,Z)
.n).x = exp_R.x
proof
let n be Nat;
let x be Real;
assume x in Z;
then
A1: x in dom(exp_R | Z) by Th5;
(diff(exp_R,Z).n).x=(exp_R | Z).x by Th6
.=exp_R.x by A1,FUNCT_1:47;
hence thesis;
end;
theorem
for n be Element of NAT, r,x be Real st 0 < r holds Maclaurin(exp_R,
].-r,r.[,x).n = x |^ n / (n!)
proof
let n be Element of NAT;
A1: |.0-0.|=0 by ABSVALUE:2;
let r,x be Real;
assume r > 0;
then 0 in ].0-r,0+r.[ by A1,RCOMP_1:1;
then
A2: 0 in dom(exp_R | ].-r,r.[) by Th5;
Maclaurin(exp_R, ].-r,r.[,x).n = (diff(exp_R,].-r,r.[).n).0 * (x-0) |^ n
/ (n!) by TAYLOR_1:def 7
.=(exp_R | ].-r,r.[).0 * x |^ n / (n!) by Th6
.=exp_R.0 * x |^ n / (n!) by A2,FUNCT_1:47
.=x |^ n / (n!) by SIN_COS2:13;
hence thesis;
end;
theorem
for n be Element of NAT, r,x,s be Real st x in ].-r,r.[ & 0 < s & s <
1 holds |.(diff(exp_R,].-r,r.[).(n+1)).(s*x) * x |^ (n+1) / ((n+1)!) .| <=
|.exp_R.(s*x).| * |.x.| |^ (n+1) / ((n+1)!)
proof
let n be Element of NAT;
let r,x,s be Real such that
A1: x in ].-r,r.[ and
A2: 0 < s and
A3: s < 1;
A4: |.s*x-0.| = |.s.| * |.x.| by COMPLEX1:65
.= s * |.x.| by A2,ABSVALUE:def 1;
x in ].0-r,0+r.[ by A1;
then
A5: |.x-0.| < r by RCOMP_1:1;
|.x.|>=0 by COMPLEX1:46;
then |.x.| * s < r * 1 by A2,A3,A5,XREAL_1:97;
then (s*x) in ].0-r,0+r.[ by A4,RCOMP_1:1;
then
A6: (s*x) in dom(exp_R | ].-r,r.[) by Th5;
A7: |.(n+1)!.| = ((n+1)!) by ABSVALUE:def 1;
|. (diff(exp_R,].-r,r.[).(n+1)).(s*x) * x |^ (n+1) /((n+1)!).| = |.
(exp_R | ].-r,r.[).(s*x) * x |^ (n+1) /((n+1)!).| by Th6
.= |.exp_R.(s*x) * x |^ (n+1) /((n+1)!).| by A6,FUNCT_1:47
.= |.exp_R.(s*x) * x |^ (n+1).| /|.(n+1)!.| by COMPLEX1:67
.= |.exp_R.(s*x).| * |.x |^ (n+1).| /((n+1)!) by A7,COMPLEX1:65;
hence thesis by Th1;
end;
theorem Th10:
for n be Element of NAT holds exp_R is_differentiable_on n, Z
proof
let n be Element of NAT;
let i be Nat such that
i <= n-1;
reconsider i as Element of NAT by ORDINAL1:def 12;
A1: for x be Real
st x in Z holds diff(exp_R,Z).i | Z is_differentiable_in x
proof
A2: diff(exp_R,Z).i | Z = exp_R | Z | Z by Th6
.= exp_R | Z by FUNCT_1:51;
A3: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
let x be Real;
assume x in Z;
hence thesis by A2,A3,FDIFF_1:def 6;
end;
dom(diff(exp_R,Z).i) = dom(exp_R | Z) by Th6
.= Z by Th5;
hence thesis by A1,FDIFF_1:def 6;
end;
theorem Th11:
for r be Real st 0 < r
ex M,L be Real st 0 <= M & 0 <= L & for n be Nat
for x,s be Real st x in ].-r,r.[ & 0 < s & s < 1 holds
|.(diff(exp_R,].-r,r.[).n).(s*x) * x |^ n /(n!).| <= M * L |^ n / (n!)
proof
let r be Real such that
A1: r > 0;
take M = exp_R.r;
take L = r;
now
let n be Nat;
now
A2: for a,b be Real st 0 <=a & a<=b
for n be Nat holds 0<= a
|^ n & a |^ n <= b |^ n
proof
let a,b be Real such that
A3: 0 <= a and
A4: a <= b;
defpred P[Nat] means 0 <= a |^ $1 & a |^ $1 <= b |^ $1;
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A6: P[k];
0*a <= a |^ k*a by A3,A6;
hence a |^ (k+1) >= 0 by NEWTON:6;
b |^ (k+1) = b |^ k*b & a |^ k*a <= b |^ k*b by A3,A4,A6,NEWTON:6
,XREAL_1:66;
hence thesis by NEWTON:6;
end;
b |^ 0 = 1 by NEWTON:4;
then
A7: P[0] by NEWTON:4;
for n be Nat holds P[n] from NAT_1:sch 2(A7,A5);
hence thesis;
end;
let x,s be Real such that
A8: x in ].-r,r.[ and
A9: 0 < s and
A10: s < 1;
x in ].0-r,0+r.[ by A8;
then
A11: |.x-0.| < r by RCOMP_1:1;
|.x.| >= 0 by COMPLEX1:46;
then
A12: |.x.| |^ n <= L |^ n by A11,A2;
|.x.| >= 0 by COMPLEX1:46;
then s * |.x.| < 1 * r by A9,A10,A11,XREAL_1:97;
then |.s.| * |.x.| < r by A9,ABSVALUE:def 1;
then |.s*x - 0.| < r by COMPLEX1:65;
then
A13: (s*x) in ].0-r,0+r.[ by RCOMP_1:1;
then
A14: |.(diff(exp_R,].-r,r.[).n).(s*x) * x |^ n / (n!).| =|.exp_R.(s*x
)* x |^ n / (n!).| by Th7
.=|.exp_R.(s*x)* (x |^ n / (n!)).| by XCMPLX_1:74
.=|.exp_R.(s*x).|*|.x |^ n / (n!).| by COMPLEX1:65;
exp_R.(s*x) >= 0 by SIN_COS:54;
then
A15: r in [#](REAL) /\ dom exp_R & |.exp_R.(s*x).| = exp_R.(s*x) by
ABSVALUE:def 1,TAYLOR_1:16, XREAL_0:def 1;
for x0 be Real holds 0 <= diff(exp_R,x0) by TAYLOR_1:16;
then
A16: exp_R|[#](REAL) is non-decreasing by FDIFF_2:39,TAYLOR_1:16;
|.x |^ n /(n!).| =|.x |^ n.| / |.n!.| by COMPLEX1:67
.=|.x |^ n.| / (n!) by ABSVALUE:def 1
.=|.x.| |^ n /(n!) by Th1;
then
A17: |.x |^ n /(n!).| <=L |^ n / (n!) by A12,XREAL_1:72;
A18: |.exp_R.(s*x).| >= 0 & |.x |^ n /(n!).| >= 0 by COMPLEX1:46;
(s*x) in {p where p is Real : -r<p & p<r} by A13,RCOMP_1:def 2;
then consider g be Real such that
A19: g= s*x & -r<g & g<r;
reconsider g as Element of REAL by XREAL_0:def 1;
g= s*x & -r<g & g<r by A19;
then |.exp_R.(s*x).| <= M by A16,A15,RFUNCT_2:24,TAYLOR_1:16;
then |.(diff(exp_R,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= M*(L |^ n /
(n!)) by A18,A17,A14,XREAL_1:66;
hence
|.(diff(exp_R,].-r,r.[).n).(s*x) * x |^ n /(n!).| <= M*L |^ n / (n
!) by XCMPLX_1:74;
end;
hence for x,s being Real
st x in ].-r,r.[ & 0 < s & s < 1 holds |.(diff(
exp_R,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= M*L |^ n / (n!);
end;
hence thesis by A1,SIN_COS:54;
end;
theorem Th12:
for M,L be Real st M >= 0 & L >= 0
for e be Real st e > 0
ex n be Nat st for m be Nat st n <= m holds (M*L |^ m / (m!)) < e
proof
let M,L be Real such that
A1: M >=0 and
A2: L >= 0;
A3: L rExpSeq is summable by SIN_COS:45;
then
A4: M(#)(L rExpSeq) is convergent by SEQ_2:7,SERIES_1:4;
lim (L rExpSeq)=0 by A3,SERIES_1:4;
then
A5: lim (M(#)(L rExpSeq))=M*0 by A3,SEQ_2:8,SERIES_1:4;
let p be Real;
assume p > 0;
then consider n be Nat such that
A6: for m be Nat st n<=m holds |.(M(#)(L rExpSeq)).m - 0.|
< p by A4,A5,SEQ_2:def 7;
take n;
A7: for n be Element of NAT holds M*(L |^ n /(n!))=(M(#)(L rExpSeq)).n
proof
let n be Element of NAT;
M*(L |^ n /(n!)) = M*((L rExpSeq).n) by SIN_COS:def 5
.= (M(#)(L rExpSeq)).n by SEQ_1:9;
hence thesis;
end;
now
let m be Nat such that
A8: n <= m;
A9: m in NAT by ORDINAL1:def 12;
A10: L |^ m >= 0 & m! > 0 by A2,POWER:3;
|.(M(#)(L rExpSeq)).m - 0.| = |.M*(L |^ m /(m!)).| by A7,A9
.=|.M.|*|.L |^ m /(m!).| by COMPLEX1:65
.=M*|.L |^ m /(m!).| by A1,ABSVALUE:def 1
.=M*(L |^ m /(m!)) by A10,ABSVALUE:def 1
.=M*L |^ m /(m!) by XCMPLX_1:74;
hence (M*L |^ m /(m!)) < p by A6,A8;
end;
hence thesis;
end;
theorem Th13:
for r, e be Real st 0 < r & 0 < e
ex n be Nat st for m be Nat st n <= m
for x,s be Real st x in ].-r,r.[ & 0
< s & s < 1 holds |.(diff(exp_R,].-r,r.[).m).(s*x) * x |^ m / (m!).|< e
proof
let r, e be Real such that
A1: 0 < r and
A2: 0 < e;
consider M, L be Real such that
A3: M >= 0 & L >= 0 and
A4: for n be Nat holds
for x,s be Real st x in ].-r,r.[ & 0 <
s & s < 1 holds |.(diff(exp_R,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= M*L |^ n
/ (n!) by A1,Th11;
consider n be Nat such that
A5: for m be Nat st n <= m holds (M*L |^ m / (m!)) < e by A2,A3,Th12;
take n;
let m be Nat;
assume n <= m;
then
A6: (M*L |^ m / (m!)) < e by A5;
let x,s be Real;
assume x in ].-r,r.[ & 0 < s & s < 1;
then
|.(diff(exp_R,].-r,r.[).m).(s*x) * x |^ m /(m!).| <= M*L |^ m /(m!) by A4;
hence thesis by A6,XXREAL_0:2;
end;
theorem
for r, e be Real st 0 < r & 0 < e
ex n be Nat st for
m be Nat st n <= m holds for x being Real st x in ].-r,r.[
holds |.exp_R.x-Partial_Sums(Maclaurin(exp_R,].-r,r.[,x)).m.| < e
proof
let r, e be Real such that
A1: r > 0 and
A2: e > 0;
consider n be Nat such that
A3: for m be Nat st n <= m
for x,s be Real st x in ].-r
,r.[ & 0 < s & s < 1 holds |. (diff(exp_R,].-r,r.[).m).(s*x) * x |^ m / (m!)
.|< e by A1,A2,Th13;
take n;
let m be Nat such that
A4: n <= m;
now
m <= m+1 by NAT_1:11;
then
A5: n <= m+1 by A4,XXREAL_0:2;
let x be Real such that
A6: x in ].-r,r.[;
ex s be Real
st 0 < s & s < 1 & |.exp_R.x-Partial_Sums (Maclaurin(
exp_R,].-r,r.[,x)).m.| =|. (diff(exp_R,].-r,r.[).(m+1)).(s*x) * x |^ (m+1) / (
(m+1)!).| by A1,A6,Th4,Th10,SIN_COS:47;
hence
|.exp_R.x-Partial_Sums(Maclaurin(exp_R,].-r,r.[,x)).m.| < e by A3,A6,A5;
end;
hence thesis;
end;
theorem Th15:
for x be Real holds x rExpSeq is absolutely_summable
proof
let x be Real;
for n be Nat holds |.x rExpSeq.n.| = (|.x.| rExpSeq).n
proof
let n be Nat;
|.x rExpSeq.n.| = |.x |^ n / (n!).| by SIN_COS:def 5
.= |.x |^ n.| / |.n!.| by COMPLEX1:67
.= |.x |^ n.| / (n!) by ABSVALUE:def 1
.= |.x.| |^ n / (n!) by Th1
.= (|.x.| rExpSeq).n by SIN_COS:def 5;
hence thesis;
end;
then |.x.| rExpSeq = |.x rExpSeq.| by SEQ_1:12;
then |.x rExpSeq.| is summable by SIN_COS:45;
hence thesis by SERIES_1:def 4;
end;
theorem
for r, x be Real st 0 < r holds Maclaurin(exp_R,].-r,r.[,x) = (x
rExpSeq) & Maclaurin(exp_R,].-r,r.[,x) is absolutely_summable & exp_R.x=Sum(
Maclaurin(exp_R,].-r,r.[,x))
proof
A1: |.0-0.|=0 by ABSVALUE:2;
let r, x be Real;
assume r > 0;
then 0 in ].0-r,0+r.[ by A1,RCOMP_1:1;
then
A2: 0 in dom(exp_R | ].-r,r.[) by Th5;
now
let t be object;
assume t in NAT;
then reconsider n=t as Element of NAT;
thus Maclaurin(exp_R,].-r,r.[,x).t = (diff(exp_R,].-r,r.[).n).0 * (x-0) |^
n / (n!) by TAYLOR_1:def 7
.= (exp_R | ].-r,r.[).0 * x |^ n / (n!) by Th6
.= exp_R.0 * x |^ n / (n!) by A2,FUNCT_1:47
.= (x rExpSeq).t by SIN_COS:def 5,SIN_COS2:13;
end;
then Maclaurin(exp_R,].-r,r.[,x) = (x rExpSeq) by FUNCT_2:12;
hence thesis by Th15,SIN_COS:def 22;
end;
theorem Th17:
sin `| Z = cos | Z & cos `| Z = (-sin) | Z & dom(sin | Z) = Z &
dom(cos | Z) = Z
proof
A1: dom (sin | Z) = dom(sin) /\ Z by RELAT_1:61
.= Z by SIN_COS:24,XBOOLE_1:28;
A2: dom (cos | Z) = dom(cos) /\ Z by RELAT_1:61
.= Z by SIN_COS:24,XBOOLE_1:28;
A3: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
A4: for x be Element of REAL st x in Z holds (sin `| Z).x = (cos | Z).x
proof
let x be Element of REAL such that
A5: x in Z;
(sin `| Z).x=diff(sin,x) by A3,A5,FDIFF_1:def 7
.=cos.x by SIN_COS:64
.=(cos | Z).x by A2,A5,FUNCT_1:47;
hence thesis;
end;
A6: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
then
A7: dom (cos `| Z) = Z by FDIFF_1:def 7;
A8: dom ((-sin) | Z) = dom((-1)(#)sin) /\ Z by RELAT_1:61
.= dom(sin) /\ Z by VALUED_1:def 5
.= Z by SIN_COS:24,XBOOLE_1:28;
A9: for x be Element of REAL st x in Z holds (cos `| Z).x = ((-sin) | Z).x
proof
let x be Element of REAL such that
A10: x in Z;
x in dom (sin) by SIN_COS:24;
then
A11: x in dom ((-1)(#)sin) by VALUED_1:def 5;
(cos `| Z).x=diff(cos,x) by A6,A10,FDIFF_1:def 7
.=-sin.x by SIN_COS:63
.=(-1)*sin.x
.=(-sin).x by A11,VALUED_1:def 5
.=((-sin) | Z).x by A8,A10,FUNCT_1:47;
hence thesis;
end;
dom (sin `| Z) = Z by A3,FDIFF_1:def 7;
hence thesis by A8,A1,A2,A4,A7,A9,PARTFUN1:5;
end;
theorem
for f be PartFunc of REAL,REAL, Z be Subset of REAL st f
is_differentiable_on Z holds (-f) `| Z = -f `| Z
proof
let f be PartFunc of REAL,REAL, Z be Subset of REAL such that
A1: f is_differentiable_on Z;
Z is open Subset of REAL by A1,FDIFF_1:10;
then (-f) `| Z = (-1)(#) (f `| Z) by A1,FDIFF_2:19
.= -f `| Z;
hence thesis;
end;
theorem Th19:
for n be Nat holds diff(sin,Z).(2*n) = (-1) |^ n (#)
sin | Z & diff(sin,Z).(2*n+1) = (-1) |^ n (#) cos | Z & diff(cos,Z).(2*n) = (-1
) |^ n (#)cos | Z & diff(cos,Z).(2*n+1) = (-1) |^ (n+1) (#)sin | Z
proof
let n be Nat;
A1: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
defpred P[Nat] means diff(sin,Z).(2*$1) = (-1) |^ $1 (#) sin | Z
& diff(sin,Z).(2*$1+1) = (-1) |^ $1 (#) cos | Z & diff(cos,Z).(2*$1) = (-1) |^
$1 (#) cos | Z & diff(cos,Z).(2*$1+1) = (-1) |^ ($1+1) (#) sin | Z;
A2: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A4: P[k];
A5: (cos | Z) is_differentiable_on Z by A1,FDIFF_2:16;
A6: diff(sin,Z).(2*(k+1)) = diff(sin,Z).((2*k+1)+1)
.= diff(sin,Z).(2*k+1) `| Z by TAYLOR_1:def 5
.= ((-1) |^ k) (#) ((cos | Z) `| Z) by A4,A5,FDIFF_2:19
.= ((-1) |^ k) (#) (cos `| Z) by A1,FDIFF_2:16
.= ((-1) |^ k) (#) (((-1) (#) sin) | Z) by Th17
.= ((-1) |^ k) (#) ((-1) (#) sin | Z) by RFUNCT_1:49
.= (((-1) |^ k) * (-1)) (#) (sin | Z) by RFUNCT_1:17
.= (-1) |^ (k+1) (#) sin | Z by NEWTON:6;
A7: (sin | Z) is_differentiable_on Z by A2,FDIFF_2:16;
A8: diff(cos,Z).(2*(k+1)) = diff(cos,Z).((2*k+1)+1)
.= diff(cos,Z).(2*k+1) `| Z by TAYLOR_1:def 5
.= ((-1) |^ (k+1)) (#) ((sin | Z) `| Z) by A4,A7,FDIFF_2:19
.= (-1) |^ (k+1) (#) (sin `| Z) by A2,FDIFF_2:16
.= (-1) |^ (k+1) (#) cos | Z by Th17;
A9: diff(cos,Z).(2*(k+1)+1) = diff(cos,Z).(2*(k+1)) `| Z by TAYLOR_1:def 5
.= ((-1) |^ (k+1)) (#) ((cos | Z) `| Z) by A5,A8,FDIFF_2:19
.= ((-1) |^ (k+1)) (#) (cos `| Z) by A1,FDIFF_2:16
.= ((-1) |^ (k+1)) (#) ((-1) (#) sin) | Z by Th17
.= ((-1) |^ (k+1)) (#) ((-1) (#) sin | Z) by RFUNCT_1:49
.= (((-1) |^ (k+1)) * (-1)) (#) sin | Z by RFUNCT_1:17
.= (-1) |^ ((k+1)+1) (#) sin | Z by NEWTON:6;
diff(sin,Z).(2*(k+1)+1) = diff(sin,Z).(2*(k+1)) `| Z by TAYLOR_1:def 5
.= ((-1) |^ (k+1)) (#) ((sin | Z) `| Z) by A7,A6,FDIFF_2:19
.= ((-1) |^ (k+1)) (#) (sin `| Z) by A2,FDIFF_2:16
.= (-1) |^ (k+1) (#) cos | Z by Th17;
hence thesis by A6,A8,A9;
end;
A10: diff(cos,Z).(2*0+1) = diff(cos,Z).0 `| Z by TAYLOR_1:def 5
.= cos | Z `| Z by TAYLOR_1:def 5
.= cos `| Z by A1,FDIFF_2:16
.= (-sin) | Z by Th17
.= 1 (#) (-sin) | Z by RFUNCT_1:21
.= ((-1) |^ 0) (#) ((-1) (#) sin) | Z by NEWTON:4
.= ((-1) |^ 0) (#) ((-1) (#) sin | Z) by RFUNCT_1:49
.= (((-1) |^ 0) * (-1)) (#) sin | Z by RFUNCT_1:17
.= (-1) |^ (0+1) (#) sin | Z by NEWTON:6;
A11: diff(sin,Z).(2*0) = sin | Z by TAYLOR_1:def 5
.= 1 (#) (sin | Z) by RFUNCT_1:21
.= (-1) |^ 0 (#) (sin | Z) by NEWTON:4;
A12: diff(cos,Z).(2*0) = cos | Z by TAYLOR_1:def 5
.= 1 (#) (cos | Z) by RFUNCT_1:21
.= (-1) |^ 0 (#) (cos | Z) by NEWTON:4;
diff(sin,Z).(2*0+1) = diff(sin,Z).0 `| Z by TAYLOR_1:def 5
.= sin | Z `| Z by TAYLOR_1:def 5
.= sin `| Z by A2,FDIFF_2:16
.= cos | Z by Th17
.= 1 (#) (cos | Z) by RFUNCT_1:21
.= (-1) |^ 0 (#) (cos | Z) by NEWTON:4;
then
A13: P[0] by A11,A12,A10;
for n be Nat holds P[n] from NAT_1:sch 2(A13,A3);
hence thesis;
end;
theorem Th20:
for n be Nat, r,x be Real st r > 0 holds Maclaurin(
sin, ].-r,r.[,x).(2*n) = 0 & Maclaurin(sin, ].-r,r.[,x).(2*n+1) = (-1) |^ n * x
|^ (2*n+1) / ((2*n+1)!) & Maclaurin(cos, ].-r,r.[,x).(2*n) = (-1) |^ n * x |^ (
2*n) / ((2*n)!) & Maclaurin(cos, ].-r,r.[,x).(2*n+1) = 0
proof
A1: |.0-0.|=0 by ABSVALUE:2;
let n be Nat, r,x be Real;
assume r > 0;
then
A2: 0 in ].0-r,0+r.[ by A1,RCOMP_1:1;
then
A3: 0 in dom(cos | ].-r,r.[) by Th17;
A4: dom(((-1) |^ n) (#) (cos | ].-r,r.[)) = dom(cos | ].-r,r.[) by
VALUED_1:def 5
.= ].-r,r.[ by Th17;
A5: Maclaurin(sin, ].-r,r.[,x).(2*n+1) = (diff(sin,].-r,r.[).(2*n+1)).0 * (
x-0) |^ (2*n+1) / ((2*n+1)!) by TAYLOR_1:def 7
.= ((-1) |^ n (#) cos | ].-r,r.[).0 * x |^ (2*n+1) / ((2*n+1)!) by Th19
.= (((-1) |^ n) * (cos | ].-r,r.[).0) * x |^ (2*n+1) / ((2*n+1)!) by A2,A4,
VALUED_1:def 5
.= ((-1) |^ n) * cos.0 * x |^ (2*n+1) / ((2*n+1)!) by A3,FUNCT_1:47
.= (-1) |^ n * x |^ (2*n+1) / ((2*n+1)!) by SIN_COS:30;
A6: dom(((-1) |^ n) (#) (sin | ].-r,r.[)) = dom(sin | ].-r,r.[) by
VALUED_1:def 5
.= ].-r,r.[ by Th17;
A7: 0 in dom(sin | ].-r,r.[) by A2,Th17;
A8: Maclaurin(cos, ].-r,r.[,x).(2*n) = (diff(cos,].-r,r.[).(2*n)).0 * (x-0)
|^ (2*n) / ((2*n)!) by TAYLOR_1:def 7
.= ((-1) |^ n (#) cos | ].-r,r.[).0 * x |^ (2*n) / ((2*n)!) by Th19
.= (((-1) |^ n) * (cos | ].-r,r.[).0) * x |^ (2*n) / ((2*n)!) by A2,A4,
VALUED_1:def 5
.= ((-1) |^ n) * cos.0 * x |^ (2*n) / ((2*n)!) by A3,FUNCT_1:47
.= (-1) |^ n * x |^ (2*n) / ((2*n)!) by SIN_COS:30;
A9: dom(((-1) |^ (n+1)) (#) (sin | ].-r,r.[)) = dom(sin | ].-r,r.[) by
VALUED_1:def 5
.= ].-r,r.[ by Th17;
A10: Maclaurin(cos, ].-r,r.[,x).(2*n+1) = (diff(cos,].-r,r.[).(2*n+1)).0 * (
x-0) |^ (2*n+1) / ((2*n+1)!) by TAYLOR_1:def 7
.= ((-1) |^ (n+1) (#) sin | ].-r,r.[).0 * x |^ (2*n+1) / ((2*n+1)!) by Th19
.= (((-1) |^ (n+1)) * (sin | ].-r,r.[).0) * x |^ (2*n+1) / ((2*n+1)!) by A2
,A9,VALUED_1:def 5
.= ((-1) |^ (n+1)) * sin.0 * x |^ (2*n+1) / ((2*n+1)!) by A7,FUNCT_1:47
.= 0 by SIN_COS:30;
Maclaurin(sin, ].-r,r.[,x).(2*n) = (diff(sin,].-r,r.[).(2*n)).0 * (x-0)
|^ (2*n) / ((2*n)!) by TAYLOR_1:def 7
.= ((-1) |^ n (#) sin | ].-r,r.[).0 * x |^ (2*n) / ((2*n)!) by Th19
.= (((-1) |^ n) * (sin | ].-r,r.[).0) * x |^ (2*n) / ((2*n)!) by A2,A6,
VALUED_1:def 5
.= ((-1) |^ n) * sin.0 * x |^ (2*n) / ((2*n)!) by A7,FUNCT_1:47
.= 0 by SIN_COS:30;
hence thesis by A5,A8,A10;
end;
theorem Th21:
for n be Element of NAT holds sin is_differentiable_on n, Z &
cos is_differentiable_on n, Z
proof
let n be Element of NAT;
now
let i be Nat such that
i <= n-1;
A1: now
per cases;
suppose
i is even;
then consider j be Nat such that
A2: i=2*j by ABIAN:def 2;
thus dom(diff(sin,Z).i) = dom((-1) |^ j (#) sin | Z) by A2,Th19
.= dom((sin | Z)) by VALUED_1:def 5
.= Z by Th17;
end;
suppose
i is odd;
then consider j be Nat such that
A3: i=2*j+1 by ABIAN:9;
thus dom(diff(sin,Z).i) = dom((-1) |^ j (#) cos | Z) by A3,Th19
.= dom((cos | Z)) by VALUED_1:def 5
.= Z by Th17;
end;
end;
for x be Real st x in Z
holds diff(sin,Z).i | Z is_differentiable_in x
proof
let x be Real such that
A4: x in Z;
now
per cases;
suppose
i is even;
then consider j be Nat such that
A5: i = 2*j by ABIAN:def 2;
sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
then
A6: (sin | Z) is_differentiable_in x by A4,FDIFF_1:def 6;
diff(sin,Z).i = (-1) |^ j (#) sin | Z by A5,Th19;
hence diff(sin,Z).i is_differentiable_in x by A6,FDIFF_1:15;
end;
suppose
i is odd;
then consider j be Nat such that
A7: i = 2*j+1 by ABIAN:9;
cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
then
A8: (cos | Z) is_differentiable_in x by A4,FDIFF_1:def 6;
diff(sin,Z).i = (-1) |^ j (#) cos | Z by A7,Th19;
hence diff(sin,Z).i is_differentiable_in x by A8,FDIFF_1:15;
end;
end;
hence thesis by A1,RELAT_1:68;
end;
hence diff(sin,Z).i is_differentiable_on Z by A1,FDIFF_1:def 6;
end;
hence sin is_differentiable_on n, Z;
now
let i be Nat such that
i <= n-1;
A9: now
per cases;
suppose
i is even;
then consider j be Nat such that
A10: i = 2*j by ABIAN:def 2;
thus dom(diff(cos,Z).i) = dom((-1) |^ j (#) cos | Z) by A10,Th19
.= dom((cos | Z)) by VALUED_1:def 5
.= Z by Th17;
end;
suppose
i is odd;
then consider j be Nat such that
A11: i = 2*j+1 by ABIAN:9;
thus dom(diff(cos,Z).i) = dom((-1) |^ (j+1) (#) sin | Z) by A11,Th19
.= dom((sin | Z)) by VALUED_1:def 5
.= Z by Th17;
end;
end;
for x be Real
st x in Z holds diff(cos,Z).i | Z is_differentiable_in x
proof
let x be Real such that
A12: x in Z;
now
per cases;
suppose
i is even;
then consider j be Nat such that
A13: i = 2*j by ABIAN:def 2;
cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
then
A14: (cos | Z) is_differentiable_in x by A12,FDIFF_1:def 6;
diff(cos,Z).i = (-1) |^ j (#) cos | Z by A13,Th19;
hence diff(cos,Z).i is_differentiable_in x by A14,FDIFF_1:15;
end;
suppose
i is odd;
then consider j be Nat such that
A15: i = 2*j+1 by ABIAN:9;
sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
then
A16: (sin | Z) is_differentiable_in x by A12,FDIFF_1:def 6;
diff(cos,Z).i = (-1) |^ (j+1) (#) sin | Z by A15,Th19;
hence diff(cos,Z).i is_differentiable_in x by A16,FDIFF_1:15;
end;
end;
hence thesis by A9,RELAT_1:68;
end;
hence diff(cos,Z).i is_differentiable_on Z by A9,FDIFF_1:def 6;
end;
hence thesis;
end;
theorem Th22:
for r be Real st r > 0
ex r1,r2 be Real st r1 >= 0 & r2 >= 0 &
for n be Nat
for x,s be Real st x in ].-r,r.[ & 0 < s & s < 1
holds |.(diff(sin,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1 * r2 |^ n / (n!)
& |.(diff(cos,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1 * r2 |^ n / (n!)
proof
let r be Real such that
A1: r > 0;
take r1 = 1;
take r2 = r;
thus r1 >= 0 & r2 >= 0 by A1;
let n be Nat;
let x,s be Real such that
A2: x in ].-r,r.[ and
A3: s > 0 and
A4: s < 1;
x in ].0-r,0+r.[ by A2;
then
A5: |.x-0.| < r by RCOMP_1:1;
A6: |.x.| |^ n / (n!) <= r2 |^ n / (n!)
proof
defpred P[Nat] means |.x.| |^ $1 / ($1!) <= r2 |^ $1 / ($1!);
A7: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A8: P[k];
A9: |.x.| |^ (k+1) / ((k+1)!) = |.x.| |^ k * |.x.| / ((k+1)!) by
NEWTON:6
.= |.x.| |^ k * |.x.| / (k! * (k+1)) by NEWTON:15
.= |.x.| |^ k * (|.x.| / (k! * (k+1))) by XCMPLX_1:74
.= |.x.| |^ k * (|.x.| / (k!) / (k+1)) by XCMPLX_1:78
.= |.x.| |^ k * (1 / ((k!) / |.x.|) / (k+1)) by XCMPLX_1:57
.= |.x.| |^ k * (1 / (k!) * |.x.| / (k+1)) by XCMPLX_1:82
.= (|.x.| |^ k * (1 / (k!) * |.x.|)) / (k+1) by XCMPLX_1:74
.= (|.x.| |^ k * (1 / (k!))) * |.x.| / (k+1)
.= (|.x.| |^ k * 1) / (k!) * |.x.| / (k+1) by XCMPLX_1:74
.= |.x.| |^ k / (k!) * |.x.| / (k+1);
|.x.| |^ k / (k!) = |.x |^ k.| / (k!) by Th1
.= |.x |^ k.| / |.k!.| by ABSVALUE:def 1
.= |.x |^ k / (k!).| by COMPLEX1:67;
then
A10: |.x.| |^ k / (k!) >= 0 by COMPLEX1:46;
A11: r2 |^ (k+1) / ((k+1)!) = r2 |^ k * r2 / ((k+1)!) by NEWTON:6
.= r2 |^ k * r2 / (k! * (k+1)) by NEWTON:15
.= r2 |^ k * (r2 / (k! * (k+1))) by XCMPLX_1:74
.= r2 |^ k * (r2 / (k!) / (k+1)) by XCMPLX_1:78
.= r2 |^ k * (1 / ((k!) / r2) / (k+1)) by XCMPLX_1:57
.= r2 |^ k * (1 / (k!) * r2 / (k+1)) by XCMPLX_1:82
.= (r2 |^ k * (1 / (k!) * r2)) / (k+1) by XCMPLX_1:74
.= (r2 |^ k * (1 / (k!))) * r2 / (k+1)
.= (r2 |^ k * 1) / (k!) * r2 / (k+1) by XCMPLX_1:74
.= r2 |^ k / (k!) * r2 / (k+1);
|.x.| >= 0 by COMPLEX1:46;
then
|.x.| |^ k / (k!) * |.x.| <= r2 |^ k / (k!) * r2 by A5,A8,A10,
XREAL_1:66;
hence thesis by A9,A11,XREAL_1:72;
end;
|.x.| |^ 0 / (0!) = 1 / (0!) by NEWTON:4
.= r2 |^ 0 / (0!) by NEWTON:4;
then
A12: P[0];
for i be Nat holds P[i] from NAT_1:sch 2(A12,A7);
hence thesis;
end;
|.x.| >= 0 by COMPLEX1:46;
then s * |.x.| < 1 * r by A3,A4,A5,XREAL_1:97;
then |.s.| * |.x.| < r by A3,ABSVALUE:def 1;
then |.s*x - 0.| < r by COMPLEX1:65;
then
A13: (s*x) in ].0-r,0+r.[ by RCOMP_1:1;
A14: for k be Nat holds |.(-1) |^ k.| = 1
proof
let k be Nat;
per cases;
suppose
k is even;
then consider j be Nat such that
A15: k = 2*j by ABIAN:def 2;
thus |.(-1) |^ k.| = |.((-1) |^ (1+1)) |^ j.| by A15,NEWTON:9
.= |.((-1) |^ 1 * (-1)) |^ j.| by NEWTON:6
.= |.((-1) * (-1)) |^ j.|
.= |.1.|
.= 1 by ABSVALUE:def 1;
end;
suppose
k is odd;
then consider j be Nat such that
A16: k = 2*j+1 by ABIAN:9;
thus |.(-1) |^ k.| = |.(-1) |^ (2*j) * (-1).| by A16,NEWTON:6
.= |.((-1) |^ (1+1)) |^ j * (-1).| by NEWTON:9
.= |.((-1) |^ 1 * (-1)) |^ j * (-1).| by NEWTON:6
.= |.((-1) * (-1)) |^ j * (-1).|
.= |.1 * (-1).|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1;
end;
end;
A17: |.(diff(sin,].-r,r.[).n).(s*x).| <= r1
proof
per cases;
suppose
n is even;
then consider k be Nat such that
A18: n = 2*k by ABIAN:def 2;
A19: dom(((-1) |^ k) (#) (sin | ].-r,r.[)) = dom(sin | ].-r,r.[) by
VALUED_1:def 5
.= ].-r,r.[ by Th17;
A20: (s*x) in dom(sin | ].-r,r.[) by A13,Th17;
A21: |.sin (s*x).| <= 1 by SIN_COS:27;
|.(diff(sin,].-r,r.[).n).(s*x).| = |.((-1) |^ k (#) sin | ].-r
,r.[).(s*x).| by A18,Th19
.= |.((-1) |^ k) * ((sin | ].-r,r.[).(s*x)).| by A13,A19,
VALUED_1:def 5
.= |.(-1) |^ k.| * |.(sin | ].-r,r.[).(s*x).| by COMPLEX1:65
.= 1 * |.(sin | ].-r,r.[).(s*x).| by A14
.= |.sin.(s*x).| by A20,FUNCT_1:47;
hence thesis by A21,SIN_COS:def 17;
end;
suppose
n is odd;
then consider k be Nat such that
A22: n = 2*k+1 by ABIAN:9;
A23: dom(((-1) |^ k) (#) (cos | ].-r,r.[)) = dom(cos | ].-r,r.[) by
VALUED_1:def 5
.= ].-r,r.[ by Th17;
A24: (s*x) in dom(cos | ].-r,r.[) by A13,Th17;
A25: |.cos (s*x).| <= 1 by SIN_COS:27;
|.(diff(sin,].-r,r.[).n).(s*x).| = |.((-1) |^ k (#) cos | ].-r
,r.[).(s*x).| by A22,Th19
.= |.((-1) |^ k) * ((cos | ].-r,r.[).(s*x)).| by A13,A23,
VALUED_1:def 5
.= |.(-1) |^ k.| * |.(cos | ].-r,r.[).(s*x).| by COMPLEX1:65
.= 1 * |.(cos | ].-r,r.[).(s*x).| by A14
.= |.cos.(s*x).| by A24,FUNCT_1:47;
hence thesis by A25,SIN_COS:def 19;
end;
end;
A26: |.(diff(cos,].-r,r.[).n).(s*x).| <= r1
proof
per cases;
suppose
n is even;
then consider k be Nat such that
A27: n = 2*k by ABIAN:def 2;
A28: dom(((-1) |^ k) (#) (cos | ].-r,r.[)) = dom(cos | ].-r,r.[) by
VALUED_1:def 5
.= ].-r,r.[ by Th17;
A29: (s*x) in dom(cos | ].-r,r.[) by A13,Th17;
A30: |.cos (s*x).| <= 1 by SIN_COS:27;
|.(diff(cos,].-r,r.[).n).(s*x).| = |.((-1) |^ k (#) cos | ].-r
,r.[).(s*x).| by A27,Th19
.= |.((-1) |^ k) * ((cos | ].-r,r.[).(s*x)).| by A13,A28,
VALUED_1:def 5
.= |.(-1) |^ k.| * |.(cos | ].-r,r.[).(s*x).| by COMPLEX1:65
.= 1 * |.(cos | ].-r,r.[).(s*x).| by A14
.= |.cos.(s*x).| by A29,FUNCT_1:47;
hence thesis by A30,SIN_COS:def 19;
end;
suppose
n is odd;
then consider k be Nat such that
A31: n = 2*k+1 by ABIAN:9;
A32: dom(((-1) |^ (k+1)) (#) (sin | ].-r,r.[)) = dom(sin | ].-r,r.[)
by VALUED_1:def 5
.= ].-r,r.[ by Th17;
A33: (s*x) in dom(sin | ].-r,r.[) by A13,Th17;
A34: |.sin (s*x).| <= 1 by SIN_COS:27;
|.(diff(cos,].-r,r.[).n).(s*x).| = |.((-1) |^ (k+1) (#) sin |
].-r,r.[).(s*x).| by A31,Th19
.= |.((-1) |^ (k+1)) * ((sin | ].-r,r.[).(s*x)).| by A13,A32,
VALUED_1:def 5
.= |.(-1) |^ (k+1).| * |.(sin | ].-r,r.[).(s*x).| by COMPLEX1:65
.= 1 * |.(sin | ].-r,r.[).(s*x).| by A14
.= |.sin.(s*x).| by A33,FUNCT_1:47;
hence thesis by A34,SIN_COS:def 17;
end;
end;
A35: |.x |^ n / (n!).| = |.x |^ n.| / |.n!.| by COMPLEX1:67
.= |.x |^ n.| / (n!) by ABSVALUE:def 1
.= |.x.| |^ n / (n!) by Th1;
then
A36: |.x.| |^ n / (n!) >= 0 by COMPLEX1:46;
A37: |.(diff(cos,].-r,r.[).n).(s*x) * x |^ n / (n!).| = |.(diff(cos,].-
r,r.[).n).(s*x) * (x |^ n / (n!)).| by XCMPLX_1:74
.= |.(diff(cos,].-r,r.[).n).(s*x).| * |.x |^ n / (n!).| by COMPLEX1:65
.= |.(diff(cos,].-r,r.[).n).(s*x).| * |.x.| |^ n / (n!) by A35,
XCMPLX_1:74;
A38: |.(diff(sin,].-r,r.[).n).(s*x) * x |^ n / (n!).| = |.(diff(sin,].-
r,r.[).n).(s*x) * (x |^ n / (n!)).| by XCMPLX_1:74
.= |.(diff(sin,].-r,r.[).n).(s*x).| * |.x |^ n / (n!).| by COMPLEX1:65
.= |.(diff(sin,].-r,r.[).n).(s*x).| * |.x.| |^ n / (n!) by A35,
XCMPLX_1:74;
|.(diff(cos,].-r,r.[).n).(s*x).| >= 0 by COMPLEX1:46;
then
A39: |.(diff(cos,].-r,r.[).n).(s*x).| * (|.x.| |^ n / (n!)) <= r1*(r2 |^
n / (n!)) by A36,A26,A6,XREAL_1:66;
|.(diff(sin,].-r,r.[).n).(s*x).| >= 0 by COMPLEX1:46;
then
|.(diff(sin,].-r,r.[).n).(s*x).| * (|.x.| |^ n / (n!)) <= r1*(r2 |^
n / (n!)) by A36,A17,A6,XREAL_1:66;
hence
|.(diff(sin,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1*r2 |^ n / (n!
) & |.(diff(cos,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1*r2 |^ n / (n!) by
A38,A37,A39,XCMPLX_1:74;
end;
theorem Th23:
for r, e be Real st 0 < r & 0 < e
ex n be Nat
st for m be Nat st n <= m
for x,s be Real st x in ].-r,r.[ & 0
< s & s < 1 holds |.(diff(sin,].-r,r.[).m).(s*x) * x |^ m / (m!).| < e & |.(
diff(cos,].-r,r.[).m).(s*x) * x |^ m / (m!).| < e
proof
let r, e be Real such that
A1: r > 0 and
A2: e > 0;
consider r1,r2 be Real such that
A3: r1 >= 0 & r2 >= 0 and
A4: for n be Nat holds
for x,s be Real st x in ].-r,r.[ & 0 <
s & s < 1 holds |.(diff(sin,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1*r2 |^ n
/ (n!) & |.(diff(cos,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1*r2 |^ n / (n!)
by A1,Th22;
consider n be Nat such that
A5: for m be Nat st n <= m holds (r1 * r2 |^ m / (m!)) < e by A2,A3
,Th12;
take n;
let m be Nat;
assume n <= m;
then
A6: (r1*r2 |^ m /(m!)) < e by A5;
let x,s be Real;
assume x in ].-r,r.[ & 0 < s & s < 1;
then |.(diff(sin,].-r,r.[).m).(s*x) * x |^ m /(m!).| <= r1*r2 |^ m /(m!) &
|.( diff(cos,].-r,r.[).m).(s*x) * x |^ m /(m!).| <= r1*r2 |^ m /(m!) by A4;
hence thesis by A6,XXREAL_0:2;
end;
theorem
for r, e be Real st 0 < r & 0 < e
ex n be Nat st
for m be Nat st n <= m for x being Real st x in ].-r,r.[
holds |.sin.x-Partial_Sums(Maclaurin(sin,].-r,r.[,x)).m.| < e & |.cos.x-
Partial_Sums(Maclaurin(cos,].-r,r.[,x)).m.| < e
proof
let r, e be Real such that
A1: r > 0 and
A2: e > 0;
consider n be Nat such that
A3: for m be Nat st n <= m
for x,s be Real st x in ].-r
,r.[ & 0 < s & s < 1 holds |.(diff(sin,].-r,r.[).m).(s*x) * x |^ m /(m!).|< e
& |.(diff(cos,].-r,r.[).m).(s*x) * x |^ m /(m!).|< e by A1,A2,Th23;
take n;
let m be Nat such that
A4: n <= m;
A5: cos is_differentiable_on m+1, ].-r,r.[ & dom cos =REAL by Th21,
FUNCT_2:def 1;
A6: sin is_differentiable_on m+1, ].-r,r.[ & dom sin = REAL by Th21,
FUNCT_2:def 1;
now
m <= m+1 by NAT_1:11;
then
A7: n <= m+1 by A4,XXREAL_0:2;
let x be Real such that
A8: x in ].-r,r.[;
ex s be Real
st 0 < s & s < 1 & |.sin.x-Partial_Sums( Maclaurin(sin,
].-r,r.[,x)).m.| =|.(diff(sin,].-r,r.[).(m+1)).(s*x) * x |^ (m+1 ) / ((m+1)!).|
by A1,A6,A8,Th4;
hence |.sin.x-Partial_Sums(Maclaurin(sin,].-r,r.[,x)).m.| < e by A3,A8,A7;
ex s be Real
st 0 < s & s < 1 & |.cos.x-Partial_Sums( Maclaurin(cos,
].-r,r.[,x)).m.| =|.(diff(cos,].-r,r.[).(m+1)).(s*x) * x |^ (m+1 ) / ((m+1)!).|
by A1,A5,A8,Th4;
hence |.cos.x-Partial_Sums(Maclaurin(cos,].-r,r.[,x)).m.| < e by A3,A8,A7;
end;
hence thesis;
end;
theorem Th25:
for r, x be Real, m be Nat st 0 < r holds
Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*m+1) = Partial_Sums(x P_sin).m &
Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*m+1) = Partial_Sums(x P_cos).m
proof
let r, x be Real, m be Nat such that
A1: r > 0;
thus Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*m+1) = Partial_Sums(x P_sin)
.m
proof
defpred P[Nat] means Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2
*$1+1) = Partial_Sums(x P_sin).$1;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*(k+1)+1) = Partial_Sums(
Maclaurin(sin,].-r,r.[,x)).(2*k+2) + Maclaurin(sin,].-r,r.[,x).(2*k+3)
by SERIES_1:def 1
.= Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*k+2) + (-1) |^ (k+1) *
x |^ (2*(k+1)+1) / ((2*(k+1)+1)!) by A1,Th20
.= Partial_Sums(Maclaurin(sin,].-r,r.[,x)).((2*k+1)+1) + (x P_sin).(
k+1) by SIN_COS:def 20
.= Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*k+1) + Maclaurin(sin,
].-r,r.[,x).(2*(k+1)) + (x P_sin).(k+1) by SERIES_1:def 1
.= Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*k+1) + 0 + (x P_sin).(
k+1) by A1,Th20
.= Partial_Sums(x P_sin).(k+1) by A3,SERIES_1:def 1;
hence thesis;
end;
Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*0+1) = Partial_Sums(
Maclaurin(sin,].-r,r.[,x)).(2*0) + Maclaurin(sin,].-r,r.[,x).((2*0)+1) by
SERIES_1:def 1
.= Maclaurin(sin,].-r,r.[,x).(2*0) + Maclaurin(sin,].-r,r.[,x).(2*0+1)
by SERIES_1:def 1
.= 0 + Maclaurin(sin,].-r,r.[,x).(2*0+1) by A1,Th20
.= (-1) |^ 0 * x |^ (2*0+1) / ((2*0+1)!) by A1,Th20
.= (x P_sin).0 by SIN_COS:def 20
.= Partial_Sums(x P_sin).0 by SERIES_1:def 1;
then
A4: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
defpred P[Nat] means Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*
$1+1) = Partial_Sums(x P_cos).$1;
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A6: P[k];
Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*(k+1)+1) = Partial_Sums(
Maclaurin(cos,].-r,r.[,x)).(2*k+2) + Maclaurin(cos,].-r,r.[,x).(2*(k+1)+1) by
SERIES_1:def 1
.= Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*k+2) + 0 by A1,Th20
.= Partial_Sums(Maclaurin(cos,].-r,r.[,x)).((2*k+1)+1)
.= Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*k+1) + Maclaurin(cos,].-
r,r.[,x).(2*k+2) by SERIES_1:def 1
.= Partial_Sums(x P_cos).k + (-1) |^ (k+1) * x |^ (2*(k+1)) / ((2*(k+1
))!) by A1,A6,Th20
.= Partial_Sums(x P_cos).k + (x P_cos).(k+1) by SIN_COS:def 21
.= Partial_Sums(x P_cos).(k+1) by SERIES_1:def 1;
hence thesis;
end;
Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*0+1) = Partial_Sums(Maclaurin
(cos,].-r,r.[,x)).(2*0) + Maclaurin(cos,].-r,r.[,x).((2*0)+1) by SERIES_1:def 1
.= Maclaurin(cos,].-r,r.[,x).(2*0) + Maclaurin(cos,].-r,r.[,x).(2*0+1)
by SERIES_1:def 1
.= Maclaurin(cos,].-r,r.[,x).(2*0) + 0 by A1,Th20
.= (-1) |^ 0 * x |^ (2*0) / ((2*0)!) by A1,Th20
.= (x P_cos).0 by SIN_COS:def 21
.= Partial_Sums(x P_cos).0 by SERIES_1:def 1;
then
A7: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A7,A5);
hence thesis;
end;
theorem Th26:
for r, x be Real, m being Nat st 0 < r & m > 0 holds
Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*m) = Partial_Sums(x P_sin).(m-1) &
Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*m) = Partial_Sums(x P_cos).m
proof
let r, x be Real, m be Nat such that
A1: r > 0 and
A2: m > 0;
A3: m-1 is Element of NAT by A2,NAT_1:20;
2*m > 2*0 by A2,XREAL_1:68;
then
A4: 2*m-1 is Element of NAT by NAT_1:20;
then
A5: Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*m) = Partial_Sums(Maclaurin(
sin,].-r,r.[,x)).(2*m-1) + Maclaurin(sin,].-r,r.[,x).((2*m-1)+1) by
SERIES_1:def 1
.= Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*m-1) + 0 by A1,Th20
.= Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*(m-1)+1)
.= Partial_Sums(x P_sin).(m-1) by A1,A3,Th25;
Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*m) = Partial_Sums(Maclaurin(
cos,].-r,r.[,x)).(2*m-1) + Maclaurin(cos,].-r,r.[,x).((2*m-1)+1) by A4,
SERIES_1:def 1
.= Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*m-1) + (-1) |^ m * x |^ (2
*m) / ((2*m)!) by A1,Th20
.= Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*(m-1)+1) + (x P_cos).m by
SIN_COS:def 21
.= Partial_Sums(x P_cos).((m-1)) + (x P_cos).((m-1)+1) by A1,A3,Th25
.= Partial_Sums(x P_cos).m by A3,SERIES_1:def 1;
hence thesis by A5;
end;
theorem Th27:
for r, x be Real, m be Nat st 0 < r holds
Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*m) = Partial_Sums(x P_cos).m
proof
let r, x be Real, m be Nat such that
A1: r > 0;
defpred P[Nat] means Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*
$1) = Partial_Sums(x P_cos).$1;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
P[k];
thus Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*(k+1)) = Partial_Sums(
Maclaurin(cos,].-r,r.[,x)).(2*k+1) + Maclaurin(cos,].-r,r.[,x).((2*k+1)+1) by
SERIES_1:def 1
.= Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*k+1) + (-1) |^ (k+1) * x
|^ (2*(k+1)) / ((2*(k+1))!) by A1,Th20
.= Partial_Sums(x P_cos).k + (-1) |^ (k+1) * x |^ (2*(k+1)) / ((2*(k+1
))!) by A1,Th25
.= Partial_Sums(x P_cos).k + (x P_cos).(k+1) by SIN_COS:def 21
.= Partial_Sums(x P_cos).(k+1) by SERIES_1:def 1;
end;
Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*0) = Maclaurin(cos,].-r,r.[,x
).(2*0) by SERIES_1:def 1
.= (-1) |^ 0 * x |^ (2*0) / ((2*0)!) by A1,Th20
.= (x P_cos).0 by SIN_COS:def 21
.= Partial_Sums(x P_cos).0 by SERIES_1:def 1;
then
A3: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A3,A2);
hence thesis;
end;
theorem
for r, x be Real st r > 0 holds Partial_Sums(Maclaurin(sin,].-r,r.[,x)
) is convergent & sin.x = Sum(Maclaurin(sin,].-r,r.[,x)) & Partial_Sums(
Maclaurin(cos,].-r,r.[,x)) is convergent & cos.x = Sum(Maclaurin(cos,].-r,r.[,x
))
proof
let r, x be Real such that
A1: r > 0;
set g = sin.x;
Sum(x P_sin) = sin.x by SIN_COS:37;
then
A2: lim Partial_Sums(x P_sin) = sin.x by SERIES_1:def 3;
A3: Partial_Sums(x P_sin) is convergent by SIN_COS:36;
A4: for p being Real st p>0
ex n1 being Nat st
for m1 be Nat st m1>=n1 holds |.Partial_Sums(Maclaurin(sin,].-r,r.[,x)
).m1-g.|<p
proof
let p be Real;
assume p > 0;
then consider n be Nat such that
A5: for m being Nat st n<=m holds |.Partial_Sums(x P_sin)
.m-g.| < p by A2,A3,SEQ_2:def 7;
reconsider n1=2*n+2 as Nat;
take n1;
let m1 be Nat such that
A6: m1>=n1;
per cases;
suppose
m1 is even;
then consider j be Nat such that
A7: m1=2*j by ABIAN:def 2;
A8: ((n+1)*2)/2 <= (j*2)/2 by A6,A7,XREAL_1:72;
then
A9: (n+1)-1 <= j-1 by XREAL_1:9;
n+1 >= 0+1 by XREAL_1:6;
then j-1 is Element of NAT by A8,NAT_1:20;
then |.Partial_Sums(x P_sin).(j-1)-g.| < p by A5,A9;
hence thesis by A1,A7,A8,Th26;
end;
suppose
m1 is odd;
then consider j be Nat such that
A10: m1=2*j+1 by ABIAN:9;
n*2+0 <= n*2+1 & (n*2+2)-1 <= (2*j+1)-1 by A6,A10,XREAL_1:6,9;
then n*2 <= j*2 by XXREAL_0:2;
then (n*2)/2 <= (j*2)/2 by XREAL_1:72;
then |.Partial_Sums(x P_sin).j-g.| < p by A5;
hence thesis by A1,A10,Th25;
end;
end;
then Partial_Sums(Maclaurin(sin,].-r,r.[,x)) is convergent by SEQ_2:def 6;
then
A11: lim Partial_Sums(Maclaurin(sin,].-r,r.[,x)) = sin.x by A4,SEQ_2:def 7;
Sum(x P_cos) = cos.x by SIN_COS:37;
then
A12: lim Partial_Sums(x P_cos) = cos.x by SERIES_1:def 3;
set g = cos.x;
A13: Partial_Sums(x P_cos) is convergent by SIN_COS:36;
A14: for p being Real st p>0 holds ex n1 being Nat st for
m1 be Nat st m1>=n1 holds |.Partial_Sums(Maclaurin(cos,].-r,r.[,x)
).m1-g.|<p
proof
let p be Real;
assume p > 0;
then consider n be Nat such that
A15: for m being Nat st n<=m holds |.Partial_Sums(x P_cos
).m-g.| < p by A12,A13,SEQ_2:def 7;
reconsider n1=2*n+1 as Nat;
take n1;
let m1 be Nat such that
A16: m1>=n1;
per cases;
suppose
m1 is even;
then consider j be Nat such that
A17: m1=2*j by ABIAN:def 2;
(n*2)+1 >= n*2 by XREAL_1:29;
then n*2 <= j*2 by A16,A17,XXREAL_0:2;
then (n*2)/2 <= (j*2)/2 by XREAL_1:72;
then |.Partial_Sums(x P_cos).j-g.| < p by A15;
hence thesis by A1,A17,Th27;
end;
suppose
m1 is odd;
then consider j be Nat such that
A18: m1=2*j+1 by ABIAN:9;
(n*2+1)-1 <= (j*2+1)-1 by A16,A18,XREAL_1:9;
then (n*2)/2 <= (j*2)/2 by XREAL_1:72;
then |.Partial_Sums(x P_cos).j-g.| < p by A15;
hence thesis by A1,A18,Th25;
end;
end;
then Partial_Sums(Maclaurin(cos,].-r,r.[,x)) is convergent by SEQ_2:def 6;
then lim Partial_Sums(Maclaurin(cos,].-r,r.[,x)) = cos.x by A14,SEQ_2:def 7;
hence thesis by A4,A11,A14,SEQ_2:def 6,SERIES_1:def 3;
end;