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 &

hoelzl@56193

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

berghofe@17634

22 
proof 

berghofe@17634

23 
from INTERV have "0 < bc" by arith

berghofe@17634

24 
moreover

nipkow@25162

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

berghofe@17634

26 
moreover

nipkow@25162

27 
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

28 
proof (intro strip)

berghofe@17634

29 
fix m t

berghofe@17634

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

berghofe@17634

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

berghofe@17634

32 
moreover

huffman@23069

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

berghofe@17634

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

berghofe@17634

35 
by (rule DERIV_chain2)

berghofe@17634

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

berghofe@17634

37 
qed

berghofe@17634

38 
ultimately

berghofe@17634

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

hoelzl@56193

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

berghofe@17634

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

berghofe@17634

42 
by (rule Maclaurin)

berghofe@17634

43 
show ?thesis

berghofe@17634

44 
proof 

berghofe@17634

45 
from EX obtain x where

berghofe@17634

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

hoelzl@56193

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

berghofe@17634

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

berghofe@17634

49 
let ?H = "x + c"

hoelzl@56193

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

berghofe@17634

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

nipkow@44890

52 
by fastforce

nipkow@44890

53 
thus ?thesis by fastforce

berghofe@17634

54 
qed

berghofe@17634

55 
qed

berghofe@17634

56 

berghofe@17634

57 
lemma taylor_down:

nipkow@25162

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

berghofe@17634

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

berghofe@17634

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

berghofe@17634

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

hoelzl@56193

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

berghofe@17634

63 
proof 

berghofe@17634

64 
from INTERV have "ac < 0" by arith

berghofe@17634

65 
moreover

nipkow@25162

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

berghofe@17634

67 
moreover

berghofe@17634

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

berghofe@17634

69 
proof (rule allI impI)+

berghofe@17634

70 
fix m t

berghofe@17634

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

berghofe@17634

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

berghofe@17634

73 
moreover

huffman@23069

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

berghofe@17634

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

berghofe@17634

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

berghofe@17634

77 
qed

berghofe@17634

78 
ultimately

berghofe@17634

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

hoelzl@56193

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

berghofe@17634

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

berghofe@17634

82 
by (rule Maclaurin_minus)

berghofe@17634

83 
show ?thesis

berghofe@17634

84 
proof 

berghofe@17634

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

hoelzl@56193

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

berghofe@17634

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

berghofe@17634

88 
let ?H = "x + c"

hoelzl@56193

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

berghofe@17634

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

nipkow@44890

91 
by fastforce

nipkow@44890

92 
thus ?thesis by fastforce

berghofe@17634

93 
qed

berghofe@17634

94 
qed

berghofe@17634

95 

berghofe@17634

96 
lemma taylor:

nipkow@25162

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

berghofe@17634

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

berghofe@17634

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

berghofe@17634

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

hoelzl@56193

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

berghofe@17634

102 
proof (cases "x<c")

berghofe@17634

103 
case True

berghofe@17634

104 
note INIT

berghofe@17634

105 
moreover from DERIV and INTERV

berghofe@17634

106 
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

107 
by fastforce

berghofe@17634

108 
moreover note True

berghofe@17634

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

berghofe@17634

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

hoelzl@56193

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

berghofe@17634

112 
by (rule taylor_down)

berghofe@17634

113 
with True show ?thesis by simp

berghofe@17634

114 
next

berghofe@17634

115 
case False

berghofe@17634

116 
note INIT

berghofe@17634

117 
moreover from DERIV and INTERV

berghofe@17634

118 
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

119 
by fastforce

berghofe@17634

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

berghofe@17634

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

berghofe@17634

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

hoelzl@56193

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

berghofe@17634

124 
by (rule taylor_up)

berghofe@17634

125 
with False show ?thesis by simp

berghofe@17634

126 
qed

berghofe@17634

127 

berghofe@17634

128 
end
