src/HOL/Taylor.thy
 author haftmann Fri Oct 10 19:55:32 2014 +0200 (2014-10-10) changeset 58646 cd63a4b12a33 parent 56193 c726ecfb22b6 child 58889 5b7a9633cfa8 permissions -rw-r--r--
specialized specification: avoid trivial instances
```     1 (*  Title:      HOL/Taylor.thy
```
```     2     Author:     Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen
```
```     3 *)
```
```     4
```
```     5 header {* Taylor series *}
```
```     6
```
```     7 theory Taylor
```
```     8 imports MacLaurin
```
```     9 begin
```
```    10
```
```    11 text {*
```
```    12 We use MacLaurin and the translation of the expansion point @{text c} to @{text 0}
```
```    13 to prove Taylor's theorem.
```
```    14 *}
```
```    15
```
```    16 lemma taylor_up:
```
```    17   assumes INIT: "n>0" "diff 0 = f"
```
```    18   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
```
```    19   and INTERV: "a \<le> c" "c < b"
```
```    20   shows "\<exists> t. c < t & t < b &
```
```    21     f b = (\<Sum>m<n. (diff m c / real (fact m)) * (b - c)^m) + (diff n t / real (fact n)) * (b - c)^n"
```
```    22 proof -
```
```    23   from INTERV have "0 < b-c" by arith
```
```    24   moreover
```
```    25   from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
```
```    26   moreover
```
```    27   have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
```
```    28   proof (intro strip)
```
```    29     fix m t
```
```    30     assume "m < n & 0 <= t & t <= b - c"
```
```    31     with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto
```
```    32     moreover
```
```    33     from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
```
```    34     ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)"
```
```    35       by (rule DERIV_chain2)
```
```    36     thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
```
```    37   qed
```
```    38   ultimately
```
```    39   have EX:"EX t>0. t < b - c &
```
```    40     f (b - c + c) = (SUM m<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
```
```    41       diff n (t + c) / real (fact n) * (b - c) ^ n"
```
```    42     by (rule Maclaurin)
```
```    43   show ?thesis
```
```    44   proof -
```
```    45     from EX obtain x where
```
```    46       X: "0 < x & x < b - c &
```
```    47         f (b - c + c) = (\<Sum>m<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
```
```    48           diff n (x + c) / real (fact n) * (b - c) ^ n" ..
```
```    49     let ?H = "x + c"
```
```    50     from X have "c<?H & ?H<b \<and> f b = (\<Sum>m<n. diff m c / real (fact m) * (b - c) ^ m) +
```
```    51       diff n ?H / real (fact n) * (b - c) ^ n"
```
```    52       by fastforce
```
```    53     thus ?thesis by fastforce
```
```    54   qed
```
```    55 qed
```
```    56
```
```    57 lemma taylor_down:
```
```    58   assumes INIT: "n>0" "diff 0 = f"
```
```    59   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
```
```    60   and INTERV: "a < c" "c \<le> b"
```
```    61   shows "\<exists> t. a < t & t < c &
```
```    62     f a = (\<Sum>m<n. (diff m c / real (fact m)) * (a - c)^m) + (diff n t / real (fact n)) * (a - c)^n"
```
```    63 proof -
```
```    64   from INTERV have "a-c < 0" by arith
```
```    65   moreover
```
```    66   from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
```
```    67   moreover
```
```    68   have "ALL m t. m < n & a-c <= t & t <= 0 --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
```
```    69   proof (rule allI impI)+
```
```    70     fix m t
```
```    71     assume "m < n & a-c <= t & t <= 0"
```
```    72     with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto
```
```    73     moreover
```
```    74     from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
```
```    75     ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2)
```
```    76     thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
```
```    77   qed
```
```    78   ultimately
```
```    79   have EX: "EX t>a - c. t < 0 &
```
```    80     f (a - c + c) = (SUM m<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
```
```    81       diff n (t + c) / real (fact n) * (a - c) ^ n"
```
```    82     by (rule Maclaurin_minus)
```
```    83   show ?thesis
```
```    84   proof -
```
```    85     from EX obtain x where X: "a - c < x & x < 0 &
```
```    86       f (a - c + c) = (SUM m<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
```
```    87         diff n (x + c) / real (fact n) * (a - c) ^ n" ..
```
```    88     let ?H = "x + c"
```
```    89     from X have "a<?H & ?H<c \<and> f a = (\<Sum>m<n. diff m c / real (fact m) * (a - c) ^ m) +
```
```    90       diff n ?H / real (fact n) * (a - c) ^ n"
```
```    91       by fastforce
```
```    92     thus ?thesis by fastforce
```
```    93   qed
```
```    94 qed
```
```    95
```
```    96 lemma taylor:
```
```    97   assumes INIT: "n>0" "diff 0 = f"
```
```    98   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
```
```    99   and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"
```
```   100   shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
```
```   101     f x = (\<Sum>m<n. (diff m c / real (fact m)) * (x - c)^m) + (diff n t / real (fact n)) * (x - c)^n"
```
```   102 proof (cases "x<c")
```
```   103   case True
```
```   104   note INIT
```
```   105   moreover from DERIV and INTERV
```
```   106   have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
```
```   107     by fastforce
```
```   108   moreover note True
```
```   109   moreover from INTERV have "c \<le> b" by simp
```
```   110   ultimately have EX: "\<exists>t>x. t < c \<and> f x =
```
```   111     (\<Sum>m<n. diff m c / real (fact m) * (x - c) ^ m) + diff n t / real (fact n) * (x - c) ^ n"
```
```   112     by (rule taylor_down)
```
```   113   with True show ?thesis by simp
```
```   114 next
```
```   115   case False
```
```   116   note INIT
```
```   117   moreover from DERIV and INTERV
```
```   118   have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
```
```   119     by fastforce
```
```   120   moreover from INTERV have "a \<le> c" by arith
```
```   121   moreover from False and INTERV have "c < x" by arith
```
```   122   ultimately have EX: "\<exists>t>c. t < x \<and> f x =
```
```   123     (\<Sum>m<n. diff m c / real (fact m) * (x - c) ^ m) + diff n t / real (fact n) * (x - c) ^ n"
```
```   124     by (rule taylor_up)
```
```   125   with False show ?thesis by simp
```
```   126 qed
```
```   127
```
```   128 end
```