Quelle MacLaurin.thy

Sprache: Isabelle

(*  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
  by (rule exI[where x = "(f h - (∑m]) simp

lemma eq_diff_eq': "x = y - z ⟷ 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
    (is "difg ≡ (λ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 -
    ((∑x
     real (n - m) * t ^ (n - Suc m) * B / fact (n - m))"
    by (auto simp: difg_def intro!: derivative_eq_intros DERIV[rule_format, OF INIT2])
  moreover
  from INIT2 have intvl: "{.. and "0 < n - m"
    unfolding atLeast0LessThan[symmetric] by auto
  have "(∑x
      (∑x
    unfolding intvl by (subst sum.insert) (auto simp: sum.reindex)
  moreover
  have fact_neq_0: "∧x. (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 🚫 - m› by (simp add: field_split_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) {..
proof -
  from n obtain m where m: "n = Suc m"
    by (cases n) (simp add: n)
  from m have "m < n" by simp

  obtain B where f_h: "f h = (∑m
    using Maclaurin_lemma [OF h] ..

  define g where [abs_def]: "g t =
    f t - (sum (λm. (diff m 0 / fact m) * t^m) {.. for t
  have g2: "g 0 = 0" "g h = 0"
    by (simp_all add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 sum.reindex)

  define difg where [abs_def]: "difg m t =
    diff m t - (sum (λp. (diff (m + p) 0 / fact p) * (t ^ p)) {..
      B * ((t ^ (n - m)) / fact (n - m)))" for m t
  have difg_0: "difg 0 = g"
    by (simp add: difg_def g_def diff_0)
  have difg_Suc: "∀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: "∀m
    by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff sum.reindex)
  have isCont_difg: "∧m 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)"
    using difg_Suc real_differentiable_def by auto
  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 🚫›
  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 "continuous_on {0..h} (difg 0)"
        by (simp add: continuous_at_imp_continuous_on isCont_difg n)
    qed (simp add: differentiable_difg n)
  next
    case (Suc m')
    then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0"
      by force
    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' 🚫› by (simp add: difg_Suc_eq_0 difg_eq_0)
      have "∧x. 0 ≤ x ∧ x ≤ t ==> isCont (difg (Suc m')) x"
        using ‹t 🚫› ‹Suc m' 🚫› by (simp add: isCont_difg)
      then show "continuous_on {0..t} (difg (Suc m'))"
        by (simp add: continuous_at_imp_continuous_on)
    qed (use ‹t 🚫› ‹Suc m' 🚫› in ‹simp add: differentiable_difg›)
    with ‹t 🚫› show ?case
      by auto
  qed
  then obtain t where "0 < t" "t < h" "difg (Suc m) t = 0"
    using ‹m 🚫› difg_Suc_eq_0 by force
  show ?thesis
  proof (intro exI conjI)
    show "0 < t" "t < h" by fact+
    show "f h = (∑m
      using ‹difg (Suc m) t = 0› by (simp add: m f_h difg_def)
  qed
qed

lemma Maclaurin2:
  fixes n :: nat
    and h :: real
  assumes INIT1: "0 < h"
    and INIT2: "diff 0 = f"
    and DERIV: "∀m t. m < n ∧ 0 ≤ t ∧ t ≤ h ⟶ DERIV (diff m) t :> diff (Suc m) t"
  shows "∃t. 0 < t ∧ t ≤ h ∧ f h = (∑m
proof (cases n)
  case 0
  with INIT1 INIT2 show ?thesis by fastforce
next
  case Suc
  then have "n > 0" by simp
  from Maclaurin [OF INIT1 this INIT2 DERIV]
  show ?thesis by fastforce
qed

lemma Maclaurin_minus:
  fixes n :: nat and h :: real
  assumes "h < 0" "0 < n" "diff 0 = f"
    and DERIV: "∀m t. m < n ∧ h ≤ t ∧ t ≤ 0 ⟶ DERIV (diff m) t :> diff (Suc m) t"
  shows "∃t. h < t ∧ t < 0 ∧ f h = (∑m
proof -
  txt ‹Transform ‹ABL'› into ‹derivative_intros› format.›
  note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
  let ?sum = "λt.
    (∑m
    (- 1) ^ n * diff n (- t) / (fact n) * (- h) ^ n"
  from assms have "∃t>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 "(∑m∑m
    by (auto intro: sum.cong simp add: power_mult_distrib[symmetric])
  ultimately have "h < - t ∧ - t < 0 ∧
    f h = (∑m
    by auto
  then show ?thesis ..
qed

subsection ‹More Convenient "Bidirectional" Version.›

lemma Maclaurin_bi_le:
  fixes n :: nat and x :: real
  assumes "diff 0 = f"
    and DERIV : "∀m t. m < n ∧ ∣t∣ ≤ ∣x∣ ⟶ DERIV (diff m) t :> diff (Suc m) t"
  shows "∃t. ∣t∣ ≤ ∣x∣ ∧ f x = (∑m
    (is "∃t. _ ∧ 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
    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 = (∑m
      by blast
    with ‹x 🚫› ‹diff 0 = f› show ?thesis by force
  next
    assume "x > 0"
    with ‹n ≠ 0› ‹diff 0 = f› DERIV have "∃t>0. t < x ∧ diff 0 x = ?f x t"
      by (intro Maclaurin) auto
    then obtain t where "0 < t" "t < x"
      "diff 0 x = (∑m
      by blast
    with ‹x > 0› ‹diff 0 = f› have "∣t∣ ≤ ∣x∣ ∧ f x = ?f x t" by simp
    then show ?thesis ..
  qed
qed

lemma Maclaurin_all_lt:
  fixes x :: real
  assumes INIT1: "diff 0 = f"
    and INIT2: "0 < n"
    and INIT3: "x ≠ 0"
    and DERIV: "∀m x. DERIV (diff m) x :> diff(Suc m) x"
  shows "∃t. 0 < ∣t∣ ∧ ∣t∣ < ∣x∣ ∧ f x =
      (∑m
    (is "∃t. _ ∧ _ ∧ f x = ?f x t")
proof (cases rule: linorder_cases)
  assume "x = 0"
  with INIT3 show ?thesis ..
next
  assume "x < 0"
  with assms have "∃t>x. t < 0 ∧ f x = ?f x t"
    by (intro Maclaurin_minus) auto
  then show ?thesis by force
next
  assume "x > 0"
  with assms have "∃t>0. t < x ∧ f x = ?f x t"
    by (intro Maclaurin) auto
  then show ?thesis by force
qed

lemma Maclaurin_zero: "x = 0 ==> n ≠ 0 ==> (∑m
  for x :: real and n :: nat
  by simp

lemma Maclaurin_all_le:
  fixes x :: real and n :: nat
  assumes INIT: "diff 0 = f"
    and DERIV: "∀m x. DERIV (diff m) x :> diff (Suc m) x"
  shows "∃t. ∣t∣ ≤ ∣x∣ ∧ f x = (∑m
    (is "∃t. _ ∧ f x = ?f x t")
proof (cases "n = 0")
  case True
  with INIT show ?thesis by force
next
  case False
  show ?thesis
    using DERIV INIT Maclaurin_bi_le by auto
qed

lemma Maclaurin_all_le_objl:
  "diff 0 = f ∧ (∀m x. DERIV (diff m) x :> diff (Suc m) x) ⟶
    (∃t::real. ∣t∣ ≤ ∣x∣ ∧ f x = (∑m
  for x :: real and n :: nat
  by (blast intro: Maclaurin_all_le)

subsection ‹Version for Exponential Function›

lemma Maclaurin_exp_lt:
  fixes x :: real and n :: nat
  shows
    "x ≠ 0 ==> n > 0 ==>
      (∃t. 0 < ∣t∣ ∧ ∣t∣ < ∣x∣ ∧ exp x = (∑m
using Maclaurin_all_lt [where diff = "λn. exp" and f = exp and x = x and n = n] by auto

lemma Maclaurin_exp_le:
  fixes x :: real and n :: nat
  shows "∃t. ∣t∣ ≤ ∣x∣ ∧ exp x = (∑m
  using Maclaurin_all_le_objl [where diff = "λn. exp" and f = exp and x = x and n = n] by auto

corollary exp_lower_Taylor_quadratic: "0 ≤ x ==> 1 + x + x🪙2 / 2 ≤ exp x"
  for x :: real
  using Maclaurin_exp_le [of x 3] by (auto simp: numeral_3_eq_3 power2_eq_square)

corollary ln_2_less_1: "ln 2 < (1::real)"
  by (smt (verit) ln_eq_minus_one ln_le_minus_one)

subsection ‹Version for Sine Function›

lemma mod_exhaust_less_4: "m mod 4 = 0 ∨ m mod 4 = 1 ∨ m mod 4 = 2 ∨ m mod 4 = 3"
  for m :: nat
  by auto

text ‹It is unclear why so many variant results are needed.›

lemma sin_expansion_lemma: "sin (x + real (Suc m) * pi / 2) = cos (x + real m * pi / 2)"
  by (auto simp: cos_add sin_add add_divide_distrib distrib_right)

lemma Maclaurin_sin_expansion2:
  "∃t. ∣t∣ ≤ ∣x∣ ∧
    sin x = (∑m
proof (cases "n = 0 ∨ x = 0")
  case False
  let ?diff = "λn x. sin (x + 1/2 * real n * pi)"
  have "∃t. 0 < ∣t∣ ∧ ∣t∣ < ∣x∣ ∧ sin x =
      (∑m
  proof (rule Maclaurin_all_lt)
    show "∀m x. ((λt. sin (t + 1/2 * real m * pi)) has_real_derivative
           sin (x + 1/2 * real (Suc m) * pi)) (at x)"
      by (rule allI derivative_eq_intros | use sin_expansion_lemma in force)+
  qed (use False in auto)
  then show ?thesis
    apply (rule ex_forward, simp)
    apply (rule sum.cong[OF refl])
    apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
    done
qed auto

lemma Maclaurin_sin_expansion:
  "∃t. sin x = (∑m
  using Maclaurin_sin_expansion2 [of x n] by blast

lemma Maclaurin_sin_expansion3:
  assumes "n > 0" "x > 0"
    shows "∃t. 0 < t ∧ t < x ∧
          sin x = (∑m
proof -
  let ?diff = "λn x. sin (x + 1/2 * real n * pi)"
  have "∃t. 0 < t ∧ t < x ∧ sin x = (∑m
  proof (rule Maclaurin)
    show "∀m t. m < n ∧ 0 ≤ t ∧ t ≤ x ⟶
                ((λu. sin (u + 1/2 * real m * pi)) has_real_derivative
                 sin (t + 1/2 * real (Suc m) * pi)) (at t)"
      using DERIV_shift sin_expansion_lemma by fastforce
  qed (use assms in auto)
  then show ?thesis
    apply (rule ex_forward, simp)
    apply (rule sum.cong[OF refl])
    apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
    done
qed

lemma Maclaurin_sin_expansion4:
  assumes "0 < x"
  shows "∃t. 0 < t ∧ t ≤ x ∧ sin x = (∑m
proof -
  let ?diff = "λn x. sin (x + 1/2 * real n * pi)"
  have "∃t. 0 < t ∧ t ≤ x ∧ sin x = (∑m
  proof (rule Maclaurin2)
    show "∀m t. m < n ∧ 0 ≤ t ∧ t ≤ x ⟶
                ((λu. sin (u + 1/2 * real m * pi)) has_real_derivative
                 sin (t + 1/2 * real (Suc m) * pi)) (at t)"
      using DERIV_shift sin_expansion_lemma by fastforce
  qed (use assms in auto)
  then show ?thesis
    apply (rule ex_forward, simp)
    apply (rule sum.cong[OF refl])
    apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
    done
qed

subsection ‹Maclaurin Expansion for Cosine Function›

lemma sumr_cos_zero_one [simp]: "(∑m
  by (induct n) auto

lemma cos_expansion_lemma: "cos (x + real (Suc m) * pi / 2) = - sin (x + real m * pi / 2)"
  by (auto simp: cos_add sin_add distrib_right add_divide_distrib)

lemma Maclaurin_cos_expansion:
  "∃t::real. ∣t∣ ≤ ∣x∣ ∧
    cos x = (∑m
proof (cases "n = 0 ∨ x = 0")
  case False
  let ?diff = "λn x. cos (x + 1/2 * real n * pi)"
  have "∃t. 0 < ∣t∣ ∧ ∣t∣ < ∣x∣ ∧ cos x =
      (∑m
  proof (rule Maclaurin_all_lt)
    show "∀m x. ((λt. cos (t + 1/2 * real m * pi)) has_real_derivative
           cos (x + 1/2 * real (Suc m) * pi)) (at x)"
      using cos_expansion_lemma
      by (intro allI derivative_eq_intros | simp)+
  qed (use False in auto)
  then show ?thesis
    apply (rule ex_forward, simp)
    apply (rule sum.cong[OF refl])
    apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE simp del: of_nat_Suc)
    done
qed auto

lemma Maclaurin_cos_expansion2:
  assumes "x > 0" "n > 0"
  shows "∃t. 0 < t ∧ t < x ∧
      cos x = (∑m
proof -
  let ?diff = "λn x. cos (x + 1/2 * real n * pi)"
  have "∃t. 0 < t ∧ t < x ∧ cos x = (∑m
  proof (rule Maclaurin)
    show "∀m t. m < n ∧ 0 ≤ t ∧ t ≤ x ⟶
              ((λu. cos (u + 1 / 2 * real m * pi)) has_real_derivative
               cos (t + 1 / 2 * real (Suc m) * pi)) (at t)"
      by (simp add: cos_expansion_lemma del: of_nat_Suc)
  qed (use assms in auto)
  then show ?thesis
    apply (rule ex_forward, simp)
    apply (rule sum.cong[OF refl])
    apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
    done
qed

lemma Maclaurin_minus_cos_expansion:
  assumes "n > 0" "x < 0"
  shows "∃t. x < t ∧ t < 0 ∧
         cos x = (∑m
proof -
  let ?diff = "λn x. cos (x + 1/2 * real n * pi)"
  have "∃t. x < t ∧ t < 0 ∧ cos x = (∑m
  proof (rule Maclaurin_minus)
    show "∀m t. m < n ∧ x ≤ t ∧ t ≤ 0 ⟶
              ((λu. cos (u + 1 / 2 * real m * pi)) has_real_derivative
               cos (t + 1 / 2 * real (Suc m) * pi)) (at t)"
      by (simp add: cos_expansion_lemma del: of_nat_Suc)
  qed (use assms in auto)
  then show ?thesis
    apply (rule ex_forward, simp)
    apply (rule sum.cong[OF refl])
    apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
    done
qed

(* Version for ln(1 +/- x). Where is it?? *)

lemma sin_bound_lemma: "x = y ==> ∣u∣ ≤ v ==> ∣(x + u) - y∣ ≤ v"
  for x y u v :: real
  by auto

lemma Maclaurin_sin_bound: "∣sin x - (∑m∣ ≤ inverse (fact n) * ∣x∣ ^ n"
proof -
  have est: "x ≤ 1 ==> 0 ≤ y ==> x * y ≤ 1 * y" for x y :: real
    by (rule mult_right_mono) simp_all
  let ?diff = "λ(n::nat) (x::real).
    if n mod 4 = 0 then sin x
    else if n mod 4 = 1 then cos x
    else if n mod 4 = 2 then - sin x
    else - cos x"
  have diff_0: "?diff 0 = sin" by simp
  have "DERIV (?diff m) x :> ?diff (Suc m) x" for m and x
    using mod_exhaust_less_4 [of m]
    by (auto simp: mod_Suc intro!: derivative_eq_intros)
  then have DERIV_diff: "∀m x. DERIV (?diff m) x :> ?diff (Suc m) x"
    by blast
  from Maclaurin_all_le [OF diff_0 DERIV_diff]
  obtain t where t1: "∣t∣ ≤ ∣x∣"
    and t2: "sin x = (∑m
    by fast
  have diff_m_0: "?diff m 0 = (if even m then 0 else (- 1) ^ ((m - Suc 0) div 2))" for m
    using mod_exhaust_less_4 [of m]
    by (auto simp: minus_one_power_iff even_even_mod_4_iff [of m] dest: even_mod_4_div_2 odd_mod_4_div_2)
  show ?thesis
    apply (subst t2)
    apply (rule sin_bound_lemma)
     apply (rule sum.cong[OF refl])
    apply (simp add: diff_m_0 sin_coeff_def)
    using est
    apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
        simp: ac_simps divide_inverse power_abs [symmetric] abs_mult)
    done
qed

section ‹Taylor series›

text ‹
We use MacLaurin and the translation of the expansion point ‹c› t
  to prove Taylor's theorem.
›

lemma Taylor_up:
  assumes INIT: "n > 0" "diff 0 = f"
    and DERIV: "∀m t. m < n ∧ a ≤ t ∧ t ≤ b ⟶ DERIV (diff m) t :> (diff (Suc m) t)"
    and INTERV: "a ≤ c" "c < b"
  shows "∃t::real. c < t ∧ t < b ∧
    f b = (∑m
proof -
  from INTERV have "0 < b - c" by arith
  moreover from INIT have "n > 0" "(λm x. diff m (x + c)) 0 = (λx. f (x + c))"
    by auto
  moreover
  have "∀m t. m < n ∧ 0 ≤ t ∧ t ≤ b - c ⟶ DERIV (λx. diff m (x + c)) t :> diff (Suc m) (t + c)"
  proof (intro strip)
    fix m t
    assume "m < n ∧ 0 ≤ t ∧ t ≤ b - c"
    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
      by auto
    moreover from DERIV_ident and DERIV_const have "DERIV (λx. x + c) t :> 1 + 0"
      by (rule DERIV_add)
    ultimately have "DERIV (λx. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
      by (rule DERIV_chain2)
    then show "DERIV (λx. diff m (x + c)) t :> diff (Suc m) (t + c)"
      by simp
  qed
  ultimately obtain x where
    "0 < x ∧ x < b - c ∧
      f (b - c + c) =
        (∑m
     by (rule Maclaurin [THEN exE])
  then show ?thesis
    by (smt (verit) sum.cong)
qed

lemma Taylor_down:
  fixes a :: real and n :: nat
  assumes INIT: "n > 0" "diff 0 = f"
    and DERIV: "(∀m t. m < n ∧ a ≤ t ∧ t ≤ b ⟶ DERIV (diff m) t :> diff (Suc m) t)"
    and INTERV: "a < c" "c ≤ b"
  shows "∃t. a < t ∧ t < c ∧
    f a = (∑m
proof -
  from INTERV have "a-c < 0" by arith
  moreover from INIT have "n > 0" "(λm x. diff m (x + c)) 0 = (λx. f (x + c))"
    by auto
  moreover
  have "∀m t. m < n ∧ a - c ≤ t ∧ t ≤ 0 ⟶ DERIV (λx. diff m (x + c)) t :> diff (Suc m) (t + c)"
  proof (rule allI impI)+
    fix m t
    assume "m < n ∧ a - c ≤ t ∧ t ≤ 0"
    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
      by auto
    moreover from DERIV_ident and DERIV_const have "DERIV (λx. x + c) t :> 1 + 0"
      by (rule DERIV_add)
    ultimately show "DERIV (λx. diff m (x + c)) t :> diff (Suc m) (t + c)"
      using DERIV_chain2 DERIV_shift by blast
  qed
  ultimately obtain x where
    "a - c < x ∧ x < 0 ∧
      f (a - c + c) =
        (∑m
    by (rule Maclaurin_minus [THEN exE])
  then have "a < x + c ∧ x + c < c ∧
    f a = (∑m
    by fastforce
  then show ?thesis by fastforce
qed

theorem Taylor:
  fixes a :: real and n :: nat
  assumes INIT: "n > 0" "diff 0 = f"
    and DERIV: "∀m t. m < n ∧ a ≤ t ∧ t ≤ b ⟶ DERIV (diff m) t :> diff (Suc m) t"
    and INTERV: "a ≤ c " "c ≤ b" "a ≤ x" "x ≤ b" "x ≠ c"
  shows "∃t.
    (if x < c then x < t ∧ t < c else c < t ∧ t < x) ∧
    f x = (∑m
proof (cases "x < c")
  case True
  note INIT
  moreover have "∀m t. m < n ∧ x ≤ t ∧ t ≤ b ⟶ DERIV (diff m) t :> diff (Suc m) t"
    using DERIV and INTERV by fastforce
  ultimately show ?thesis
    using True INTERV Taylor_down by simp
next
  case False
  note INIT
  moreover have "∀m t. m < n ∧ a ≤ t ∧ t ≤ x ⟶ DERIV (diff m) t :> diff (Suc m) t"
    using DERIV and INTERV by fastforce
  ultimately show ?thesis
    using Taylor_up INTERV False by simp
qed

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet am 2026-04-26) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.