summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Taylor.thy

author | hoelzl |

Fri Feb 19 13:40:50 2016 +0100 (2016-02-19) | |

changeset 62378 | 85ed00c1fe7c |

parent 61954 | 1d43f86f48be |

child 63569 | 7e0b0db5e9ac |

permissions | -rw-r--r-- |

generalize more theorems to support enat and ennreal

1 (* Title: HOL/Taylor.thy

2 Author: Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen

3 *)

5 section \<open>Taylor series\<close>

7 theory Taylor

8 imports MacLaurin

9 begin

11 text \<open>

12 We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close>

13 to prove Taylor's theorem.

14 \<close>

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::real. c < t & t < b &

21 f b = (\<Sum>m<n. (diff m c / (fact m)) * (b - c)^m) + (diff n t / (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 obtain x where

39 "0 < x & x < b - c &

40 f (b - c + c) = (\<Sum>m<n. diff m (0 + c) / (fact m) * (b - c) ^ m) +

41 diff n (x + c) / (fact n) * (b - c) ^ n"

42 by (rule Maclaurin [THEN exE])

43 then have "c<x+c & x+c<b \<and> f b = (\<Sum>m<n. diff m c / (fact m) * (b - c) ^ m) +

44 diff n (x+c) / (fact n) * (b - c) ^ n"

45 by fastforce

46 thus ?thesis by fastforce

47 qed

49 lemma taylor_down:

50 fixes a::real

51 assumes INIT: "n>0" "diff 0 = f"

52 and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"

53 and INTERV: "a < c" "c \<le> b"

54 shows "\<exists> t. a < t & t < c &

55 f a = (\<Sum>m<n. (diff m c / (fact m)) * (a - c)^m) + (diff n t / (fact n)) * (a - c)^n"

56 proof -

57 from INTERV have "a-c < 0" by arith

58 moreover

59 from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto

60 moreover

61 have "ALL m t. m < n & a-c <= t & t <= 0 --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"

62 proof (rule allI impI)+

63 fix m t

64 assume "m < n & a-c <= t & t <= 0"

65 with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto

66 moreover

67 from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)

68 ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2)

69 thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp

70 qed

71 ultimately obtain x where

72 "a - c < x & x < 0 &

73 f (a - c + c) = (\<Sum>m<n. diff m (0 + c) / (fact m) * (a - c) ^ m) +

74 diff n (x + c) / (fact n) * (a - c) ^ n"

75 by (rule Maclaurin_minus [THEN exE])

76 then have "a<x+c & x+c<c \<and> f a = (\<Sum>m<n. diff m c / (fact m) * (a - c) ^ m) +

77 diff n (x+c) / (fact n) * (a - c) ^ n"

78 by fastforce

79 thus ?thesis by fastforce

80 qed

82 lemma taylor:

83 fixes a::real

84 assumes INIT: "n>0" "diff 0 = f"

85 and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"

86 and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"

87 shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &

88 f x = (\<Sum>m<n. (diff m c / (fact m)) * (x - c)^m) + (diff n t / (fact n)) * (x - c)^n"

89 proof (cases "x<c")

90 case True

91 note INIT

92 moreover from DERIV and INTERV

93 have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"

94 by fastforce

95 moreover note True

96 moreover from INTERV have "c \<le> b" by simp

97 ultimately have "\<exists>t>x. t < c \<and> f x =

98 (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"

99 by (rule taylor_down)

100 with True show ?thesis by simp

101 next

102 case False

103 note INIT

104 moreover from DERIV and INTERV

105 have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"

106 by fastforce

107 moreover from INTERV have "a \<le> c" by arith

108 moreover from False and INTERV have "c < x" by arith

109 ultimately have "\<exists>t>c. t < x \<and> f x =

110 (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"

111 by (rule taylor_up)

112 with False show ?thesis by simp

113 qed

115 end