# HG changeset patch
# User immler
# Date 1435748996 -7200
# Node ID bfb14ff434911d8e81a22042cb9201016d3bbe2a
# Parent  41e180848d021b0158442eeffabaa0ef3283ee2a
taylor series with has_integral and integrable_on

diff -r 41e180848d02 -r bfb14ff43491 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jun 30 17:02:24 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Jul 01 13:09:56 2015 +0200
@@ -6055,16 +6055,22 @@
     by (auto intro!: derivative_eq_intros has_vector_derivative)
 qed (auto intro!: derivative_eq_intros has_vector_derivative)
 
-lemma taylor_integral:
+lemma
   fixes f::"real\<Rightarrow>'a::banach"
   assumes "p>0"
   and f0: "Df 0 = f"
   and Df: "\<And>m t. m < p \<Longrightarrow> a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow>
     (Df m has_vector_derivative Df (Suc m) t) (at t within {a .. b})"
   and ivl: "a \<le> b"
-  shows "f b = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a) +
-    integral {a..b} (\<lambda>x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x)"
-proof -
+  defines "i \<equiv> \<lambda>x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x"
+  shows taylor_has_integral:
+    "(i has_integral f b - (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a)) {a..b}"
+  and taylor_integral:
+    "f b = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a) + integral {a..b} i"
+  and taylor_integrable:
+    "i integrable_on {a .. b}"
+proof goals
+  case 1
   interpret bounded_bilinear "scaleR::real\<Rightarrow>'a\<Rightarrow>'a"
     by (rule bounded_bilinear_scaleR)
   def g \<equiv> "\<lambda>s. (b - s)^(p - 1)/fact (p - 1)"
@@ -6085,29 +6091,26 @@
     unfolding Dg_def
     by (auto intro!: derivative_eq_intros simp: has_vector_derivative_def
       fact_eq real_eq_of_nat[symmetric] divide_simps)
+  let ?sum = "\<lambda>t. \<Sum>i<p. (- 1) ^ i *\<^sub>R Dg i t *\<^sub>R Df (p - Suc i) t"
   from setsum_prod_derivatives_has_vector_derivative[of _ Dg _ _ _ Df,
       OF \<open>p > 0\<close> g0 Dg f0 Df]
   have deriv: "\<And>t. a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow>
-    ((\<lambda>t. \<Sum>i<p. (- 1) ^ i *\<^sub>R Dg i t *\<^sub>R Df (p - Suc i) t) has_vector_derivative
+    (?sum has_vector_derivative
       g t *\<^sub>R Df p t - (- 1) ^ p *\<^sub>R Dg p t *\<^sub>R f t) (at t within {a..b})"
     by auto
   from fundamental_theorem_of_calculus[rule_format, OF \<open>a \<le> b\<close> deriv]
-  have ftc: "integral {a..b} (\<lambda>x. g x *\<^sub>R Df p x - (- 1) ^ p *\<^sub>R Dg p x *\<^sub>R f x) =
-    (\<Sum>i<p. (- 1) ^ i *\<^sub>R Dg i b *\<^sub>R Df (p - Suc i) b) -
-    (\<Sum>i<p. (- 1) ^ i *\<^sub>R Dg i a *\<^sub>R Df (p - Suc i) a)"
-    unfolding atLeastAtMost_iff by (auto dest!: integral_unique)
-  def p' \<equiv> "p - 1"
-  have p': "p = Suc p'" using \<open>p > 0\<close> by (simp add: p'_def)
-  have Dgp': "Dg p' = (\<lambda>_. (- 1) ^ p')"
-    by (auto simp: Dg_def p')
-  have one: "\<And>p'. (- 1::real) ^ p' * (- 1) ^ p' = 1"
-    "\<And>p' k. (- 1::real) ^ p' * ((- 1) ^ p' * k) = k"
-    by (simp_all add: power_mult_distrib[symmetric] )
-  from ftc
-  have "f b =
-    (\<Sum>i<p. ((b - a) ^ (p' - i) / fact (p' - i)) *\<^sub>R Df (p' - i) a) +
-     integral {a..b} (\<lambda>x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x)"
-    by (simp add: p' assms Dgp' one Dg_def g_def zero_power)
+  have "(i has_integral ?sum b - ?sum a) {a .. b}"
+    by (simp add: i_def g_def Dg_def)
+  also
+  have one: "(- 1) ^ p' * (- 1) ^ p' = (1::real)"
+    and "{..<p} \<inter> {i. p = Suc i} = {p - 1}"
+    for p'
+    using `p > 0`
+    by (auto simp: power_mult_distrib[symmetric])
+  then have "?sum b = f b"
+    using Suc_pred'[OF `p > 0`]
+    by (simp add: diff_eq_eq Dg_def power_0_left le_Suc_eq if_distrib
+        cond_application_beta setsum.If_cases f0)
   also
   have "{..<p} = (\<lambda>x. p - x - 1) ` {..<p}"
   proof safe
@@ -6116,11 +6119,12 @@
     thus "x \<in> (\<lambda>x. p - x - 1) ` {..<p}"
       by (auto intro!: image_eqI[where x = "p - x - 1"])
   qed simp
-  from _ this have "(\<Sum>i<p. ((b - a) ^ (p' - i) / fact (p' - i)) *\<^sub>R Df (p' - i) a) =
-    (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a)"
-    by (rule setsum.reindex_cong) (auto simp add: p' inj_on_def)
-  finally show "f b = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a) +
-    integral {a..b} (\<lambda>x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x)" .
+  from _ this
+  have "?sum a = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a)"
+    by (rule setsum.reindex_cong) (auto simp add: inj_on_def Dg_def one)
+  finally show c: ?case .
+  case 2 show ?case using c integral_unique by force
+  case 3 show ?case using c by force
 qed