(* Title: HOL/Transcendental.thy Author: Jacques D. Fleuriot, University of Cambridge, University of Edinburgh Author: Lawrence C Paulson Author: Jeremy Avigad *) section ‹Power Series, Transcendental Functions etc.› theory Transcendental imports Series Deriv NthRoot begin text ‹A theorem about the factcorial function on the reals.› lemma square_fact_le_2_fact: "fact n * fact n ≤ (fact (2 * n) :: real)" proof (induct n) case 0 then show ?case by simp next case (Suc n) have "(fact (Suc n)) * (fact (Suc n)) = of_nat (Suc n) * of_nat (Suc n) * (fact n * fact n :: real)" by (simp add: field_simps) also have "… ≤ of_nat (Suc n) * of_nat (Suc n) * fact (2 * n)" by (rule mult_left_mono [OF Suc]) simp also have "… ≤ of_nat (Suc (Suc (2 * n))) * of_nat (Suc (2 * n)) * fact (2 * n)" by (rule mult_right_mono)+ (auto simp: field_simps) also have "… = fact (2 * Suc n)" by (simp add: field_simps) finally show ?case . qed lemma fact_in_Reals: "fact n ∈ ℝ" by (induction n) auto lemma of_real_fact [simp]: "of_real (fact n) = fact n" by (metis of_nat_fact of_real_of_nat_eq) lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)" by (simp add: pochhammer_prod) lemma norm_fact [simp]: "norm (fact n :: 'a::real_normed_algebra_1) = fact n" proof - have "(fact n :: 'a) = of_real (fact n)" by simp also have "norm … = fact n" by (subst norm_of_real) simp finally show ?thesis . qed lemma root_test_convergence: fixes f :: "nat ⇒ 'a::banach" assumes f: "(λn. root n (norm (f n))) ⇢ x" ― ‹could be weakened to lim sup› and "x < 1" shows "summable f" proof - have "0 ≤ x" by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1]) from ‹x < 1› obtain z where z: "x < z" "z < 1" by (metis dense) from f ‹x < z› have "eventually (λn. root n (norm (f n)) < z) sequentially" by (rule order_tendstoD) then have "eventually (λn. norm (f n) ≤ z^n) sequentially" using eventually_ge_at_top proof eventually_elim fix n assume less: "root n (norm (f n)) < z" and n: "1 ≤ n" from power_strict_mono[OF less, of n] n show "norm (f n) ≤ z ^ n" by simp qed then show "summable f" unfolding eventually_sequentially using z ‹0 ≤ x› by (auto intro!: summable_comparison_test[OF _ summable_geometric]) qed subsection ‹More facts about binomial coefficients› text ‹ These facts could have been proven before, but having real numbers makes the proofs a lot easier. › lemma central_binomial_odd: "odd n ⟹ n choose (Suc (n div 2)) = n choose (n div 2)" proof - assume "odd n" hence "Suc (n div 2) ≤ n" by presburger hence "n choose (Suc (n div 2)) = n choose (n - Suc (n div 2))" by (rule binomial_symmetric) also from ‹odd n› have "n - Suc (n div 2) = n div 2" by presburger finally show ?thesis . qed lemma binomial_less_binomial_Suc: assumes k: "k < n div 2" shows "n choose k < n choose (Suc k)" proof - from k have k': "k ≤ n" "Suc k ≤ n" by simp_all from k' have "real (n choose k) = fact n / (fact k * fact (n - k))" by (simp add: binomial_fact) also from k' have "n - k = Suc (n - Suc k)" by simp also from k' have "fact … = (real n - real k) * fact (n - Suc k)" by (subst fact_Suc) (simp_all add: of_nat_diff) also from k have "fact k = fact (Suc k) / (real k + 1)" by (simp add: field_simps) also have "fact n / (fact (Suc k) / (real k + 1) * ((real n - real k) * fact (n - Suc k))) = (n choose (Suc k)) * ((real k + 1) / (real n - real k))" using k by (simp add: field_split_simps binomial_fact) also from assms have "(real k + 1) / (real n - real k) < 1" by simp finally show ?thesis using k by (simp add: mult_less_cancel_left) qed lemma binomial_strict_mono: assumes "k < k'" "2*k' ≤ n" shows "n choose k < n choose k'" proof - from assms have "k ≤ k' - 1" by simp thus ?thesis proof (induction rule: inc_induct) case base with assms binomial_less_binomial_Suc[of "k' - 1" n] show ?case by simp next case (step k) from step.prems step.hyps assms have "n choose k < n choose (Suc k)" by (intro binomial_less_binomial_Suc) simp_all also have "… < n choose k'" by (rule step.IH) finally show ?case . qed qed lemma binomial_mono: assumes "k ≤ k'" "2*k' ≤ n" shows "n choose k ≤ n choose k'" using assms binomial_strict_mono[of k k' n] by (cases "k = k'") simp_all lemma binomial_strict_antimono: assumes "k < k'" "2 * k ≥ n" "k' ≤ n" shows "n choose k > n choose k'" proof - from assms have "n choose (n - k) > n choose (n - k')" by (intro binomial_strict_mono) (simp_all add: algebra_simps) with assms show ?thesis by (simp add: binomial_symmetric [symmetric]) qed lemma binomial_antimono: assumes "k ≤ k'" "k ≥ n div 2" "k' ≤ n" shows "n choose k ≥ n choose k'" proof (cases "k = k'") case False note not_eq = False show ?thesis proof (cases "k = n div 2 ∧ odd n") case False with assms(2) have "2*k ≥ n" by presburger with not_eq assms binomial_strict_antimono[of k k' n] show ?thesis by simp next case True have "n choose k' ≤ n choose (Suc (n div 2))" proof (cases "k' = Suc (n div 2)") case False with assms True not_eq have "Suc (n div 2) < k'" by simp with assms binomial_strict_antimono[of "Suc (n div 2)" k' n] True show ?thesis by auto qed simp_all also from True have "… = n choose k" by (simp add: central_binomial_odd) finally show ?thesis . qed qed simp_all lemma binomial_maximum: "n choose k ≤ n choose (n div 2)" proof - have "k ≤ n div 2 ⟷ 2*k ≤ n" by linarith consider "2*k ≤ n" | "2*k ≥ n" "k ≤ n" | "k > n" by linarith thus ?thesis proof cases case 1 thus ?thesis by (intro binomial_mono) linarith+ next case 2 thus ?thesis by (intro binomial_antimono) simp_all qed (simp_all add: binomial_eq_0) qed lemma binomial_maximum': "(2*n) choose k ≤ (2*n) choose n" using binomial_maximum[of "2*n"] by simp lemma central_binomial_lower_bound: assumes "n > 0" shows "4^n / (2*real n) ≤ real ((2*n) choose n)" proof - from binomial[of 1 1 "2*n"] have "4 ^ n = (∑k≤2*n. (2*n) choose k)" by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def) also have "{..2*n} = {0<..<2*n} ∪ {0,2*n}" by auto also have "(∑k∈…. (2*n) choose k) = (∑k∈{0<..<2*n}. (2*n) choose k) + (∑k∈{0,2*n}. (2*n) choose k)" by (subst sum.union_disjoint) auto also have "(∑k∈{0,2*n}. (2*n) choose k) ≤ (∑k≤1. (n choose k)⇧^{2})" by (cases n) simp_all also from assms have "… ≤ (∑k≤n. (n choose k)⇧^{2})" by (intro sum_mono2) auto also have "… = (2*n) choose n" by (rule choose_square_sum) also have "(∑k∈{0<..<2*n}. (2*n) choose k) ≤ (∑k∈{0<..<2*n}. (2*n) choose n)" by (intro sum_mono binomial_maximum') also have "… = card {0<..<2*n} * ((2*n) choose n)" by simp also have "card {0<..<2*n} ≤ 2*n - 1" by (cases n) simp_all also have "(2 * n - 1) * (2 * n choose n) + (2 * n choose n) = ((2*n) choose n) * (2*n)" using assms by (simp add: algebra_simps) finally have "4 ^ n ≤ (2 * n choose n) * (2 * n)" by simp_all hence "real (4 ^ n) ≤ real ((2 * n choose n) * (2 * n))" by (subst of_nat_le_iff) with assms show ?thesis by (simp add: field_simps) qed subsection ‹Properties of Power Series› lemma powser_zero [simp]: "(∑n. f n * 0 ^ n) = f 0" for f :: "nat ⇒ 'a::real_normed_algebra_1" proof - have "(∑n<1. f n * 0 ^ n) = (∑n. f n * 0 ^ n)" by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left) then show ?thesis by simp qed lemma powser_sums_zero: "(λn. a n * 0^n) sums a 0" for a :: "nat ⇒ 'a::real_normed_div_algebra" using sums_finite [of "{0}" "λn. a n * 0 ^ n"] by simp lemma powser_sums_zero_iff [simp]: "(λn. a n * 0^n) sums x ⟷ a 0 = x" for a :: "nat ⇒ 'a::real_normed_div_algebra" using powser_sums_zero sums_unique2 by blast text ‹ Power series has a circle or radius of convergence: if it sums for ‹x›, then it sums absolutely for ‹z› with \<^term>‹¦z¦ < ¦x¦›.› lemma powser_insidea: fixes x z :: "'a::real_normed_div_algebra" assumes 1: "summable (λn. f n * x^n)" and 2: "norm z < norm x" shows "summable (λn. norm (f n * z ^ n))" proof - from 2 have x_neq_0: "x ≠ 0" by clarsimp from 1 have "(λn. f n * x^n) ⇢ 0" by (rule summable_LIMSEQ_zero) then have "convergent (λn. f n * x^n)" by (rule convergentI) then have "Cauchy (λn. f n * x^n)" by (rule convergent_Cauchy) then have "Bseq (λn. f n * x^n)" by (rule Cauchy_Bseq) then obtain K where 3: "0 < K" and 4: "∀n. norm (f n * x^n) ≤ K" by (auto simp: Bseq_def) have "∃N. ∀n≥N. norm (norm (f n * z ^ n)) ≤ K * norm (z ^ n) * inverse (norm (x^n))" proof (intro exI allI impI) fix n :: nat assume "0 ≤ n" have "norm (norm (f n * z ^ n)) * norm (x^n) = norm (f n * x^n) * norm (z ^ n)" by (simp add: norm_mult abs_mult) also have "… ≤ K * norm (z ^ n)" by (simp only: mult_right_mono 4 norm_ge_zero) also have "… = K * norm (z ^ n) * (inverse (norm (x^n)) * norm (x^n))" by (simp add: x_neq_0) also have "… = K * norm (z ^ n) * inverse (norm (x^n)) * norm (x^n)" by (simp only: mult.assoc) finally show "norm (norm (f n * z ^ n)) ≤ K * norm (z ^ n) * inverse (norm (x^n))" by (simp add: mult_le_cancel_right x_neq_0) qed moreover have "summable (λn. K * norm (z ^ n) * inverse (norm (x^n)))" proof - from 2 have "norm (norm (z * inverse x)) < 1" using x_neq_0 by (simp add: norm_mult nonzero_norm_inverse divide_inverse [where 'a=real, symmetric]) then have "summable (λn. norm (z * inverse x) ^ n)" by (rule summable_geometric) then have "summable (λn. K * norm (z * inverse x) ^ n)" by (rule summable_mult) then show "summable (λn. K * norm (z ^ n) * inverse (norm (x^n)))" using x_neq_0 by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib power_inverse norm_power mult.assoc) qed ultimately show "summable (λn. norm (f n * z ^ n))" by (rule summable_comparison_test) qed lemma powser_inside: fixes f :: "nat ⇒ 'a::{real_normed_div_algebra,banach}" shows "summable (λn. f n * (x^n)) ⟹ norm z < norm x ⟹ summable (λn. f n * (z ^ n))" by (rule powser_insidea [THEN summable_norm_cancel]) lemma powser_times_n_limit_0: fixes x :: "'a::{real_normed_div_algebra,banach}" assumes "norm x < 1" shows "(λn. of_nat n * x ^ n) ⇢ 0" proof - have "norm x / (1 - norm x) ≥ 0" using assms by (auto simp: field_split_simps) moreover obtain N where N: "norm x / (1 - norm x) < of_int N" using ex_le_of_int by (meson ex_less_of_int) ultimately have N0: "N>0" by auto then have *: "real_of_int (N + 1) * norm x / real_of_int N < 1" using N assms by (auto simp: field_simps) have **: "real_of_int N * (norm x * (real_of_nat (Suc n) * norm (x ^ n))) ≤ real_of_nat n * (norm x * ((1 + N) * norm (x ^ n)))" if "N ≤ int n" for n :: nat proof - from that have "real_of_int N * real_of_nat (Suc n) ≤ real_of_nat n * real_of_int (1 + N)" by (simp add: algebra_simps) then have "(real_of_int N * real_of_nat (Suc n)) * (norm x * norm (x ^ n)) ≤ (real_of_nat n * (1 + N)) * (norm x * norm (x ^ n))" using N0 mult_mono by fastforce then show ?thesis by (simp add: algebra_simps) qed show ?thesis using * by (rule summable_LIMSEQ_zero [OF summable_ratio_test, where N1="nat N"]) (simp add: N0 norm_mult field_simps ** del: of_nat_Suc of_int_add) qed corollary lim_n_over_pown: fixes x :: "'a::{real_normed_field,banach}" shows "1 < norm x ⟹ ((λn. of_nat n / x^n) ⤏ 0) sequentially" using powser_times_n_limit_0 [of "inverse x"] by (simp add: norm_divide field_split_simps) lemma sum_split_even_odd: fixes f :: "nat ⇒ real" shows "(∑i<2 * n. if even i then f i else g i) = (∑i<n. f (2 * i)) + (∑i<n. g (2 * i + 1))" proof (induct n) case 0 then show ?case by simp next case (Suc n) have "(∑i<2 * Suc n. if even i then f i else g i) = (∑i<n. f (2 * i)) + (∑i<n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))" using Suc.hyps unfolding One_nat_def by auto also have "… = (∑i<Suc n. f (2 * i)) + (∑i<Suc n. g (2 * i + 1))" by auto finally show ?case . qed lemma sums_if': fixes g :: "nat ⇒ real" assumes "g sums x" shows "(λ n. if even n then 0 else g ((n - 1) div 2)) sums x" unfolding sums_def proof (rule LIMSEQ_I) fix r :: real assume "0 < r" from ‹g sums x›[unfolded sums_def, THEN LIMSEQ_D, OF this] obtain no where no_eq: "⋀n. n ≥ no ⟹ (norm (sum g {..<n} - x) < r)" by blast let ?SUM = "λ m. ∑i<m. if even i then 0 else g ((i - 1) div 2)" have "(norm (?SUM m - x) < r)" if "m ≥ 2 * no" for m proof - from that have "m div 2 ≥ no" by auto have sum_eq: "?SUM (2 * (m div 2)) = sum g {..< m div 2}" using sum_split_even_odd by auto then have "(norm (?SUM (2 * (m div 2)) - x) < r)" using no_eq unfolding sum_eq using ‹m div 2 ≥ no› by auto moreover have "?SUM (2 * (m div 2)) = ?SUM m" proof (cases "even m") case True then show ?thesis by (auto simp: even_two_times_div_two) next case False then have eq: "Suc (2 * (m div 2)) = m" by simp then have "even (2 * (m div 2))" using ‹odd m› by auto have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq .. also have "… = ?SUM (2 * (m div 2))" using ‹even (2 * (m div 2))› by auto finally show ?thesis by auto qed ultimately show ?thesis by auto qed then show "∃no. ∀ m ≥ no. norm (?SUM m - x) < r" by blast qed lemma sums_if: fixes g :: "nat ⇒ real" assumes "g sums x" and "f sums y" shows "(λ n. if even n then f (n div 2) else g ((n - 1) div 2)) sums (x + y)" proof - let ?s = "λ n. if even n then 0 else f ((n - 1) div 2)" have if_sum: "(if B then (0 :: real) else E) + (if B then T else 0) = (if B then T else E)" for B T E by (cases B) auto have g_sums: "(λ n. if even n then 0 else g ((n - 1) div 2)) sums x" using sums_if'[OF ‹g sums x›] . have if_eq: "⋀B T E. (if ¬ B then T else E) = (if B then E else T)" by auto have "?s sums y" using sums_if'[OF ‹f sums y›] . from this[unfolded sums_def, THEN LIMSEQ_Suc] have "(λn. if even n then f (n div 2) else 0) sums y" by (simp add: lessThan_Suc_eq_insert_0 sum.atLeast1_atMost_eq image_Suc_lessThan if_eq sums_def cong del: if_weak_cong) from sums_add[OF g_sums this] show ?thesis by (simp only: if_sum) qed subsection ‹Alternating series test / Leibniz formula› (* FIXME: generalise these results from the reals via type classes? *) lemma sums_alternating_upper_lower: fixes a :: "nat ⇒ real" assumes mono: "⋀n. a (Suc n) ≤ a n" and a_pos: "⋀n. 0 ≤ a n" and "a ⇢ 0" shows "∃l. ((∀n. (∑i<2*n. (- 1)^i*a i) ≤ l) ∧ (λ n. ∑i<2*n. (- 1)^i*a i) ⇢ l) ∧ ((∀n. l ≤ (∑i<2*n + 1. (- 1)^i*a i)) ∧ (λ n. ∑i<2*n + 1. (- 1)^i*a i) ⇢ l)" (is "∃l. ((∀n. ?f n ≤ l) ∧ _) ∧ ((∀n. l ≤ ?g n) ∧ _)") proof (rule nested_sequence_unique) have fg_diff: "⋀n. ?f n - ?g n = - a (2 * n)" by auto show "∀n. ?f n ≤ ?f (Suc n)" proof show "?f n ≤ ?f (Suc n)" for n using mono[of "2*n"] by auto qed show "∀n. ?g (Suc n) ≤ ?g n" proof show "?g (Suc n) ≤ ?g n" for n using mono[of "Suc (2*n)"] by auto qed show "∀n. ?f n ≤ ?g n" proof show "?f n ≤ ?g n" for n using fg_diff a_pos by auto qed show "(λn. ?f n - ?g n) ⇢ 0" unfolding fg_diff proof (rule LIMSEQ_I) fix r :: real assume "0 < r" with ‹a ⇢ 0›[THEN LIMSEQ_D] obtain N where "⋀ n. n ≥ N ⟹ norm (a n - 0) < r" by auto then have "∀n ≥ N. norm (- a (2 * n) - 0) < r" by auto then show "∃N. ∀n ≥ N. norm (- a (2 * n) - 0) < r" by auto qed qed lemma summable_Leibniz': fixes a :: "nat ⇒ real" assumes a_zero: "a ⇢ 0" and a_pos: "⋀n. 0 ≤ a n" and a_monotone: "⋀n. a (Suc n) ≤ a n" shows summable: "summable (λ n. (-1)^n * a n)" and "⋀n. (∑i<2*n. (-1)^i*a i) ≤ (∑i. (-1)^i*a i)" and "(λn. ∑i<2*n. (-1)^i*a i) ⇢ (∑i. (-1)^i*a i)" and "⋀n. (∑i. (-1)^i*a i) ≤ (∑i<2*n+1. (-1)^i*a i)" and "(λn. ∑i<2*n+1. (-1)^i*a i) ⇢ (∑i. (-1)^i*a i)" proof - let ?S = "λn. (-1)^n * a n" let ?P = "λn. ∑i<n. ?S i" let ?f = "λn. ?P (2 * n)" let ?g = "λn. ?P (2 * n + 1)" obtain l :: real where below_l: "∀ n. ?f n ≤ l" and "?f ⇢ l" and above_l: "∀ n. l ≤ ?g n" and "?g ⇢ l" using sums_alternating_upper_lower[OF a_monotone a_pos a_zero] by blast let ?Sa = "λm. ∑n<m. ?S n" have "?Sa ⇢ l" proof (rule LIMSEQ_I) fix r :: real assume "0 < r" with ‹?f ⇢ l›[THEN LIMSEQ_D] obtain f_no where f: "⋀n. n ≥ f_no ⟹ norm (?f n - l) < r" by auto from ‹0 < r› ‹?g ⇢ l›[THEN LIMSEQ_D] obtain g_no where g: "⋀n. n ≥ g_no ⟹ norm (?g n - l) < r" by auto have "norm (?Sa n - l) < r" if "n ≥ (max (2 * f_no) (2 * g_no))" for n proof - from that have "n ≥ 2 * f_no" and "n ≥ 2 * g_no" by auto show ?thesis proof (cases "even n") case True then have n_eq: "2 * (n div 2) = n" by (simp add: even_two_times_div_two) with ‹n ≥ 2 * f_no› have "n div 2 ≥ f_no" by auto from f[OF this] show ?thesis unfolding n_eq atLeastLessThanSuc_atLeastAtMost . next case False then have "even (n - 1)" by simp then have n_eq: "2 * ((n - 1) div 2) = n - 1" by (simp add: even_two_times_div_two) then have range_eq: "n - 1 + 1 = n" using odd_pos[OF False] by auto from n_eq ‹n ≥ 2 * g_no› have "(n - 1) div 2 ≥ g_no" by auto from g[OF this] show ?thesis by (simp only: n_eq range_eq) qed qed then show "∃no. ∀n ≥ no. norm (?Sa n - l) < r" by blast qed then have sums_l: "(λi. (-1)^i * a i) sums l" by (simp only: sums_def) then show "summable ?S" by (auto simp: summable_def) have "l = suminf ?S" by (rule sums_unique[OF sums_l]) fix n show "suminf ?S ≤ ?g n" unfolding sums_unique[OF sums_l, symmetric] using above_l by auto show "?f n ≤ suminf ?S" unfolding sums_unique[OF sums_l, symmetric] using below_l by auto show "?g ⇢ suminf ?S" using ‹?g ⇢ l› ‹l = suminf ?S› by auto show "?f ⇢ suminf ?S" using ‹?f ⇢ l› ‹l = suminf ?S› by auto qed theorem summable_Leibniz: fixes a :: "nat ⇒ real" assumes a_zero: "a ⇢ 0" and "monoseq a" shows "summable (λ n. (-1)^n * a n)" (is "?summable") and "0 < a 0 ⟶ (∀n. (∑i. (- 1)^i*a i) ∈ { ∑i<2*n. (- 1)^i * a i .. ∑i<2*n+1. (- 1)^i * a i})" (is "?pos") and "a 0 < 0 ⟶ (∀n. (∑i. (- 1)^i*a i) ∈ { ∑i<2*n+1. (- 1)^i * a i .. ∑i<2*n. (- 1)^i * a i})" (is "?neg") and "(λn. ∑i<2*n. (- 1)^i*a i) ⇢ (∑i. (- 1)^i*a i)" (is "?f") and "(λn. ∑i<2*n+1. (- 1)^i*a i) ⇢ (∑i. (- 1)^i*a i)" (is "?g") proof - have "?summable ∧ ?pos ∧ ?neg ∧ ?f ∧ ?g" proof (cases "(∀n. 0 ≤ a n) ∧ (∀m. ∀n≥m. a n ≤ a m)") case True then have ord: "⋀n m. m ≤ n ⟹ a n ≤ a m" and ge0: "⋀n. 0 ≤ a n" by auto have mono: "a (Suc n) ≤ a n" for n using ord[where n="Suc n" and m=n] by auto note leibniz = summable_Leibniz'[OF ‹a ⇢ 0› ge0] from leibniz[OF mono] show ?thesis using ‹0 ≤ a 0› by auto next let ?a = "λn. - a n" case False with monoseq_le[OF ‹monoseq a› ‹a ⇢ 0›] have "(∀ n. a n ≤ 0) ∧ (∀m. ∀n≥m. a m ≤ a n)" by auto then have ord: "⋀n m. m ≤ n ⟹ ?a n ≤ ?a m" and ge0: "⋀ n. 0 ≤ ?a n" by auto have monotone: "?a (Suc n) ≤ ?a n" for n using ord[where n="Suc n" and m=n] by auto note leibniz = summable_Leibniz'[OF _ ge0, of "λx. x", OF tendsto_minus[OF ‹a ⇢ 0›, unfolded minus_zero] monotone] have "summable (λ n. (-1)^n * ?a n)" using leibniz(1) by auto then obtain l where "(λ n. (-1)^n * ?a n) sums l" unfolding summable_def by auto from this[THEN sums_minus] have "(λ n. (-1)^n * a n) sums -l" by auto then have ?summable by (auto simp: summable_def) moreover have "¦- a - - b¦ = ¦a - b¦" for a b :: real unfolding minus_diff_minus by auto from suminf_minus[OF leibniz(1), unfolded mult_minus_right minus_minus] have move_minus: "(∑n. - ((- 1) ^ n * a n)) = - (∑n. (- 1) ^ n * a n)" by auto have ?pos using ‹0 ≤ ?a 0› by auto moreover have ?neg using leibniz(2,4) unfolding mult_minus_right sum_negf move_minus neg_le_iff_le by auto moreover have ?f and ?g using leibniz(3,5)[unfolded mult_minus_right sum_negf move_minus, THEN tendsto_minus_cancel] by auto ultimately show ?thesis by auto qed then show ?summable and ?pos and ?neg and ?f and ?g by safe qed subsection ‹Term-by-Term Differentiability of Power Series› definition diffs :: "(nat ⇒ 'a::ring_1) ⇒ nat ⇒ 'a" where "diffs c = (λn. of_nat (Suc n) * c (Suc n))" text ‹Lemma about distributing negation over it.› lemma diffs_minus: "diffs (λn. - c n) = (λn. - diffs c n)" by (simp add: diffs_def) lemma diffs_equiv: fixes x :: "'a::{real_normed_vector,ring_1}" shows "summable (λn. diffs c n * x^n) ⟹ (λn. of_nat n * c n * x^(n - Suc 0)) sums (∑n. diffs c n * x^n)" unfolding diffs_def by (simp add: summable_sums sums_Suc_imp) lemma lemma_termdiff1: fixes z :: "'a :: {monoid_mult,comm_ring}" shows "(∑p<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) = (∑p<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))" by (auto simp: algebra_simps power_add [symmetric]) lemma sumr_diff_mult_const2: "sum f {..<n} - of_nat n * r = (∑i<n. f i - r)" for r :: "'a::ring_1" by (simp add: sum_subtractf) lemma lemma_termdiff2: fixes h :: "'a::field" assumes h: "h ≠ 0" shows "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) = h * (∑p< n - Suc 0. ∑q< n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs") proof (cases n) case (Suc m) have 0: "⋀x k. (∑n<Suc k. h * (z ^ x * (z ^ (k - n) * (h + z) ^ n))) = (∑j<Suc k. h * ((h + z) ^ j * z ^ (x + k - j)))" by (auto simp add: power_add [symmetric] mult.commute intro: sum.cong) have *: "(∑i<m. z ^ i * ((z + h) ^ (m - i) - z ^ (m - i))) = (∑i<m. ∑j<m - i. h * ((z + h) ^ j * z ^ (m - Suc j)))" by (force simp add: less_iff_Suc_add sum_distrib_left diff_power_eq_sum ac_simps 0 simp del: sum.lessThan_Suc power_Suc intro: sum.cong) have "h * ?lhs = (z + h) ^ n - z ^ n - h * of_nat n * z ^ (n - Suc 0)" by (simp add: right_diff_distrib diff_divide_distrib h mult.assoc [symmetric]) also have "... = h * ((∑p<Suc m. (z + h) ^ p * z ^ (m - p)) - of_nat (Suc m) * z ^ m)" by (simp add: Suc diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc del: power_Suc sum.lessThan_Suc of_nat_Suc) also have "... = h * ((∑p<Suc m. (z + h) ^ (m - p) * z ^ p) - of_nat (Suc m) * z ^ m)" by (subst sum.nat_diff_reindex[symmetric]) simp also have "... = h * (∑i<Suc m. (z + h) ^ (m - i) * z ^ i - z ^ m)" by (simp add: sum_subtractf) also have "... = h * ?rhs" by (simp add: lemma_termdiff1 sum_distrib_left Suc *) finally have "h * ?lhs = h * ?rhs" . then show ?thesis by (simp add: h) qed auto lemma real_sum_nat_ivl_bounded2: fixes K :: "'a::linordered_semidom" assumes f: "⋀p::nat. p < n ⟹ f p ≤ K" and K: "0 ≤ K" shows "sum f {..<n-k} ≤ of_nat n * K" proof - have "sum f {..<n-k} ≤ (∑i<n - k. K)" by (rule sum_mono [OF f]) auto also have "... ≤ of_nat n * K" by (auto simp: mult_right_mono K) finally show ?thesis . qed lemma lemma_termdiff3: fixes h z :: "'a::real_normed_field" assumes 1: "h ≠ 0" and 2: "norm z ≤ K" and 3: "norm (z + h) ≤ K" shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) ≤ of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h" proof - have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) = norm (∑p<n - Suc 0. ∑q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q)) * norm h" by (metis (lifting, no_types) lemma_termdiff2 [OF 1] mult.commute norm_mult) also have "… ≤ of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h" proof (rule mult_right_mono [OF _ norm_ge_zero]) from norm_ge_zero 2 have K: "0 ≤ K" by (rule order_trans) have le_Kn: "norm ((z + h) ^ i * z ^ j) ≤ K ^ n" if "i + j = n" for i j n proof - have "norm (z + h) ^ i * norm z ^ j ≤ K ^ i * K ^ j" by (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K) also have "... = K^n" by (metis power_add that) finally show ?thesis by (simp add: norm_mult norm_power) qed then have "⋀p q. ⟦p < n; q < n - Suc 0⟧ ⟹ norm ((z + h) ^ q * z ^ (n - 2 - q)) ≤ K ^ (n - 2)" by (simp del: subst_all) then show "norm (∑p<n - Suc 0. ∑q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q)) ≤ of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))" by (intro order_trans [OF norm_sum] real_sum_nat_ivl_bounded2 mult_nonneg_nonneg of_nat_0_le_iff zero_le_power K) qed also have "… = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h" by (simp only: mult.assoc) finally show ?thesis . qed lemma lemma_termdiff4: fixes f :: "'a::real_normed_vector ⇒ 'b::real_normed_vector" and k :: real assumes k: "0 < k" and le: "⋀h. h ≠ 0 ⟹ norm h < k ⟹ norm (f h) ≤ K * norm h" shows "f ─0→ 0" proof (rule tendsto_norm_zero_cancel) show "(λh. norm (f h)) ─0→ 0" proof (rule real_tendsto_sandwich) show "eventually (λh. 0 ≤ norm (f h)) (at 0)" by simp show "eventually (λh. norm (f h) ≤ K * norm h) (at 0)" using k by (auto simp: eventually_at dist_norm le) show "(λh. 0) ─(0::'a)→ (0::real)" by (rule tendsto_const) have "(λh. K * norm h) ─(0::'a)→ K * norm (0::'a)" by (intro tendsto_intros) then show "(λh. K * norm h) ─(0::'a)→ 0" by simp qed qed lemma lemma_termdiff5: fixes g :: "'a::real_normed_vector ⇒ nat ⇒ 'b::banach" and k :: real assumes k: "0 < k" and f: "summable f" and le: "⋀h n. h ≠ 0 ⟹ norm h < k ⟹ norm (g h n) ≤ f n * norm h" shows "(λh. suminf (g h)) ─0→ 0" proof (rule lemma_termdiff4 [OF k]) fix h :: 'a assume "h ≠ 0" and "norm h < k" then have 1: "∀n. norm (g h n) ≤ f n * norm h" by (simp add: le) then have "∃N. ∀n≥N. norm (norm (g h n)) ≤ f n * norm h" by simp moreover from f have 2: "summable (λn. f n * norm h)" by (rule summable_mult2) ultimately have 3: "summable (λn. norm (g h n))" by (rule summable_comparison_test) then have "norm (suminf (g h)) ≤ (∑n. norm (g h n))" by (rule summable_norm) also from 1 3 2 have "(∑n. norm (g h n)) ≤ (∑n. f n * norm h)" by (simp add: suminf_le) also from f have "(∑n. f n * norm h) = suminf f * norm h" by (rule suminf_mult2 [symmetric]) finally show "norm (suminf (g h)) ≤ suminf f * norm h" . qed (* FIXME: Long proofs *) lemma termdiffs_aux: fixes x :: "'a::{real_normed_field,banach}" assumes 1: "summable (λn. diffs (diffs c) n * K ^ n)" and 2: "norm x < norm K" shows "(λh. ∑n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) ─0→ 0" proof - from dense [OF 2] obtain r where r1: "norm x < r" and r2: "r < norm K" by fast from norm_ge_zero r1 have r: "0 < r" by (rule order_le_less_trans) then have r_neq_0: "r ≠ 0" by simp show ?thesis proof (rule lemma_termdiff5) show "0 < r - norm x" using r1 by simp from r r2 have "norm (of_real r::'a) < norm K" by simp with 1 have "summable (λn. norm (diffs (diffs c) n * (of_real r ^ n)))" by (rule powser_insidea) then have "summable (λn. diffs (diffs (λn. norm (c n))) n * r ^ n)" using r by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc) then have "summable (λn. of_nat n * diffs (λn. norm (c n)) n * r ^ (n - Suc 0))" by (rule diffs_equiv [THEN sums_summable]) also have "(λn. of_nat n * diffs (λn. norm (c n)) n * r ^ (n - Suc 0)) = (λn. diffs (λm. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))" by (simp add: diffs_def r_neq_0 fun_eq_iff split: nat_diff_split) finally have "summable (λn. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))" by (rule diffs_equiv [THEN sums_summable]) also have "(λn. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0)) = (λn. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" by (rule ext) (simp add: r_neq_0 split: nat_diff_split) finally show "summable (λn. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" . next fix h :: 'a and n assume h: "h ≠ 0" assume "norm h < r - norm x" then have "norm x + norm h < r" by simp with norm_triangle_ineq have xh: "norm (x + h) < r" by (rule order_le_less_trans) have "norm (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)) ≤ real n * (real (n - Suc 0) * (r ^ (n - 2) * norm h))" by (metis (mono_tags, lifting) h mult.assoc lemma_termdiff3 less_eq_real_def r1 xh) then show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) ≤ norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h" by (simp only: norm_mult mult.assoc mult_left_mono [OF _ norm_ge_zero]) qed qed lemma termdiffs: fixes K x :: "'a::{real_normed_field,banach}" assumes 1: "summable (λn. c n * K ^ n)" and 2: "summable (λn. (diffs c) n * K ^ n)" and 3: "summable (λn. (diffs (diffs c)) n * K ^ n)" and 4: "norm x < norm K" shows "DERIV (λx. ∑n. c n * x^n) x :> (∑n. (diffs c) n * x^n)" unfolding DERIV_def proof (rule LIM_zero_cancel) show "(λh. (suminf (λn. c n * (x + h) ^ n) - suminf (λn. c n * x^n)) / h - suminf (λn. diffs c n * x^n)) ─0→ 0" proof (rule LIM_equal2) show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq) next fix h :: 'a assume "norm (h - 0) < norm K - norm x" then have "norm x + norm h < norm K" by simp then have 5: "norm (x + h) < norm K" by (rule norm_triangle_ineq [THEN order_le_less_trans]) have "summable (λn. c n * x^n)" and "summable (λn. c n * (x + h) ^ n)" and "summable (λn. diffs c n * x^n)" using 1 2 4 5 by (auto elim: powser_inside) then have "((∑n. c n * (x + h) ^ n) - (∑n. c n * x^n)) / h - (∑n. diffs c n * x^n) = (∑n. (c n * (x + h) ^ n - c n * x^n) / h - of_nat n * c n * x ^ (n - Suc 0))" by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums) then show "((∑n. c n * (x + h) ^ n) - (∑n. c n * x^n)) / h - (∑n. diffs c n * x^n) = (∑n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))" by (simp add: algebra_simps) next show "(λh. ∑n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) ─0→ 0" by (rule termdiffs_aux [OF 3 4]) qed qed subsection ‹The Derivative of a Power Series Has the Same Radius of Convergence› lemma termdiff_converges: fixes x :: "'a::{real_normed_field,banach}" assumes K: "norm x < K" and sm: "⋀x. norm x < K ⟹ summable(λn. c n * x ^ n)" shows "summable (λn. diffs c n * x ^ n)" proof (cases "x = 0") case True then show ?thesis using powser_sums_zero sums_summable by auto next case False then have "K > 0" using K less_trans zero_less_norm_iff by blast then obtain r :: real where r: "norm x < norm r" "norm r < K" "r > 0" using K False by (auto simp: field_simps abs_less_iff add_pos_pos intro: that [of "(norm x + K) / 2"]) have to0: "(λn. of_nat n * (x / of_real r) ^ n) ⇢ 0" using r by (simp add: norm_divide powser_times_n_limit_0 [of "x / of_real r"]) obtain N where N: "⋀n. n≥N ⟹ real_of_nat n * norm x ^ n < r ^ n" using r LIMSEQ_D [OF to0, of 1] by (auto simp: norm_divide norm_mult norm_power field_simps) have "summable (λn. (of_nat n * c n) * x ^ n)" proof (rule summable_comparison_test') show "summable (λn. norm (c n * of_real r ^ n))" apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]]) using N r norm_of_real [of "r + K", where 'a = 'a] by auto show "⋀n. N ≤ n ⟹ norm (of_nat n * c n * x ^ n) ≤ norm (c n * of_real r ^ n)" using N r by (fastforce simp add: norm_mult norm_power less_eq_real_def) qed then have "summable (λn. (of_nat (Suc n) * c(Suc n)) * x ^ Suc n)" using summable_iff_shift [of "λn. of_nat n * c n * x ^ n" 1] by simp then have "summable (λn. (of_nat (Suc n) * c(Suc n)) * x ^ n)" using False summable_mult2 [of "λn. (of_nat (Suc n) * c(Suc n) * x ^ n) * x" "inverse x"] by (simp add: mult.assoc) (auto simp: ac_simps) then show ?thesis by (simp add: diffs_def) qed lemma termdiff_converges_all: fixes x :: "'a::{real_normed_field,banach}" assumes "⋀x. summable (λn. c n * x^n)" shows "summable (λn. diffs c n * x^n)" by (rule termdiff_converges [where K = "1 + norm x"]) (use assms in auto) lemma termdiffs_strong: fixes K x :: "'a::{real_normed_field,banach}" assumes sm: "summable (λn. c n * K ^ n)" and K: "norm x < norm K" shows "DERIV (λx. ∑n. c n * x^n) x :> (∑n. diffs c n * x^n)" proof - have "norm K + norm x < norm K + norm K" using K by force then have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K" by (auto simp: norm_triangle_lt norm_divide field_simps) then have [simp]: "norm ((of_real (norm K) + of_real (norm x)) :: 'a) < norm K * 2" by simp have "summable (λn. c n * (of_real (norm x + norm K) / 2) ^ n)" by (metis K2 summable_norm_cancel [OF powser_insidea [OF sm]] add.commute of_real_add) moreover have "⋀x. norm x < norm K ⟹ summable (λn. diffs c n * x ^ n)" by (blast intro: sm termdiff_converges powser_inside) moreover have "⋀x. norm x < norm K ⟹ summable (λn. diffs(diffs c) n * x ^ n)" by (blast intro: sm termdiff_converges powser_inside) ultimately show ?thesis by (rule termdiffs [where K = "of_real (norm x + norm K) / 2"]) (use K in ‹auto simp: field_simps simp flip: of_real_add›) qed lemma termdiffs_strong_converges_everywhere: fixes K x :: "'a::{real_normed_field,banach}" assumes "⋀y. summable (λn. c n * y ^ n)" shows "((λx. ∑n. c n * x^n) has_field_derivative (∑n. diffs c n * x^n)) (at x)" using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x] by (force simp del: of_real_add) lemma termdiffs_strong': fixes z :: "'a :: {real_normed_field,banach}" assumes "⋀z. norm z < K ⟹ summable (λn. c n * z ^ n)" assumes "norm z < K" shows "((λz. ∑n. c n * z^n) has_field_derivative (∑n. diffs c n * z^n)) (at z)" proof (rule termdiffs_strong) define L :: real where "L = (norm z + K) / 2" have "0 ≤ norm z" by simp also note ‹norm z < K› finally have K: "K ≥ 0" by simp from assms K have L: "L ≥ 0" "norm z < L" "L < K" by (simp_all add: L_def) from L show "norm z < norm (of_real L :: 'a)" by simp from L show "summable (λn. c n * of_real L ^ n)" by (intro assms(1)) simp_all qed lemma termdiffs_sums_strong: fixes z :: "'a :: {banach,real_normed_field}" assumes sums: "⋀z. norm z < K ⟹ (λn. c n * z ^ n) sums f z" assumes deriv: "(f has_field_derivative f') (at z)" assumes norm: "norm z < K" shows "(λn. diffs c n * z ^ n) sums f'" proof - have summable: "summable (λn. diffs c n * z^n)" by (intro termdiff_converges[OF norm] sums_summable[OF sums]) from norm have "eventually (λz. z ∈ norm -` {..<K}) (nhds z)" by (intro eventually_nhds_in_open open_vimage) (simp_all add: continuous_on_norm) hence eq: "eventually (λz. (∑n. c n * z^n) = f z) (nhds z)" by eventually_elim (insert sums, simp add: sums_iff) have "((λz. ∑n. c n * z^n) has_field_derivative (∑n. diffs c n * z^n)) (at z)" by (intro termdiffs_strong'[OF _ norm] sums_summable[OF sums]) hence "(f has_field_derivative (∑n. diffs c n * z^n)) (at z)" by (subst (asm) DERIV_cong_ev[OF refl eq refl]) from this and deriv have "(∑n. diffs c n * z^n) = f'" by (rule DERIV_unique) with summable show ?thesis by (simp add: sums_iff) qed lemma isCont_powser: fixes K x :: "'a::{real_normed_field,banach}" assumes "summable (λn. c n * K ^ n)" assumes "norm x < norm K" shows "isCont (λx. ∑n. c n * x^n) x" using termdiffs_strong[OF assms] by (blast intro!: DERIV_isCont) lemmas isCont_powser' = isCont_o2[OF _ isCont_powser] lemma isCont_powser_converges_everywhere: fixes K x :: "'a::{real_normed_field,banach}" assumes "⋀y. summable (λn. c n * y ^ n)" shows "isCont (λx. ∑n. c n * x^n) x" using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x] by (force intro!: DERIV_isCont simp del: of_real_add) lemma powser_limit_0: fixes a :: "nat ⇒ 'a::{real_normed_field,banach}" assumes s: "0 < s" and sm: "⋀x. norm x < s ⟹ (λn. a n * x ^ n) sums (f x)" shows "(f ⤏ a 0) (at 0)" proof - have "norm (of_real s / 2 :: 'a) < s" using s by (auto simp: norm_divide) then have "summable (λn. a n * (of_real s / 2) ^ n)" by (rule sums_summable [OF sm]) then have "((λx. ∑n. a n * x ^ n) has_field_derivative (∑n. diffs a n * 0 ^ n)) (at 0)" by (rule termdiffs_strong) (use s in ‹auto simp: norm_divide›) then have "isCont (λx. ∑n. a n * x ^ n) 0" by (blast intro: DERIV_continuous) then have "((λx. ∑n. a n * x ^ n) ⤏ a 0) (at 0)" by (simp add: continuous_within) moreover have "(λx. f x - (∑n. a n * x ^ n)) ─0→ 0" apply (clarsimp simp: LIM_eq) apply (rule_tac x=s in exI) using s sm sums_unique by fastforce ultimately show ?thesis by (rule Lim_transform) qed lemma powser_limit_0_strong: fixes a :: "nat ⇒ 'a::{real_normed_field,banach}" assumes s: "0 < s" and sm: "⋀x. x ≠ 0 ⟹ norm x < s ⟹ (λn. a n * x ^ n) sums (f x)" shows "(f ⤏ a 0) (at 0)" proof - have *: "((λx. if x = 0 then a 0 else f x) ⤏ a 0) (at 0)" by (rule powser_limit_0 [OF s]) (auto simp: powser_sums_zero sm) show ?thesis using "*" by (auto cong: Lim_cong_within) qed subsection ‹Derivability of power series› lemma DERIV_series': fixes f :: "real ⇒ nat ⇒ real" assumes DERIV_f: "⋀ n. DERIV (λ x. f x n) x0 :> (f' x0 n)" and allf_summable: "⋀ x. x ∈ {a <..< b} ⟹ summable (f x)" and x0_in_I: "x0 ∈ {a <..< b}" and "summable (f' x0)" and "summable L" and L_def: "⋀n x y. x ∈ {a <..< b} ⟹ y ∈ {a <..< b} ⟹ ¦f x n - f y n¦ ≤ L n * ¦x - y¦" shows "DERIV (λ x. suminf (f x)) x0 :> (suminf (f' x0))" unfolding DERIV_def proof (rule LIM_I) fix r :: real assume "0 < r" then have "0 < r/3" by auto obtain N_L where N_L: "⋀ n. N_L ≤ n ⟹ ¦ ∑ i. L (i + n) ¦ < r/3" using suminf_exist_split[OF ‹0 < r/3› ‹summable L›] by auto obtain N_f' where N_f': "⋀ n. N_f' ≤ n ⟹ ¦ ∑ i. f' x0 (i + n) ¦ < r/3" using suminf_exist_split[OF ‹0 < r/3› ‹summable (f' x0)›] by auto let ?N = "Suc (max N_L N_f')" have "¦ ∑ i. f' x0 (i + ?N) ¦ < r/3" (is "?f'_part < r/3") and L_estimate: "¦ ∑ i. L (i + ?N) ¦ < r/3" using N_L[of "?N"] and N_f' [of "?N"] by auto let ?diff = "λi x. (f (x0 + x) i - f x0 i) / x" let ?r = "r / (3 * real ?N)" from ‹0 < r› have "0 < ?r" by simp let ?s = "λn. SOME s. 0 < s ∧ (∀ x. x ≠ 0 ∧ ¦ x ¦ < s ⟶ ¦ ?diff n x - f' x0 n ¦ < ?r)" define S' where "S' = Min (?s ` {..< ?N })" have "0 < S'" unfolding S'_def proof (rule iffD2[OF Min_gr_iff]) show "∀x ∈ (?s ` {..< ?N }). 0 < x" proof fix x assume "x ∈ ?s ` {..<?N}" then obtain n where "x = ?s n" and "n ∈ {..<?N}" using image_iff[THEN iffD1] by blast from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF ‹0 < ?r›, unfolded real_norm_def] obtain s where s_bound: "0 < s ∧ (∀x. x ≠ 0 ∧ ¦x¦ < s ⟶ ¦?diff n x - f' x0 n¦ < ?r)" by auto have "0 < ?s n" by (rule someI2[where a=s]) (auto simp: s_bound simp del: of_nat_Suc) then show "0 < x" by (simp only: ‹x = ?s n›) qed qed auto define S where "S = min (min (x0 - a) (b - x0)) S'" then have "0 < S" and S_a: "S ≤ x0 - a" and S_b: "S ≤ b - x0" and "S ≤ S'" using x0_in_I and ‹0 < S'› by auto have "¦(suminf (f (x0 + x)) - suminf (f x0)) / x - suminf (f' x0)¦ < r" if "x ≠ 0" and "¦x¦ < S" for x proof - from that have x_in_I: "x0 + x ∈ {a <..< b}" using S_a S_b by auto note diff_smbl = summable_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]] note div_smbl = summable_divide[OF diff_smbl] note all_smbl = summable_diff[OF div_smbl ‹summable (f' x0)›] note ign = summable_ignore_initial_segment[where k="?N"] note diff_shft_smbl = summable_diff[OF ign[OF allf_summable[OF x_in_I]] ign[OF allf_summable[OF x0_in_I]]] note div_shft_smbl = summable_divide[OF diff_shft_smbl] note all_shft_smbl = summable_diff[OF div_smbl ign[OF ‹summable (f' x0)›]] have 1: "¦(¦?diff (n + ?N) x¦)¦ ≤ L (n + ?N)" for n proof - have "¦?diff (n + ?N) x¦ ≤ L (n + ?N) * ¦(x0 + x) - x0¦ / ¦x¦" using divide_right_mono[OF L_def[OF x_in_I x0_in_I] abs_ge_zero] by (simp only: abs_divide) with ‹x ≠ 0› show ?thesis by auto qed note 2 = summable_rabs_comparison_test[OF _ ign[OF ‹summable L›]] from 1 have "¦ ∑ i. ?diff (i + ?N) x ¦ ≤ (∑ i. L (i + ?N))" by (metis (lifting) abs_idempotent order_trans[OF summable_rabs[OF 2] suminf_le[OF _ 2 ign[OF ‹summable L›]]]) then have "¦∑i. ?diff (i + ?N) x¦ ≤ r / 3" (is "?L_part ≤ r/3") using L_estimate by auto have "¦∑n<?N. ?diff n x - f' x0 n¦ ≤ (∑n<?N. ¦?diff n x - f' x0 n¦)" .. also have "… < (∑n<?N. ?r)" proof (rule sum_strict_mono) fix n assume "n ∈ {..< ?N}" have "¦x¦ < S" using ‹¦x¦ < S› . also have "S ≤ S'" using ‹S ≤ S'› . also have "S' ≤ ?s n" unfolding S'_def proof (rule Min_le_iff[THEN iffD2]) have "?s n ∈ (?s ` {..<?N}) ∧ ?s n ≤ ?s n" using ‹n ∈ {..< ?N}› by auto then show "∃ a ∈ (?s ` {..<?N}). a ≤ ?s n" by blast qed auto finally have "¦x¦ < ?s n" . from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF ‹0 < ?r›, unfolded real_norm_def diff_0_right, unfolded some_eq_ex[symmetric], THEN conjunct2] have "∀x. x ≠ 0 ∧ ¦x¦ < ?s n ⟶ ¦?diff n x - f' x0 n¦ < ?r" . with ‹x ≠ 0› and ‹¦x¦ < ?s n› show "¦?diff n x - f' x0 n¦ < ?r" by blast qed auto also have "… = of_nat (card {..<?N}) * ?r" by (rule sum_constant) also have "… = real ?N * ?r" by simp also have "… = r/3" by (auto simp del: of_nat_Suc) finally have "¦∑n<?N. ?diff n x - f' x0 n ¦ < r / 3" (is "?diff_part < r / 3") . from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]] have "¦(suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0)¦ = ¦∑n. ?diff n x - f' x0 n¦" unfolding suminf_diff[OF div_smbl ‹summable (f' x0)›, symmetric] using suminf_divide[OF diff_smbl, symmetric] by auto also have "… ≤ ?diff_part + ¦(∑n. ?diff (n + ?N) x) - (∑ n. f' x0 (n + ?N))¦" unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"] unfolding suminf_diff[OF div_shft_smbl ign[OF ‹summable (f' x0)›]] apply (simp only: add.commute) using abs_triangle_ineq by blast also have "… ≤ ?diff_part + ?L_part + ?f'_part" using abs_triangle_ineq4 by auto also have "… < r /3 + r/3 + r/3" using ‹?diff_part < r/3› ‹?L_part ≤ r/3› and ‹?f'_part < r/3› by (rule add_strict_mono [OF add_less_le_mono]) finally show ?thesis by auto qed then show "∃s > 0. ∀ x. x ≠ 0 ∧ norm (x - 0) < s ⟶ norm (((∑n. f (x0 + x) n) - (∑n. f x0 n)) / x - (∑n. f' x0 n)) < r" using ‹0 < S› by auto qed lemma DERIV_power_series': fixes f :: "nat ⇒ real" assumes converges: "⋀x. x ∈ {-R <..< R} ⟹ summable (λn. f n * real (Suc n) * x^n)" and x0_in_I: "x0 ∈ {-R <..< R}" and "0 < R" shows "DERIV (λx. (∑n. f n * x^(Suc n))) x0 :> (∑n. f n * real (Suc n) * x0^n)" (is "DERIV (λx. suminf (?f x)) x0 :> suminf (?f' x0)") proof - have for_subinterval: "DERIV (λx. suminf (?f x)) x0 :> suminf (?f' x0)" if "0 < R'" and "R' < R" and "-R' < x0" and "x0 < R'" for R' proof - from that have "x0 ∈ {-R' <..< R'}" and "R' ∈ {-R <..< R}" and "x0 ∈ {-R <..< R}" by auto show ?thesis proof (rule DERIV_series') show