src/HOL/Taylor.thy
author blanchet
Tue, 12 Nov 2013 13:47:24 +0100
changeset 54396 8baee6b04a7c
parent 44890 22f665a2e91c
child 56193 c726ecfb22b6
permissions -rw-r--r--
moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 25162
diff changeset
     1
(*  Title:      HOL/Taylor.thy
17634
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
     2
    Author:     Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
     3
*)
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
     4
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
     5
header {* Taylor series *}
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
     6
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
     7
theory Taylor
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
     8
imports MacLaurin
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
     9
begin
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    10
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    11
text {*
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    12
We use MacLaurin and the translation of the expansion point @{text c} to @{text 0}
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    13
to prove Taylor's theorem.
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    14
*}
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    15
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    16
lemma taylor_up: 
25162
ad4d5365d9d8 went back to >0
nipkow
parents: 25134
diff changeset
    17
  assumes INIT: "n>0" "diff 0 = f"
17634
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    18
  and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    19
  and INTERV: "a \<le> c" "c < b" 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    20
  shows "\<exists> t. c < t & t < b & 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    21
    f b = setsum (%m. (diff m c / real (fact m)) * (b - c)^m) {0..<n} +
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    22
      (diff n t / real (fact n)) * (b - c)^n"
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    23
proof -
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    24
  from INTERV have "0 < b-c" by arith
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    25
  moreover 
25162
ad4d5365d9d8 went back to >0
nipkow
parents: 25134
diff changeset
    26
  from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
17634
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    27
  moreover
25162
ad4d5365d9d8 went back to >0
nipkow
parents: 25134
diff changeset
    28
  have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
17634
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    29
  proof (intro strip)
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    30
    fix m t
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    31
    assume "m < n & 0 <= t & t <= b - c"
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    32
    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    33
    moreover
23069
cdfff0241c12 rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents: 17634
diff changeset
    34
    from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
17634
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    35
    ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)"
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    36
      by (rule DERIV_chain2)
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    37
    thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    38
  qed
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    39
  ultimately 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    40
  have EX:"EX t>0. t < b - c & 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    41
    f (b - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    42
      diff n (t + c) / real (fact n) * (b - c) ^ n" 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    43
    by (rule Maclaurin)
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    44
  show ?thesis
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    45
  proof -
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    46
    from EX obtain x where 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    47
      X: "0 < x & x < b - c & 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    48
        f (b - c + c) = (\<Sum>m = 0..<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    49
          diff n (x + c) / real (fact n) * (b - c) ^ n" ..
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    50
    let ?H = "x + c"
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    51
    from X have "c<?H & ?H<b \<and> f b = (\<Sum>m = 0..<n. diff m c / real (fact m) * (b - c) ^ m) +
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    52
      diff n ?H / real (fact n) * (b - c) ^ n"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 28952
diff changeset
    53
      by fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 28952
diff changeset
    54
    thus ?thesis by fastforce
17634
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    55
  qed
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    56
qed
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    57
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    58
lemma taylor_down:
25162
ad4d5365d9d8 went back to >0
nipkow
parents: 25134
diff changeset
    59
  assumes INIT: "n>0" "diff 0 = f"
17634
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    60
  and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    61
  and INTERV: "a < c" "c \<le> b"
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    62
  shows "\<exists> t. a < t & t < c & 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    63
    f a = setsum (% m. (diff m c / real (fact m)) * (a - c)^m) {0..<n} +
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    64
      (diff n t / real (fact n)) * (a - c)^n" 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    65
proof -
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    66
  from INTERV have "a-c < 0" by arith
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    67
  moreover 
25162
ad4d5365d9d8 went back to >0
nipkow
parents: 25134
diff changeset
    68
  from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
17634
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    69
  moreover
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    70
  have "ALL m t. m < n & a-c <= t & t <= 0 --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    71
  proof (rule allI impI)+
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    72
    fix m t
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    73
    assume "m < n & a-c <= t & t <= 0"
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    74
    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    75
    moreover
23069
cdfff0241c12 rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents: 17634
diff changeset
    76
    from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
17634
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    77
    ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2)
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    78
    thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    79
  qed
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    80
  ultimately 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    81
  have EX: "EX t>a - c. t < 0 &
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    82
    f (a - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    83
      diff n (t + c) / real (fact n) * (a - c) ^ n" 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    84
    by (rule Maclaurin_minus)
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    85
  show ?thesis
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    86
  proof -
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    87
    from EX obtain x where X: "a - c < x & x < 0 &
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    88
      f (a - c + c) = (SUM m = 0..<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    89
        diff n (x + c) / real (fact n) * (a - c) ^ n" ..
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    90
    let ?H = "x + c"
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    91
    from X have "a<?H & ?H<c \<and> f a = (\<Sum>m = 0..<n. diff m c / real (fact m) * (a - c) ^ m) +
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    92
      diff n ?H / real (fact n) * (a - c) ^ n"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 28952
diff changeset
    93
      by fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 28952
diff changeset
    94
    thus ?thesis by fastforce
17634
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    95
  qed
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    96
qed
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    97
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
    98
lemma taylor:
25162
ad4d5365d9d8 went back to >0
nipkow
parents: 25134
diff changeset
    99
  assumes INIT: "n>0" "diff 0 = f"
17634
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   100
  and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   101
  and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   102
  shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   103
    f x = setsum (% m. (diff m c / real (fact m)) * (x - c)^m) {0..<n} +
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   104
      (diff n t / real (fact n)) * (x - c)^n" 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   105
proof (cases "x<c")
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   106
  case True
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   107
  note INIT
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   108
  moreover from DERIV and INTERV
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   109
  have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 28952
diff changeset
   110
    by fastforce
17634
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   111
  moreover note True
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   112
  moreover from INTERV have "c \<le> b" by simp
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   113
  ultimately have EX: "\<exists>t>x. t < c \<and> f x =
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   114
    (\<Sum>m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) +
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   115
      diff n t / real (fact n) * (x - c) ^ n"
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   116
    by (rule taylor_down)
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   117
  with True show ?thesis by simp
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   118
next
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   119
  case False
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   120
  note INIT
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   121
  moreover from DERIV and INTERV
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   122
  have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 28952
diff changeset
   123
    by fastforce
17634
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   124
  moreover from INTERV have "a \<le> c" by arith
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   125
  moreover from False and INTERV have "c < x" by arith
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   126
  ultimately have EX: "\<exists>t>c. t < x \<and> f x =
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   127
    (\<Sum>m = 0..<n. diff m c / real (fact m) * (x - c) ^ m) +
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   128
      diff n t / real (fact n) * (x - c) ^ n" 
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   129
    by (rule taylor_up)
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   130
  with False show ?thesis by simp
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   131
qed
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   132
e83ce8fe58fa Formalization of Taylor series by Lukas Bulwahn and
berghofe
parents:
diff changeset
   133
end