(* Title: HOL/MacLaurin.thy
Author: Jacques D. Fleuriot, 2001 University of Edinburgh
Author: Lawrence C Paulson, 2004
Author: Lukas Bulwahn and Bernhard HÃ¤upler, 2005
*)
section \MacLaurin and Taylor Series\
theory MacLaurin
imports Transcendental
begin
subsection \Maclaurin's Theorem with Lagrange Form of Remainder\
text \This is a very long, messy proof even now that it's been broken down
into lemmas.\
lemma Maclaurin_lemma:
"0 < h \
\B::real. f h = (\m y = x + z"
for x y z :: real
by arith
lemma fact_diff_Suc: "n < Suc m \ fact (Suc m - n) = (Suc m - n) * fact (m - n)"
by (subst fact_reduce) auto
lemma Maclaurin_lemma2:
fixes B
assumes DERIV: "\m t. m < n \ 0\t \ t\h \ DERIV (diff m) t :> diff (Suc m) t"
and INIT: "n = Suc k"
defines "difg \
(\m t::real. diff m t -
((\p (\m t. diff m t - ?difg m t)")
shows "\m t. m < n \ 0 \ t \ t \ h \ DERIV (difg m) t :> difg (Suc m) t"
proof (rule allI impI)+
fix m t
assume INIT2: "m < n \ 0 \ t \ t \ h"
have "DERIV (difg m) t :> diff (Suc m) t -
((\xxxx. (fact x) + real x * (fact x) \ 0"
by (metis add_pos_pos fact_gt_zero less_add_same_cancel1 less_add_same_cancel2
less_numeral_extra(3) mult_less_0_iff of_nat_less_0_iff)
have "\x. (Suc x) * t ^ x * diff (Suc m + x) 0 / fact (Suc x) = diff (Suc m + x) 0 * t^x / fact x"
by (rule nonzero_divide_eq_eq[THEN iffD2]) auto
moreover
have "(n - m) * t ^ (n - Suc m) * B / fact (n - m) = B * (t ^ (n - Suc m) / fact (n - Suc m))"
using \0 < n - m\ by (simp add: divide_simps fact_reduce)
ultimately show "DERIV (difg m) t :> difg (Suc m) t"
unfolding difg_def by (simp add: mult.commute)
qed
lemma Maclaurin:
assumes h: "0 < h"
and n: "0 < n"
and diff_0: "diff 0 = f"
and diff_Suc: "\m t. m < n \ 0 \ t \ t \ h \ DERIV (diff m) t :> diff (Suc m) t"
shows
"\t::real. 0 < t \ t < h \
f h = sum (\m. (diff m 0 / fact m) * h ^ m) {..mm. (diff m 0 / fact m) * t^m) {..p. (diff (m + p) 0 / fact p) * (t ^ p)) {..m t. m < n \ 0 \ t \ t \ h \ DERIV (difg m) t :> difg (Suc m) t"
using diff_Suc m unfolding difg_def [abs_def] by (rule Maclaurin_lemma2)
have difg_eq_0: "\mm x. m < n \ 0 \ x \ x \ h \ isCont (difg m) x"
by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
have differentiable_difg: "\m x. m < n \ 0 \ x \ x \ h \ difg m differentiable (at x)"
by (rule differentiableI [OF difg_Suc [rule_format]]) simp
have difg_Suc_eq_0:
"\m t. m < n \ 0 \ t \ t \ h \ DERIV (difg m) t :> 0 \ difg (Suc m) t = 0"
by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp
have "\t. 0 < t \ t < h \ DERIV (difg m) t :> 0"
using \m < n\
proof (induct m)
case 0
show ?case
proof (rule Rolle)
show "0 < h" by fact
show "difg 0 0 = difg 0 h"
by (simp add: difg_0 g2)
show "\x. 0 \ x \ x \ h \ isCont (difg (0::nat)) x"
by (simp add: isCont_difg n)
show "\x. 0 < x \ x < h \ difg (0::nat) differentiable (at x)"
by (simp add: differentiable_difg n)
qed
next
case (Suc m')
then have "\t. 0 < t \ t < h \ DERIV (difg m') t :> 0"
by simp
then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0"
by fast
have "\t'. 0 < t' \ t' < t \ DERIV (difg (Suc m')) t' :> 0"
proof (rule Rolle)
show "0 < t" by fact
show "difg (Suc m') 0 = difg (Suc m') t"
using t \Suc m' < n\ by (simp add: difg_Suc_eq_0 difg_eq_0)
show "\x. 0 \ x \ x \ t \ isCont (difg (Suc m')) x"
using \t < h\ \Suc m' < n\ by (simp add: isCont_difg)
show "\x. 0 < x \ x < t \ difg (Suc m') differentiable (at x)"
using \t < h\ \Suc m' < n\ by (simp add: differentiable_difg)
qed
with \t < h\ show ?case
by auto
qed
then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0"
by fast
with \m < n\ have "difg (Suc m) t = 0"
by (simp add: difg_Suc_eq_0)
show ?thesis
proof (intro exI conjI)
show "0 < t" by fact
show "t < h" by fact
show "f h = (\mdifg (Suc m) t = 0\ by (simp add: m f_h difg_def)
qed
qed
lemma Maclaurin_objl:
"0 < h \ n > 0 \ diff 0 = f \
(\m t. m < n \ 0 \ t \ t \ h \ DERIV (diff m) t :> diff (Suc m) t) \
(\t. 0 < t \ t < h \ f h = (\mm t. m < n \ 0 \ t \ t \ h \ DERIV (diff m) t :> diff (Suc m) t"
shows "\t. 0 < t \ t \ h \ f h = (\m 0" by simp
from INIT1 this INIT2 DERIV
have "\t>0. t < h \ f h = (\m diff 0 = f \
(\m t. m < n \ 0 \ t \ t \ h \ DERIV (diff m) t :> diff (Suc m) t) \
(\t. 0 < t \ t \ h \ f h = (\mm t. m < n \ h \ t \ t \ 0 \ DERIV (diff m) t :> diff (Suc m) t"
shows "\t. h < t \ t < 0 \ f h = (\mTransform \ABL'\ into \derivative_intros\ format.\
note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
let ?sum = "\t.
(\mt>0. t < - h \ f (- (- h)) = ?sum t"
by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV')
then obtain t where "0 < t" "t < - h" "f (- (- h)) = ?sum t"
by blast
moreover have "(- 1) ^ n * diff n (- t) * (- h) ^ n / fact n = diff n (- t) * h ^ n / fact n"
by (auto simp: power_mult_distrib[symmetric])
moreover
have "(\mm - t < 0 \
f h = (\m n > 0 \ diff 0 = f \
(\m t. m < n \ h \ t \ t \ 0 \ DERIV (diff m) t :> diff (Suc m) t) \
(\t. h < t \ t < 0 \ f h = (\mMore Convenient "Bidirectional" Version.\
(* not good for PVS sin_approx, cos_approx *)
lemma Maclaurin_bi_le_lemma:
"n > 0 \
diff 0 0 = (\mm t. m < n \ \t\ \ \x\ \ DERIV (diff m) t :> diff (Suc m) t"
shows "\t. \t\ \ \x\ \ f x = (\mt. _ \ f x = ?f x t")
proof (cases "n = 0")
case True
with \diff 0 = f\ show ?thesis by force
next
case False
show ?thesis
proof (cases rule: linorder_cases)
assume "x = 0"
with \n \ 0\ \diff 0 = f\ DERIV have "\0\ \ \x\ \ f x = ?f x 0"
by (auto simp add: Maclaurin_bi_le_lemma)
then show ?thesis ..
next
assume "x < 0"
with \n \ 0\ DERIV have "\t>x. t < 0 \ diff 0 x = ?f x t"
by (intro Maclaurin_minus) auto
then obtain t where "x < t" "t < 0"
"diff 0 x = (\mx < 0\ \diff 0 = f\ have "\t\ \ \x\ \