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

src/HOL/Taylor.thy

author | hoelzl |

Tue Nov 05 09:44:57 2013 +0100 (2013-11-05) | |

changeset 54257 | 5c7a3b6b05a9 |

parent 44890 | 22f665a2e91c |

child 56193 | c726ecfb22b6 |

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

generalize SUP and INF to the syntactic type classes Sup and Inf

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 fastforce

54 thus ?thesis by fastforce

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 fastforce

94 thus ?thesis by fastforce

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 fastforce

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 fastforce

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