# 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\'a::banach" assumes "p>0" and f0: "Df 0 = f" and Df: "\m t. m < p \ a \ t \ t \ b \ (Df m has_vector_derivative Df (Suc m) t) (at t within {a .. b})" and ivl: "a \ b" - shows "f b = (\iR Df i a) + - integral {a..b} (\x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x)" -proof - + defines "i \ \x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x" + shows taylor_has_integral: + "(i has_integral f b - (\iR Df i a)) {a..b}" + and taylor_integral: + "f b = (\iR Df i a) + integral {a..b} i" + and taylor_integrable: + "i integrable_on {a .. b}" +proof goals + case 1 interpret bounded_bilinear "scaleR::real\'a\'a" by (rule bounded_bilinear_scaleR) def g \ "\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 = "\t. \iR Dg i t *\<^sub>R Df (p - Suc i) t" from setsum_prod_derivatives_has_vector_derivative[of _ Dg _ _ _ Df, OF \p > 0\ g0 Dg f0 Df] have deriv: "\t. a \ t \ t \ b \ - ((\t. \iR 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 \a \ b\ deriv] - have ftc: "integral {a..b} (\x. g x *\<^sub>R Df p x - (- 1) ^ p *\<^sub>R Dg p x *\<^sub>R f x) = - (\iR Dg i b *\<^sub>R Df (p - Suc i) b) - - (\iR Dg i a *\<^sub>R Df (p - Suc i) a)" - unfolding atLeastAtMost_iff by (auto dest!: integral_unique) - def p' \ "p - 1" - have p': "p = Suc p'" using \p > 0\ by (simp add: p'_def) - have Dgp': "Dg p' = (\_. (- 1) ^ p')" - by (auto simp: Dg_def p') - have one: "\p'. (- 1::real) ^ p' * (- 1) ^ p' = 1" - "\p' k. (- 1::real) ^ p' * ((- 1) ^ p' * k) = k" - by (simp_all add: power_mult_distrib[symmetric] ) - from ftc - have "f b = - (\iR Df (p' - i) a) + - integral {a..b} (\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 "{.. {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 "{..x. p - x - 1) ` {.. (\x. p - x - 1) ` {..iR Df (p' - i) a) = - (\iR Df i a)" - by (rule setsum.reindex_cong) (auto simp add: p' inj_on_def) - finally show "f b = (\iR Df i a) + - integral {a..b} (\x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x)" . + from _ this + have "?sum a = (\iR 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