haftmann@28952

1 
(* Title: HOL/Taylor.thy

berghofe@17634

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

berghofe@17634

3 
*)

berghofe@17634

4 

berghofe@17634

5 
header {* Taylor series *}

berghofe@17634

6 

berghofe@17634

7 
theory Taylor

berghofe@17634

8 
imports MacLaurin

berghofe@17634

9 
begin

berghofe@17634

10 

berghofe@17634

11 
text {*

berghofe@17634

12 
We use MacLaurin and the translation of the expansion point @{text c} to @{text 0}

berghofe@17634

13 
to prove Taylor's theorem.

berghofe@17634

14 
*}

berghofe@17634

15 

berghofe@17634

16 
lemma taylor_up:

nipkow@25162

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

berghofe@17634

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

berghofe@17634

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

berghofe@17634

20 
shows "\<exists> t. c < t & t < b &

berghofe@17634

21 
f b = setsum (%m. (diff m c / real (fact m)) * (b  c)^m) {0..<n} +

berghofe@17634

22 
(diff n t / real (fact n)) * (b  c)^n"

berghofe@17634

23 
proof 

berghofe@17634

24 
from INTERV have "0 < bc" by arith

berghofe@17634

25 
moreover

nipkow@25162

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

berghofe@17634

27 
moreover

nipkow@25162

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

berghofe@17634

29 
proof (intro strip)

berghofe@17634

30 
fix m t

berghofe@17634

31 
assume "m < n & 0 <= t & t <= b  c"

berghofe@17634

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

berghofe@17634

33 
moreover

huffman@23069

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

berghofe@17634

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

berghofe@17634

36 
by (rule DERIV_chain2)

berghofe@17634

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

berghofe@17634

38 
qed

berghofe@17634

39 
ultimately

berghofe@17634

40 
have EX:"EX t>0. t < b  c &

berghofe@17634

41 
f (b  c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (b  c) ^ m) +

berghofe@17634

42 
diff n (t + c) / real (fact n) * (b  c) ^ n"

berghofe@17634

43 
by (rule Maclaurin)

berghofe@17634

44 
show ?thesis

berghofe@17634

45 
proof 

berghofe@17634

46 
from EX obtain x where

berghofe@17634

47 
X: "0 < x & x < b  c &

berghofe@17634

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

berghofe@17634

49 
diff n (x + c) / real (fact n) * (b  c) ^ n" ..

berghofe@17634

50 
let ?H = "x + c"

berghofe@17634

51 
from X have "c<?H & ?H<b \<and> f b = (\<Sum>m = 0..<n. diff m c / real (fact m) * (b  c) ^ m) +

berghofe@17634

52 
diff n ?H / real (fact n) * (b  c) ^ n"

nipkow@44890

53 
by fastforce

nipkow@44890

54 
thus ?thesis by fastforce

berghofe@17634

55 
qed

berghofe@17634

56 
qed

berghofe@17634

57 

berghofe@17634

58 
lemma taylor_down:

nipkow@25162

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

berghofe@17634

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

berghofe@17634

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

berghofe@17634

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

berghofe@17634

63 
f a = setsum (% m. (diff m c / real (fact m)) * (a  c)^m) {0..<n} +

berghofe@17634

64 
(diff n t / real (fact n)) * (a  c)^n"

berghofe@17634

65 
proof 

berghofe@17634

66 
from INTERV have "ac < 0" by arith

berghofe@17634

67 
moreover

nipkow@25162

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

berghofe@17634

69 
moreover

berghofe@17634

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

berghofe@17634

71 
proof (rule allI impI)+

berghofe@17634

72 
fix m t

berghofe@17634

73 
assume "m < n & ac <= t & t <= 0"

berghofe@17634

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

berghofe@17634

75 
moreover

huffman@23069

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

berghofe@17634

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

berghofe@17634

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

berghofe@17634

79 
qed

berghofe@17634

80 
ultimately

berghofe@17634

81 
have EX: "EX t>a  c. t < 0 &

berghofe@17634

82 
f (a  c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a  c) ^ m) +

berghofe@17634

83 
diff n (t + c) / real (fact n) * (a  c) ^ n"

berghofe@17634

84 
by (rule Maclaurin_minus)

berghofe@17634

85 
show ?thesis

berghofe@17634

86 
proof 

berghofe@17634

87 
from EX obtain x where X: "a  c < x & x < 0 &

berghofe@17634

88 
f (a  c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a  c) ^ m) +

berghofe@17634

89 
diff n (x + c) / real (fact n) * (a  c) ^ n" ..

berghofe@17634

90 
let ?H = "x + c"

berghofe@17634

91 
from X have "a<?H & ?H<c \<and> f a = (\<Sum>m = 0..<n. diff m c / real (fact m) * (a  c) ^ m) +

berghofe@17634

92 
diff n ?H / real (fact n) * (a  c) ^ n"

nipkow@44890

93 
by fastforce

nipkow@44890

94 
thus ?thesis by fastforce

berghofe@17634

95 
qed

berghofe@17634

96 
qed

berghofe@17634

97 

berghofe@17634

98 
lemma taylor:

nipkow@25162

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

berghofe@17634

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

berghofe@17634

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

berghofe@17634

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

berghofe@17634

103 
f x = setsum (% m. (diff m c / real (fact m)) * (x  c)^m) {0..<n} +

berghofe@17634

104 
(diff n t / real (fact n)) * (x  c)^n"

berghofe@17634

105 
proof (cases "x<c")

berghofe@17634

106 
case True

berghofe@17634

107 
note INIT

berghofe@17634

108 
moreover from DERIV and INTERV

berghofe@17634

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

nipkow@44890

110 
by fastforce

berghofe@17634

111 
moreover note True

berghofe@17634

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

berghofe@17634

113 
ultimately have EX: "\<exists>t>x. t < c \<and> f x =

berghofe@17634

114 
(\<Sum>m = 0..<n. diff m c / real (fact m) * (x  c) ^ m) +

berghofe@17634

115 
diff n t / real (fact n) * (x  c) ^ n"

berghofe@17634

116 
by (rule taylor_down)

berghofe@17634

117 
with True show ?thesis by simp

berghofe@17634

118 
next

berghofe@17634

119 
case False

berghofe@17634

120 
note INIT

berghofe@17634

121 
moreover from DERIV and INTERV

berghofe@17634

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

nipkow@44890

123 
by fastforce

berghofe@17634

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

berghofe@17634

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

berghofe@17634

126 
ultimately have EX: "\<exists>t>c. t < x \<and> f x =

berghofe@17634

127 
(\<Sum>m = 0..<n. diff m c / real (fact m) * (x  c) ^ m) +

berghofe@17634

128 
diff n t / real (fact n) * (x  c) ^ n"

berghofe@17634

129 
by (rule taylor_up)

berghofe@17634

130 
with False show ?thesis by simp

berghofe@17634

131 
qed

berghofe@17634

132 

berghofe@17634

133 
end
