# Theory Series

Up to index of Isabelle/HOL

theory Series
imports Deriv
`(*  Title       : Series.thy    Author      : Jacques D. Fleuriot    Copyright   : 1998  University of CambridgeConverted to Isar and polished by lcpConverted to setsum and polished yet more by TNNAdditional contributions by Jeremy Avigad*)header{*Finite Summation and Infinite Series*}theory Seriesimports SEQ Derivbegindefinition   sums  :: "(nat => 'a::{topological_space, comm_monoid_add}) => 'a => bool"     (infixr "sums" 80) where   "f sums s = (%n. setsum f {0..<n}) ----> s"definition   summable :: "(nat => 'a::{topological_space, comm_monoid_add}) => bool" where   "summable f = (∃s. f sums s)"definition   suminf   :: "(nat => 'a::{topological_space, comm_monoid_add}) => 'a" where   "suminf f = (THE s. f sums s)"notation suminf (binder "∑" 10)lemma [trans]: "f=g ==> g sums z ==> f sums z"  by simplemma sumr_diff_mult_const: "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"by (simp add: diff_minus setsum_addf real_of_nat_def)lemma real_setsum_nat_ivl_bounded:     "(!!p. p < n ==> f(p) ≤ K)      ==> setsum f {0..<n::nat} ≤ real n * K"using setsum_bounded[where A = "{0..<n}"]by (auto simp:real_of_nat_def)(* Generalize from real to some algebraic structure? *)lemma sumr_minus_one_realpow_zero [simp]:  "(∑i=0..<2*n. (-1) ^ Suc i) = (0::real)"by (induct "n", auto)(* FIXME this is an awful lemma! *)lemma sumr_one_lb_realpow_zero [simp]:  "(∑n=Suc 0..<n. f(n) * (0::real) ^ n) = 0"by (rule setsum_0', simp)lemma sumr_group:     "(∑m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}"apply (subgoal_tac "k = 0 | 0 < k", auto)apply (induct "n")apply (simp_all add: setsum_add_nat_ivl add_commute)donelemma sumr_offset3:  "setsum f {0::nat..<n+k} = (∑m=0..<n. f (m+k)) + setsum f {0..<k}"apply (subst setsum_shift_bounds_nat_ivl [symmetric])apply (simp add: setsum_add_nat_ivl add_commute)donelemma sumr_offset:  fixes f :: "nat => 'a::ab_group_add"  shows "(∑m=0..<n. f(m+k)) = setsum f {0..<n+k} - setsum f {0..<k}"by (simp add: sumr_offset3)lemma sumr_offset2: "∀f. (∑m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"by (simp add: sumr_offset)lemma sumr_offset4:  "∀n f. setsum f {0::nat..<n+k} = (∑m=0..<n. f (m+k)::real) + setsum f {0..<k}"by (clarify, rule sumr_offset3)subsection{* Infinite Sums, by the Properties of Limits*}(*----------------------   suminf is the sum ---------------------*)lemma sums_summable: "f sums l ==> summable f"  by (simp add: sums_def summable_def, blast)lemma summable_sums:  fixes f :: "nat => 'a::{t2_space, comm_monoid_add}"  assumes "summable f"  shows "f sums (suminf f)"proof -  from assms obtain s where s: "(λn. setsum f {0..<n}) ----> s"    unfolding summable_def sums_def [abs_def] ..  then show ?thesis unfolding sums_def [abs_def] suminf_def    by (rule theI, auto intro!: tendsto_unique[OF trivial_limit_sequentially])qedlemma summable_sumr_LIMSEQ_suminf:  fixes f :: "nat => 'a::{t2_space, comm_monoid_add}"  shows "summable f ==> (λn. setsum f {0..<n}) ----> suminf f"by (rule summable_sums [unfolded sums_def])lemma suminf_eq_lim: "suminf f = lim (%n. setsum f {0..<n})"  by (simp add: suminf_def sums_def lim_def)(*-------------------    sum is unique ------------------*)lemma sums_unique:  fixes f :: "nat => 'a::{t2_space, comm_monoid_add}"  shows "f sums s ==> (s = suminf f)"apply (frule sums_summable[THEN summable_sums])apply (auto intro!: tendsto_unique[OF trivial_limit_sequentially] simp add: sums_def)donelemma sums_iff:  fixes f :: "nat => 'a::{t2_space, comm_monoid_add}"  shows "f sums x <-> summable f ∧ (suminf f = x)"  by (metis summable_sums sums_summable sums_unique)lemma sums_finite:  assumes [simp]: "finite N"  assumes f: "!!n. n ∉ N ==> f n = 0"  shows "f sums (∑n∈N. f n)"proof -  { fix n    have "setsum f {..<n + Suc (Max N)} = setsum f N"    proof cases      assume "N = {}"      with f have "f = (λx. 0)" by auto      then show ?thesis by simp    next      assume [simp]: "N ≠ {}"      show ?thesis      proof (safe intro!: setsum_mono_zero_right f)        fix i assume "i ∈ N"        then have "i ≤ Max N" by simp        then show "i < n + Suc (Max N)" by simp      qed    qed }  note eq = this  show ?thesis unfolding sums_def    by (rule LIMSEQ_offset[of _ "Suc (Max N)"])       (simp add: eq atLeast0LessThan tendsto_const del: add_Suc_right)qedlemma suminf_finite:  fixes f :: "nat => 'a::{comm_monoid_add,t2_space}"  assumes N: "finite N" and f: "!!n. n ∉ N ==> f n = 0"  shows "suminf f = (∑n∈N. f n)"  using sums_finite[OF assms, THEN sums_unique] by simplemma sums_If_finite_set:  "finite A ==> (λr. if r ∈ A then f r else 0 :: 'a::{comm_monoid_add,t2_space}) sums (∑r∈A. f r)"  using sums_finite[of A "(λr. if r ∈ A then f r else 0)"] by simplemma sums_If_finite:  "finite {r. P r} ==> (λr. if P r then f r else 0 :: 'a::{comm_monoid_add,t2_space}) sums (∑r | P r. f r)"  using sums_If_finite_set[of "{r. P r}" f] by simplemma sums_single:  "(λr. if r = i then f r else 0::'a::{comm_monoid_add,t2_space}) sums f i"  using sums_If_finite[of "λr. r = i" f] by simplemma sums_split_initial_segment:  fixes f :: "nat => 'a::real_normed_vector"  shows "f sums s ==> (λn. f(n + k)) sums (s - (SUM i = 0..< k. f i))"  apply (unfold sums_def)  apply (simp add: sumr_offset)  apply (rule tendsto_diff [OF _ tendsto_const])  apply (rule LIMSEQ_ignore_initial_segment)  apply assumptiondonelemma summable_ignore_initial_segment:  fixes f :: "nat => 'a::real_normed_vector"  shows "summable f ==> summable (%n. f(n + k))"  apply (unfold summable_def)  apply (auto intro: sums_split_initial_segment)donelemma suminf_minus_initial_segment:  fixes f :: "nat => 'a::real_normed_vector"  shows "summable f ==>    suminf f = s ==> suminf (%n. f(n + k)) = s - (SUM i = 0..< k. f i)"  apply (frule summable_ignore_initial_segment)  apply (rule sums_unique [THEN sym])  apply (frule summable_sums)  apply (rule sums_split_initial_segment)  apply autodonelemma suminf_split_initial_segment:  fixes f :: "nat => 'a::real_normed_vector"  shows "summable f ==>    suminf f = (SUM i = 0..< k. f i) + (∑n. f(n + k))"by (auto simp add: suminf_minus_initial_segment)lemma suminf_exist_split: fixes r :: real assumes "0 < r" and "summable a"  shows "∃ N. ∀ n ≥ N. ¦ ∑ i. a (i + n) ¦ < r"proof -  from LIMSEQ_D[OF summable_sumr_LIMSEQ_suminf[OF `summable a`] `0 < r`]  obtain N :: nat where "∀ n ≥ N. norm (setsum a {0..<n} - suminf a) < r" by auto  thus ?thesis unfolding suminf_minus_initial_segment[OF `summable a` refl] abs_minus_commute real_norm_def    by autoqedlemma sums_Suc:  fixes f :: "nat => 'a::real_normed_vector"  assumes sumSuc: "(λ n. f (Suc n)) sums l" shows "f sums (l + f 0)"proof -  from sumSuc[unfolded sums_def]  have "(λi. ∑n = Suc 0..<Suc i. f n) ----> l" unfolding setsum_reindex[OF inj_Suc] image_Suc_atLeastLessThan[symmetric] comp_def .  from tendsto_add[OF this tendsto_const, where b="f 0"]  have "(λi. ∑n = 0..<Suc i. f n) ----> l + f 0" unfolding add_commute setsum_head_upt_Suc[OF zero_less_Suc] .  thus ?thesis unfolding sums_def by (rule LIMSEQ_imp_Suc)qedlemma series_zero:  fixes f :: "nat => 'a::{t2_space, comm_monoid_add}"  assumes "∀m. n ≤ m --> f m = 0"  shows "f sums (setsum f {0..<n})"proof -  { fix k :: nat have "setsum f {0..<k + n} = setsum f {0..<n}"      using assms by (induct k) auto }  note setsum_const = this  show ?thesis    unfolding sums_def    apply (rule LIMSEQ_offset[of _ n])    unfolding setsum_const    apply (rule tendsto_const)    doneqedlemma sums_zero[simp, intro]: "(λn. 0) sums 0"  unfolding sums_def by (simp add: tendsto_const)lemma summable_zero[simp, intro]: "summable (λn. 0)"by (rule sums_zero [THEN sums_summable])lemma suminf_zero[simp]: "suminf (λn. 0::'a::{t2_space, comm_monoid_add}) = 0"by (rule sums_zero [THEN sums_unique, symmetric])lemma (in bounded_linear) sums:  "(λn. X n) sums a ==> (λn. f (X n)) sums (f a)"  unfolding sums_def by (drule tendsto, simp only: setsum)lemma (in bounded_linear) summable:  "summable (λn. X n) ==> summable (λn. f (X n))"unfolding summable_def by (auto intro: sums)lemma (in bounded_linear) suminf:  "summable (λn. X n) ==> f (∑n. X n) = (∑n. f (X n))"by (intro sums_unique sums summable_sums)lemmas sums_of_real = bounded_linear.sums [OF bounded_linear_of_real]lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]lemma sums_mult:  fixes c :: "'a::real_normed_algebra"  shows "f sums a ==> (λn. c * f n) sums (c * a)"  by (rule bounded_linear.sums [OF bounded_linear_mult_right])lemma summable_mult:  fixes c :: "'a::real_normed_algebra"  shows "summable f ==> summable (%n. c * f n)"  by (rule bounded_linear.summable [OF bounded_linear_mult_right])lemma suminf_mult:  fixes c :: "'a::real_normed_algebra"  shows "summable f ==> suminf (λn. c * f n) = c * suminf f"  by (rule bounded_linear.suminf [OF bounded_linear_mult_right, symmetric])lemma sums_mult2:  fixes c :: "'a::real_normed_algebra"  shows "f sums a ==> (λn. f n * c) sums (a * c)"  by (rule bounded_linear.sums [OF bounded_linear_mult_left])lemma summable_mult2:  fixes c :: "'a::real_normed_algebra"  shows "summable f ==> summable (λn. f n * c)"  by (rule bounded_linear.summable [OF bounded_linear_mult_left])lemma suminf_mult2:  fixes c :: "'a::real_normed_algebra"  shows "summable f ==> suminf f * c = (∑n. f n * c)"  by (rule bounded_linear.suminf [OF bounded_linear_mult_left])lemma sums_divide:  fixes c :: "'a::real_normed_field"  shows "f sums a ==> (λn. f n / c) sums (a / c)"  by (rule bounded_linear.sums [OF bounded_linear_divide])lemma summable_divide:  fixes c :: "'a::real_normed_field"  shows "summable f ==> summable (λn. f n / c)"  by (rule bounded_linear.summable [OF bounded_linear_divide])lemma suminf_divide:  fixes c :: "'a::real_normed_field"  shows "summable f ==> suminf (λn. f n / c) = suminf f / c"  by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric])lemma sums_add:  fixes a b :: "'a::real_normed_field"  shows "[|X sums a; Y sums b|] ==> (λn. X n + Y n) sums (a + b)"  unfolding sums_def by (simp add: setsum_addf tendsto_add)lemma summable_add:  fixes X Y :: "nat => 'a::real_normed_field"  shows "[|summable X; summable Y|] ==> summable (λn. X n + Y n)"unfolding summable_def by (auto intro: sums_add)lemma suminf_add:  fixes X Y :: "nat => 'a::real_normed_field"  shows "[|summable X; summable Y|] ==> suminf X + suminf Y = (∑n. X n + Y n)"by (intro sums_unique sums_add summable_sums)lemma sums_diff:  fixes X Y :: "nat => 'a::real_normed_field"  shows "[|X sums a; Y sums b|] ==> (λn. X n - Y n) sums (a - b)"  unfolding sums_def by (simp add: setsum_subtractf tendsto_diff)lemma summable_diff:  fixes X Y :: "nat => 'a::real_normed_field"  shows "[|summable X; summable Y|] ==> summable (λn. X n - Y n)"unfolding summable_def by (auto intro: sums_diff)lemma suminf_diff:  fixes X Y :: "nat => 'a::real_normed_field"  shows "[|summable X; summable Y|] ==> suminf X - suminf Y = (∑n. X n - Y n)"by (intro sums_unique sums_diff summable_sums)lemma sums_minus:  fixes X :: "nat => 'a::real_normed_field"  shows "X sums a ==> (λn. - X n) sums (- a)"  unfolding sums_def by (simp add: setsum_negf tendsto_minus)lemma summable_minus:  fixes X :: "nat => 'a::real_normed_field"  shows "summable X ==> summable (λn. - X n)"unfolding summable_def by (auto intro: sums_minus)lemma suminf_minus:  fixes X :: "nat => 'a::real_normed_field"  shows "summable X ==> (∑n. - X n) = - (∑n. X n)"by (intro sums_unique [symmetric] sums_minus summable_sums)lemma sums_group:  fixes f :: "nat => 'a::real_normed_field"  shows "[|f sums s; 0 < k|] ==> (λn. setsum f {n*k..<n*k+k}) sums s"apply (simp only: sums_def sumr_group)apply (unfold LIMSEQ_iff, safe)apply (drule_tac x="r" in spec, safe)apply (rule_tac x="no" in exI, safe)apply (drule_tac x="n*k" in spec)apply (erule mp)apply (erule order_trans)apply simpdonetext{*A summable series of positive terms has limit that is at least asgreat as any partial sum.*}lemma pos_summable:  fixes f:: "nat => real"  assumes pos: "!!n. 0 ≤ f n" and le: "!!n. setsum f {0..<n} ≤ x"  shows "summable f"proof -  have "convergent (λn. setsum f {0..<n})"    proof (rule Bseq_mono_convergent)      show "Bseq (λn. setsum f {0..<n})"        by (rule f_inc_g_dec_Beq_f [of "(λn. setsum f {0..<n})" "λn. x"])           (auto simp add: le pos)    next      show "∀m n. m ≤ n --> setsum f {0..<m} ≤ setsum f {0..<n}"        by (auto intro: setsum_mono2 pos)    qed  then obtain L where "(%n. setsum f {0..<n}) ----> L"    by (blast dest: convergentD)  thus ?thesis    by (force simp add: summable_def sums_def)qedlemma series_pos_le:  fixes f :: "nat => real"  shows "[|summable f; ∀m≥n. 0 ≤ f m|] ==> setsum f {0..<n} ≤ suminf f"apply (drule summable_sums)apply (simp add: sums_def)apply (cut_tac k = "setsum f {0..<n}" in tendsto_const)apply (erule LIMSEQ_le, blast)apply (rule_tac x="n" in exI, clarify)apply (rule setsum_mono2)apply autodonelemma series_pos_less:  fixes f :: "nat => real"  shows "[|summable f; ∀m≥n. 0 < f m|] ==> setsum f {0..<n} < suminf f"apply (rule_tac y="setsum f {0..<Suc n}" in order_less_le_trans)apply simpapply (erule series_pos_le)apply (simp add: order_less_imp_le)donelemma suminf_gt_zero:  fixes f :: "nat => real"  shows "[|summable f; ∀n. 0 < f n|] ==> 0 < suminf f"by (drule_tac n="0" in series_pos_less, simp_all)lemma suminf_ge_zero:  fixes f :: "nat => real"  shows "[|summable f; ∀n. 0 ≤ f n|] ==> 0 ≤ suminf f"by (drule_tac n="0" in series_pos_le, simp_all)lemma sumr_pos_lt_pair:  fixes f :: "nat => real"  shows "[|summable f;        ∀d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))|]      ==> setsum f {0..<k} < suminf f"unfolding One_nat_defapply (subst suminf_split_initial_segment [where k="k"])apply assumptionapply simpapply (drule_tac k="k" in summable_ignore_initial_segment)apply (drule_tac k="Suc (Suc 0)" in sums_group [OF summable_sums], simp)apply simpapply (frule sums_unique)apply (drule sums_summable)apply simpapply (erule suminf_gt_zero)apply (simp add: add_ac)donetext{*Sum of a geometric progression.*}lemmas sumr_geometric = geometric_sum [where 'a = real]lemma geometric_sums:  fixes x :: "'a::{real_normed_field}"  shows "norm x < 1 ==> (λn. x ^ n) sums (1 / (1 - x))"proof -  assume less_1: "norm x < 1"  hence neq_1: "x ≠ 1" by auto  hence neq_0: "x - 1 ≠ 0" by simp  from less_1 have lim_0: "(λn. x ^ n) ----> 0"    by (rule LIMSEQ_power_zero)  hence "(λn. x ^ n / (x - 1) - 1 / (x - 1)) ----> 0 / (x - 1) - 1 / (x - 1)"    using neq_0 by (intro tendsto_intros)  hence "(λn. (x ^ n - 1) / (x - 1)) ----> 1 / (1 - x)"    by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib)  thus "(λn. x ^ n) sums (1 / (1 - x))"    by (simp add: sums_def geometric_sum neq_1)qedlemma summable_geometric:  fixes x :: "'a::{real_normed_field}"  shows "norm x < 1 ==> summable (λn. x ^ n)"by (rule geometric_sums [THEN sums_summable])lemma half: "0 < 1 / (2::'a::linordered_field)"  by simplemma power_half_series: "(λn. (1/2::real)^Suc n) sums 1"proof -  have 2: "(λn. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]    by auto  have "(λn. (1/2::real)^Suc n) = (λn. (1 / 2) ^ n / 2)"    by simp  thus ?thesis using sums_divide [OF 2, of 2]    by simpqedtext{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}lemma summable_convergent_sumr_iff: "summable f = convergent (%n. setsum f {0..<n})"by (simp add: summable_def sums_def convergent_def)lemma summable_LIMSEQ_zero:  fixes f :: "nat => 'a::real_normed_vector"  shows "summable f ==> f ----> 0"apply (drule summable_convergent_sumr_iff [THEN iffD1])apply (drule convergent_Cauchy)apply (simp only: Cauchy_iff LIMSEQ_iff, safe)apply (drule_tac x="r" in spec, safe)apply (rule_tac x="M" in exI, safe)apply (drule_tac x="Suc n" in spec, simp)apply (drule_tac x="n" in spec, simp)donelemma suminf_le:  fixes x :: real  shows "summable f ==> (!!n. setsum f {0..<n} ≤ x) ==> suminf f ≤ x"  by (simp add: summable_convergent_sumr_iff suminf_eq_lim lim_le)lemma summable_Cauchy:     "summable (f::nat => 'a::banach) =      (∀e > 0. ∃N. ∀m ≥ N. ∀n. norm (setsum f {m..<n}) < e)"apply (simp only: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_iff, safe)apply (drule spec, drule (1) mp)apply (erule exE, rule_tac x="M" in exI, clarify)apply (rule_tac x="m" and y="n" in linorder_le_cases)apply (frule (1) order_trans)apply (drule_tac x="n" in spec, drule (1) mp)apply (drule_tac x="m" in spec, drule (1) mp)apply (simp add: setsum_diff [symmetric])apply simpapply (drule spec, drule (1) mp)apply (erule exE, rule_tac x="N" in exI, clarify)apply (rule_tac x="m" and y="n" in linorder_le_cases)apply (subst norm_minus_commute)apply (simp add: setsum_diff [symmetric])apply (simp add: setsum_diff [symmetric])donetext{*Comparison test*}lemma norm_setsum:  fixes f :: "'a => 'b::real_normed_vector"  shows "norm (setsum f A) ≤ (∑i∈A. norm (f i))"apply (case_tac "finite A")apply (erule finite_induct)apply simpapply simpapply (erule order_trans [OF norm_triangle_ineq add_left_mono])apply simpdonelemma summable_comparison_test:  fixes f :: "nat => 'a::banach"  shows "[|∃N. ∀n≥N. norm (f n) ≤ g n; summable g|] ==> summable f"apply (simp add: summable_Cauchy, safe)apply (drule_tac x="e" in spec, safe)apply (rule_tac x = "N + Na" in exI, safe)apply (rotate_tac 2)apply (drule_tac x = m in spec)apply (auto, rotate_tac 2, drule_tac x = n in spec)apply (rule_tac y = "∑k=m..<n. norm (f k)" in order_le_less_trans)apply (rule norm_setsum)apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans)apply (auto intro: setsum_mono simp add: abs_less_iff)donelemma summable_norm_comparison_test:  fixes f :: "nat => 'a::banach"  shows "[|∃N. ∀n≥N. norm (f n) ≤ g n; summable g|]         ==> summable (λn. norm (f n))"apply (rule summable_comparison_test)apply (auto)donelemma summable_rabs_comparison_test:  fixes f :: "nat => real"  shows "[|∃N. ∀n≥N. ¦f n¦ ≤ g n; summable g|] ==> summable (λn. ¦f n¦)"apply (rule summable_comparison_test)apply (auto)donetext{*Summability of geometric series for real algebras*}lemma complete_algebra_summable_geometric:  fixes x :: "'a::{real_normed_algebra_1,banach}"  shows "norm x < 1 ==> summable (λn. x ^ n)"proof (rule summable_comparison_test)  show "∃N. ∀n≥N. norm (x ^ n) ≤ norm x ^ n"    by (simp add: norm_power_ineq)  show "norm x < 1 ==> summable (λn. norm x ^ n)"    by (simp add: summable_geometric)qedtext{*Limit comparison property for series (c.f. jrh)*}lemma summable_le:  fixes f g :: "nat => real"  shows "[|∀n. f n ≤ g n; summable f; summable g|] ==> suminf f ≤ suminf g"apply (drule summable_sums)+apply (simp only: sums_def, erule (1) LIMSEQ_le)apply (rule exI)apply (auto intro!: setsum_mono)donelemma summable_le2:  fixes f g :: "nat => real"  shows "[|∀n. ¦f n¦ ≤ g n; summable g|] ==> summable f ∧ suminf f ≤ suminf g"apply (subgoal_tac "summable f")apply (auto intro!: summable_le)apply (simp add: abs_le_iff)apply (rule_tac g="g" in summable_comparison_test, simp_all)done(* specialisation for the common 0 case *)lemma suminf_0_le:  fixes f::"nat=>real"  assumes gt0: "∀n. 0 ≤ f n" and sm: "summable f"  shows "0 ≤ suminf f"proof -  let ?g = "(λn. (0::real))"  from gt0 have "∀n. ?g n ≤ f n" by simp  moreover have "summable ?g" by (rule summable_zero)  moreover from sm have "summable f" .  ultimately have "suminf ?g ≤ suminf f" by (rule summable_le)  then show "0 ≤ suminf f" by simpqedtext{*Absolute convergence imples normal convergence*}lemma summable_norm_cancel:  fixes f :: "nat => 'a::banach"  shows "summable (λn. norm (f n)) ==> summable f"apply (simp only: summable_Cauchy, safe)apply (drule_tac x="e" in spec, safe)apply (rule_tac x="N" in exI, safe)apply (drule_tac x="m" in spec, safe)apply (rule order_le_less_trans [OF norm_setsum])apply (rule order_le_less_trans [OF abs_ge_self])apply simpdonelemma summable_rabs_cancel:  fixes f :: "nat => real"  shows "summable (λn. ¦f n¦) ==> summable f"by (rule summable_norm_cancel, simp)text{*Absolute convergence of series*}lemma summable_norm:  fixes f :: "nat => 'a::banach"  shows "summable (λn. norm (f n)) ==> norm (suminf f) ≤ (∑n. norm (f n))"  by (auto intro: LIMSEQ_le tendsto_norm summable_norm_cancel                summable_sumr_LIMSEQ_suminf norm_setsum)lemma summable_rabs:  fixes f :: "nat => real"  shows "summable (λn. ¦f n¦) ==> ¦suminf f¦ ≤ (∑n. ¦f n¦)"by (fold real_norm_def, rule summable_norm)subsection{* The Ratio Test*}lemma norm_ratiotest_lemma:  fixes x y :: "'a::real_normed_vector"  shows "[|c ≤ 0; norm x ≤ c * norm y|] ==> x = 0"apply (subgoal_tac "norm x ≤ 0", simp)apply (erule order_trans)apply (simp add: mult_le_0_iff)donelemma rabs_ratiotest_lemma: "[| c ≤ 0; abs x ≤ c * abs y |] ==> x = (0::real)"by (erule norm_ratiotest_lemma, simp)(* TODO: MOVE *)lemma le_Suc_ex: "(k::nat) ≤ l ==> (∃n. l = k + n)"apply (drule le_imp_less_or_eq)apply (auto dest: less_imp_Suc_add)donelemma le_Suc_ex_iff: "((k::nat) ≤ l) = (∃n. l = k + n)"by (auto simp add: le_Suc_ex)(*All this trouble just to get 0<c *)lemma ratio_test_lemma2:  fixes f :: "nat => 'a::banach"  shows "[|∀n≥N. norm (f (Suc n)) ≤ c * norm (f n)|] ==> 0 < c ∨ summable f"apply (simp (no_asm) add: linorder_not_le [symmetric])apply (simp add: summable_Cauchy)apply (safe, subgoal_tac "∀n. N < n --> f (n) = 0") prefer 2 apply clarify apply(erule_tac x = "n - Suc 0" in allE) apply (simp add:diff_Suc split:nat.splits) apply (blast intro: norm_ratiotest_lemma)apply (rule_tac x = "Suc N" in exI, clarify)apply(simp cong del: setsum_cong cong: setsum_ivl_cong)donelemma ratio_test:  fixes f :: "nat => 'a::banach"  shows "[|c < 1; ∀n≥N. norm (f (Suc n)) ≤ c * norm (f n)|] ==> summable f"apply (frule ratio_test_lemma2, auto)apply (rule_tac g = "%n. (norm (f N) / (c ^ N))*c ^ n"       in summable_comparison_test)apply (rule_tac x = N in exI, safe)apply (drule le_Suc_ex_iff [THEN iffD1])apply (auto simp add: power_add field_power_not_zero)apply (induct_tac "na", auto)apply (rule_tac y = "c * norm (f (N + n))" in order_trans)apply (auto intro: mult_right_mono simp add: summable_def)apply (rule_tac x = "norm (f N) * (1/ (1 - c)) / (c ^ N)" in exI)apply (rule sums_divide)apply (rule sums_mult)apply (auto intro!: geometric_sums)donesubsection {* Cauchy Product Formula *}(* Proof based on Analysis WebNotes: Chapter 07, Class 41http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm *)lemma setsum_triangle_reindex:  fixes n :: nat  shows "(∑(i,j)∈{(i,j). i+j < n}. f i j) = (∑k=0..<n. ∑i=0..k. f i (k - i))"proof -  have "(∑(i, j)∈{(i, j). i + j < n}. f i j) =    (∑(k, i)∈(SIGMA k:{0..<n}. {0..k}). f i (k - i))"  proof (rule setsum_reindex_cong)    show "inj_on (λ(k,i). (i, k - i)) (SIGMA k:{0..<n}. {0..k})"      by (rule inj_on_inverseI [where g="λ(i,j). (i+j, i)"], auto)    show "{(i,j). i + j < n} = (λ(k,i). (i, k - i)) ` (SIGMA k:{0..<n}. {0..k})"      by (safe, rule_tac x="(a+b,a)" in image_eqI, auto)    show "!!a. (λ(k, i). f i (k - i)) a = split f ((λ(k, i). (i, k - i)) a)"      by clarify  qed  thus ?thesis by (simp add: setsum_Sigma)qedlemma Cauchy_product_sums:  fixes a b :: "nat => 'a::{real_normed_algebra,banach}"  assumes a: "summable (λk. norm (a k))"  assumes b: "summable (λk. norm (b k))"  shows "(λk. ∑i=0..k. a i * b (k - i)) sums ((∑k. a k) * (∑k. b k))"proof -  let ?S1 = "λn::nat. {0..<n} × {0..<n}"  let ?S2 = "λn::nat. {(i,j). i + j < n}"  have S1_mono: "!!m n. m ≤ n ==> ?S1 m ⊆ ?S1 n" by auto  have S2_le_S1: "!!n. ?S2 n ⊆ ?S1 n" by auto  have S1_le_S2: "!!n. ?S1 (n div 2) ⊆ ?S2 n" by auto  have finite_S1: "!!n. finite (?S1 n)" by simp  with S2_le_S1 have finite_S2: "!!n. finite (?S2 n)" by (rule finite_subset)  let ?g = "λ(i,j). a i * b j"  let ?f = "λ(i,j). norm (a i) * norm (b j)"  have f_nonneg: "!!x. 0 ≤ ?f x"    by (auto simp add: mult_nonneg_nonneg)  hence norm_setsum_f: "!!A. norm (setsum ?f A) = setsum ?f A"    unfolding real_norm_def    by (simp only: abs_of_nonneg setsum_nonneg [rule_format])  have "(λn. (∑k=0..<n. a k) * (∑k=0..<n. b k))           ----> (∑k. a k) * (∑k. b k)"    by (intro tendsto_mult summable_sumr_LIMSEQ_suminf        summable_norm_cancel [OF a] summable_norm_cancel [OF b])  hence 1: "(λn. setsum ?g (?S1 n)) ----> (∑k. a k) * (∑k. b k)"    by (simp only: setsum_product setsum_Sigma [rule_format]                   finite_atLeastLessThan)  have "(λn. (∑k=0..<n. norm (a k)) * (∑k=0..<n. norm (b k)))       ----> (∑k. norm (a k)) * (∑k. norm (b k))"    using a b by (intro tendsto_mult summable_sumr_LIMSEQ_suminf)  hence "(λn. setsum ?f (?S1 n)) ----> (∑k. norm (a k)) * (∑k. norm (b k))"    by (simp only: setsum_product setsum_Sigma [rule_format]                   finite_atLeastLessThan)  hence "convergent (λn. setsum ?f (?S1 n))"    by (rule convergentI)  hence Cauchy: "Cauchy (λn. setsum ?f (?S1 n))"    by (rule convergent_Cauchy)  have "Zfun (λn. setsum ?f (?S1 n - ?S2 n)) sequentially"  proof (rule ZfunI, simp only: eventually_sequentially norm_setsum_f)    fix r :: real    assume r: "0 < r"    from CauchyD [OF Cauchy r] obtain N    where "∀m≥N. ∀n≥N. norm (setsum ?f (?S1 m) - setsum ?f (?S1 n)) < r" ..    hence "!!m n. [|N ≤ n; n ≤ m|] ==> norm (setsum ?f (?S1 m - ?S1 n)) < r"      by (simp only: setsum_diff finite_S1 S1_mono)    hence N: "!!m n. [|N ≤ n; n ≤ m|] ==> setsum ?f (?S1 m - ?S1 n) < r"      by (simp only: norm_setsum_f)    show "∃N. ∀n≥N. setsum ?f (?S1 n - ?S2 n) < r"    proof (intro exI allI impI)      fix n assume "2 * N ≤ n"      hence n: "N ≤ n div 2" by simp      have "setsum ?f (?S1 n - ?S2 n) ≤ setsum ?f (?S1 n - ?S1 (n div 2))"        by (intro setsum_mono2 finite_Diff finite_S1 f_nonneg                  Diff_mono subset_refl S1_le_S2)      also have "… < r"        using n div_le_dividend by (rule N)      finally show "setsum ?f (?S1 n - ?S2 n) < r" .    qed  qed  hence "Zfun (λn. setsum ?g (?S1 n - ?S2 n)) sequentially"    apply (rule Zfun_le [rule_format])    apply (simp only: norm_setsum_f)    apply (rule order_trans [OF norm_setsum setsum_mono])    apply (auto simp add: norm_mult_ineq)    done  hence 2: "(λn. setsum ?g (?S1 n) - setsum ?g (?S2 n)) ----> 0"    unfolding tendsto_Zfun_iff diff_0_right    by (simp only: setsum_diff finite_S1 S2_le_S1)  with 1 have "(λn. setsum ?g (?S2 n)) ----> (∑k. a k) * (∑k. b k)"    by (rule LIMSEQ_diff_approach_zero2)  thus ?thesis by (simp only: sums_def setsum_triangle_reindex)qedlemma Cauchy_product:  fixes a b :: "nat => 'a::{real_normed_algebra,banach}"  assumes a: "summable (λk. norm (a k))"  assumes b: "summable (λk. norm (b k))"  shows "(∑k. a k) * (∑k. b k) = (∑k. ∑i=0..k. a i * b (k - i))"using a bby (rule Cauchy_product_sums [THEN sums_unique])end`