# HG changeset patch # User immler # Date 1430844310 -7200 # Node ID 09a7481c03b111d309ffeb25fe324dfa4fef6a5b # Parent d87c8c2d49382c132af830b226b1fe3eb89f9f50 general Taylor series expansion with integral remainder diff -r d87c8c2d4938 -r 09a7481c03b1 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Tue May 05 18:45:10 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue May 05 18:45:10 2015 +0200 @@ -6887,6 +6887,121 @@ qed +subsection {* Taylor series expansion *} + +lemma + setsum_telescope: + fixes f::"nat \ 'a::ab_group_add" + shows "setsum (\i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)" + by (induct i) simp_all + +lemma (in bounded_bilinear) setsum_prod_derivatives_has_vector_derivative: + 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 g0: "Dg 0 = g" + and Dg: "\m t. m < p \ a \ t \ t \ b \ + (Dg m has_vector_derivative Dg (Suc m) t) (at t within {a .. b})" + and ivl: "a \ t" "t \ b" + shows "((\t. \iR prod (Df i t) (Dg (p - Suc i) t)) + has_vector_derivative + prod (f t) (Dg p t) - (-1)^p *\<^sub>R prod (Df p t) (g t)) + (at t within {a .. b})" + using assms +proof cases + assume p: "p \ 1" + def p' \ "p - 2" + from assms p have p': "{..i. i \ p' \ Suc (Suc p' - i) = (Suc (Suc p') - i)" + by auto + let ?f = "\i. (-1) ^ i *\<^sub>R (prod (Df i t) (Dg ((p - i)) t))" + have "(\iR (prod (Df i t) (Dg (Suc (p - Suc i)) t) + + prod (Df (Suc i) t) (Dg (p - Suc i) t))) = + (\i\(Suc p'). ?f i - ?f (Suc i))" + by (auto simp: algebra_simps p'(2) numeral_2_eq_2 * lessThan_Suc_atMost) + also note setsum_telescope + finally + have "(\iR (prod (Df i t) (Dg (Suc (p - Suc i)) t) + + prod (Df (Suc i) t) (Dg (p - Suc i) t))) + = prod (f t) (Dg p t) - (- 1) ^ p *\<^sub>R prod (Df p t) (g t)" + unfolding p'[symmetric] + by (simp add: assms) + thus ?thesis + using assms + by (auto intro!: derivative_eq_intros has_vector_derivative) +qed (auto intro!: derivative_eq_intros has_vector_derivative) + +lemma taylor_integral: + 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 - + interpret bounded_bilinear "scaleR::real\'a\'a" + by (rule bounded_bilinear_scaleR) + def g \ "\s. (b - s)^(p - 1)/fact (p - 1)" + def Dg \ "\n s. if n < p then (-1)^n * (b - s)^(p - 1 - n) / fact (p - 1 - n) else 0" + have g0: "Dg 0 = g" + using `p > 0` + by (auto simp add: Dg_def divide_simps g_def split: split_if_asm) + { + fix m + assume "p > Suc m" + hence "p - Suc m = Suc (p - Suc (Suc m))" + by auto + hence "real (p - Suc m) * fact (p - Suc (Suc m)) = fact (p - Suc m)" + by auto + } note fact_eq = this + have Dg: "\m t. m < p \ a \ t \ t \ b \ + (Dg m has_vector_derivative Dg (Suc m) t) (at t within {a .. b})" + unfolding Dg_def + by (auto intro!: derivative_eq_intros simp: has_vector_derivative_def + fact_eq real_eq_of_nat[symmetric] divide_simps) + 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 + 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) + 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)" . +qed + + subsection {* Attempt a systematic general set of "offset" results for components. *} lemma gauge_modify: