# Theory Taylor

Up to index of Isabelle/HOL/HOL-Complex

theory Taylor
imports MacLaurin
begin

    (*  Title:      HOL/Hyperreal/Taylor.thy
        ID:         $Id: Taylor.thy,v 1.1 2005/09/25 18:14:16 berghofe Exp $
        Author:     Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen
    *)

    header {* Taylor series *}

    theory Taylor
    imports MacLaurin
    begin

    text {*
    We use MacLaurin and the translation of the expansion point @{text c} to @{text 0}
    to prove Taylor's theorem.
    *}

    lemma taylor_up:
      assumes INIT: "0 < n" "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. c < t & t < b &
        f b = setsum (%m. (diff m c / real (fact m)) * (b - c)^m) {0..<n} +
          (diff n t / real (fact n)) * (b - c)^n"
    proof -
      from INTERV have "0 < b-c" by arith
      moreover
      from INIT have "0<n" "((λm x. diff m (x + c)) 0) = (λx. f (x + c))" by auto
      moreover
      have "ALL 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_Id 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)
        thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
      qed
      ultimately
      have EX:"EX t>0. t < b - c &
        f (b - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
          diff n (t + c) / real (fact n) * (b - c) ^ n"
        by (rule Maclaurin)
      show ?thesis
      proof -
        from EX obtain x where
          X: "0 < x & x < b - c &
            f (b - c + c) = (∑m = 0..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
              diff n (x + c) / real (fact n) * (b - c) ^ n" ..
        let ?H = "x + c"
        from X have "c<?H & ?H<b ∧ f b = (∑m = 0..<n. diff m c / real (fact m) * (b - c) ^ m) +
          diff n ?H / real (fact n) * (b - c) ^ n"
          by fastsimp
        thus ?thesis by fastsimp
      qed
    qed

    lemma taylor_down:
      assumes INIT: "0 < n" "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 = setsum (% m. (diff m c / real (fact m)) * (a - c)^m) {0..<n} +
          (diff n t / real (fact n)) * (a - c)^n"
    proof -
      from INTERV have "a-c < 0" by arith
      moreover
      from INIT have "0<n" "((λm x. diff m (x + c)) 0) = (λx. f (x + c))" by auto
      moreover
      have "ALL 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_Id 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)
        thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
      qed
      ultimately
      have EX: "EX t>a - c. t < 0 &
        f (a - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
          diff n (t + c) / real (fact n) * (a - c) ^ n"
        by (rule Maclaurin_minus)
      show ?thesis
      proof -
        from EX obtain x where X: "a - c < x & x < 0 &
          f (a - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
            diff n (x + c) / real (fact n) * (a - c) ^ n" ..
        let ?H = "x + c"
        from X have "a<?H & ?H<c ∧ f a = (∑m = 0..<n. diff m c / real (fact m) * (a - c) ^ m) +
          diff n ?H / real (fact n) * (a - c) ^ n"
          by fastsimp
        thus ?thesis by fastsimp
      qed
    qed

    lemma taylor:
      assumes INIT: "0 < n" "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 = setsum (% m. (diff m c / real (fact m)) * (x - c)^m) {0..<n} +
          (diff n t / real (fact n)) * (x - c)^n"
    proof (cases "x<c")
      case True
      note INIT
      moreover from DERIV and INTERV
      have "∀m t. m < n ∧ x ≤ t ∧ t ≤ b --> DERIV (diff m) t :> diff (Suc m) t"
        by fastsimp
      moreover note True
      moreover from INTERV have "c ≤ b" by simp
      ultimately have EX: "∃t>x. t < c ∧ f x =
        (∑m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) +
          diff n t / real (fact n) * (x - c) ^ n"
        by (rule taylor_down)
      with True show ?thesis by simp
    next
      case False
      note INIT
      moreover from DERIV and INTERV
      have "∀m t. m < n ∧ a ≤ t ∧ t ≤ x --> DERIV (diff m) t :> diff (Suc m) t"
        by fastsimp
      moreover from INTERV have "a ≤ c" by arith
      moreover from False and INTERV have "c < x" by arith
      ultimately have EX: "∃t>c. t < x ∧ f x =
        (∑m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) +
          diff n t / real (fact n) * (x - c) ^ n"
        by (rule taylor_up)
      with False show ?thesis by simp
    qed

    end

lemma taylor_up:

      [| 0 < n; diff 0 = f;
         ∀m t. m < n ∧ a ≤ t ∧ t ≤ b --> DERIV (diff m) t :> diff (Suc m) t; a ≤ c;
         c < b |]
      ==> ∃t>c. t < b ∧
                f b =
                (∑m = 0..<n. diff m c / real (fact m) * (b - c) ^ m) +
                diff n t / real (fact n) * (b - c) ^ n

lemma taylor_down:

      [| 0 < n; diff 0 = f;
         ∀m t. m < n ∧ a ≤ t ∧ t ≤ b --> DERIV (diff m) t :> diff (Suc m) t; a < c;
         c ≤ b |]
      ==> ∃t>a. t < c ∧
                f a =
                (∑m = 0..<n. diff m c / real (fact m) * (a - c) ^ m) +
                diff n t / real (fact n) * (a - c) ^ n

lemma taylor:

      [| 0 < n; diff 0 = f;
         ∀m t. m < n ∧ a ≤ t ∧ t ≤ b --> DERIV (diff m) t :> diff (Suc m) t; a ≤ c;
         c ≤ b; a ≤ x; x ≤ b; x ≠ c |]
      ==> ∃t. (if x < c then x < t ∧ t < c else c < t ∧ t < x) ∧
              f x =
              (∑m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) +
              diff n t / real (fact n) * (x - c) ^ n