src/HOL/Taylor.thy
 author haftmann Mon Apr 27 10:11:44 2009 +0200 (2009-04-27) changeset 31001 7e6ffd8f51a9 parent 28952 15a4b2cf8c34 child 44890 22f665a2e91c permissions -rw-r--r--
cleaned up theory power further
1 (*  Title:      HOL/Taylor.thy
2     Author:     Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen
3 *)
5 header {* Taylor series *}
7 theory Taylor
8 imports MacLaurin
9 begin
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 *}
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 = setsum (%m. (diff m c / real (fact m)) * (b - c)^m) {0..<n} +
22       (diff n t / real (fact n)) * (b - c)^n"
23 proof -
24   from INTERV have "0 < b-c" by arith
25   moreover
26   from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
27   moreover
28   have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
29   proof (intro strip)
30     fix m t
31     assume "m < n & 0 <= t & t <= b - c"
32     with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto
33     moreover
34     from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
35     ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)"
36       by (rule DERIV_chain2)
37     thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
38   qed
39   ultimately
40   have EX:"EX t>0. t < b - c &
41     f (b - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
42       diff n (t + c) / real (fact n) * (b - c) ^ n"
43     by (rule Maclaurin)
44   show ?thesis
45   proof -
46     from EX obtain x where
47       X: "0 < x & x < b - c &
48         f (b - c + c) = (\<Sum>m = 0..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
49           diff n (x + c) / real (fact n) * (b - c) ^ n" ..
50     let ?H = "x + c"
51     from X have "c<?H & ?H<b \<and> f b = (\<Sum>m = 0..<n. diff m c / real (fact m) * (b - c) ^ m) +
52       diff n ?H / real (fact n) * (b - c) ^ n"
53       by fastsimp
54     thus ?thesis by fastsimp
55   qed
56 qed
58 lemma taylor_down:
59   assumes INIT: "n>0" "diff 0 = f"
60   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
61   and INTERV: "a < c" "c \<le> b"
62   shows "\<exists> t. a < t & t < c &
63     f a = setsum (% m. (diff m c / real (fact m)) * (a - c)^m) {0..<n} +
64       (diff n t / real (fact n)) * (a - c)^n"
65 proof -
66   from INTERV have "a-c < 0" by arith
67   moreover
68   from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
69   moreover
70   have "ALL m t. m < n & a-c <= t & t <= 0 --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
71   proof (rule allI impI)+
72     fix m t
73     assume "m < n & a-c <= t & t <= 0"
74     with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto
75     moreover
76     from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
77     ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2)
78     thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
79   qed
80   ultimately
81   have EX: "EX t>a - c. t < 0 &
82     f (a - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
83       diff n (t + c) / real (fact n) * (a - c) ^ n"
84     by (rule Maclaurin_minus)
85   show ?thesis
86   proof -
87     from EX obtain x where X: "a - c < x & x < 0 &
88       f (a - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
89         diff n (x + c) / real (fact n) * (a - c) ^ n" ..
90     let ?H = "x + c"
91     from X have "a<?H & ?H<c \<and> f a = (\<Sum>m = 0..<n. diff m c / real (fact m) * (a - c) ^ m) +
92       diff n ?H / real (fact n) * (a - c) ^ n"
93       by fastsimp
94     thus ?thesis by fastsimp
95   qed
96 qed
98 lemma taylor:
99   assumes INIT: "n>0" "diff 0 = f"
100   and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
101   and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"
102   shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
103     f x = setsum (% m. (diff m c / real (fact m)) * (x - c)^m) {0..<n} +
104       (diff n t / real (fact n)) * (x - c)^n"
105 proof (cases "x<c")
106   case True
107   note INIT
108   moreover from DERIV and INTERV
109   have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
110     by fastsimp
111   moreover note True
112   moreover from INTERV have "c \<le> b" by simp
113   ultimately have EX: "\<exists>t>x. t < c \<and> f x =
114     (\<Sum>m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) +
115       diff n t / real (fact n) * (x - c) ^ n"
116     by (rule taylor_down)
117   with True show ?thesis by simp
118 next
119   case False
120   note INIT
121   moreover from DERIV and INTERV
122   have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
123     by fastsimp
124   moreover from INTERV have "a \<le> c" by arith
125   moreover from False and INTERV have "c < x" by arith
126   ultimately have EX: "\<exists>t>c. t < x \<and> f x =
127     (\<Sum>m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) +
128       diff n t / real (fact n) * (x - c) ^ n"
129     by (rule taylor_up)
130   with False show ?thesis by simp
131 qed
133 end