Theory Summation_Tests_More

section ‹Some Abel-Style Summation Tests›
theory Summation_Tests_More
  imports "HOL-Analysis.Analysis" "HOL-Library.Landau_Symbols" Lambert_Series_Library
begin

text ‹
  The following five summation tests are taking from Chapter 10 of Knopp's textbook~\cite{knopp22}.
  He introduces a strong variant of Abel's summation test and then deduces from it four
  summation test named after Abel, Dirichlet, du Bois-Reymond, and Dedekind.
›
lemma abel_partial_summation:
  fixes f g :: "nat ⇒ 'a :: comm_ring_1"
  defines "F ≡ (λn. ∑k≤n. f k)"
  shows   "(∑r=n+1..n+k. f r * g r) =
             (∑r=n+1..n+k. F r * (g r - g (Suc r))) - 
             F n * g (Suc n) + F (n + k) * g (n + k + 1)"
  by (induction k) (auto simp: F_def algebra_simps)

theorem abel_summation_test_strong:
  fixes f g :: "nat ⇒ 'a :: {real_normed_field, banach}"
  defines "F ≡ (λn. ∑k≤n. f k)"
  assumes "summable (λr. F r * (g r - g (Suc r)))"
  assumes "convergent (λr. F r * g (Suc r))"
  shows   "summable (λr. f r * g r)"
  unfolding summable_iff_convergent'
proof (rule Cauchy_convergent)
  show "Cauchy (λn. ∑r≤n. f r * g r)"
    unfolding Cauchy_def
  proof safe
    fix ε :: real assume ε: "ε > 0"
    let ?A = "λn. (∑r≤n. F r * (g r - g (Suc r)))"
    from assms(2) have "Cauchy (λn. ∑r≤n. F r * (g r - g (Suc r)))"
      unfolding summable_iff_convergent' using convergent_Cauchy by blast
    moreover have "ε / 2 > 0"
      using ε by auto
    ultimately obtain M1 where M1: "dist (?A m) (?A n) < ε / 2" if "m ≥ M1" "n ≥ M1" for m n
      unfolding Cauchy_def by fast
    have M1': "norm (∑r=m..n. F r * (g r - g (Suc r))) < ε / 2" if "M1 < m" "m ≤ Suc n" for m n
    proof -
      have "dist (?A n) (?A (m - 1)) < ε / 2"
        by (rule M1) (use that in auto)
      also have "dist (?A n) (?A (m - 1)) = norm (∑r∈{..n}-{..m - 1}. F r * (g r - g (Suc r)))"
        unfolding dist_norm using that by (subst Groups_Big.sum_diff) auto
      also have "{..n} - {..m - 1} = {m..n}"
        using that by auto
      finally show ?thesis .
    qed

    from ε have "ε / 4 > 0"
      by auto
    from assms(3) obtain c where "(λr. F r * g (Suc r)) ⇢ c"
      by (auto simp: convergent_def)
    with ‹ε / 4 > 0› have "eventually (λr. dist (F r * g (Suc r)) c < ε / 4) sequentially"
      using tendstoD by blast
    then obtain M2 where M2: "dist (F r * g (Suc r)) c < ε / 4" if "r ≥ M2" for r
      unfolding eventually_at_top_linorder by blast

    show "∃M. ∀m≥M. ∀n≥M. dist (∑r≤m. f r * g r) (∑r≤n. f r * g r) < ε"
    proof (rule exI[of _ "max M1 M2"], safe)
      fix m n :: nat assume "m ≥ max M1 M2" "n ≥ max M1 M2"
      thus "dist (∑r≤m. f r * g r) (∑r≤n. f r * g r) < ε"
      proof (induction m n rule: linorder_wlog)
        case (le m n)
        define k where "k = n - m"
        from le have n_eq: "n = m + k"
          by (auto simp: k_def)
        have "dist (∑r≤m. f r * g r) (∑r≤n. f r * g r) =
              norm ((∑r≤n. f r * g r) - (∑r≤m. f r * g r))"
          by (simp add: dist_norm norm_minus_commute)
        also have "(∑r≤n. f r * g r) - (∑r≤m. f r * g r) = (∑r∈{..n}-{..m}. f r * g r)"
          using le by (subst Groups_Big.sum_diff) auto
        also have "{..n} - {..m} = {m+1..m+k}"
          by (auto simp: n_eq)
        also have "(∑r=m+1..m+k. f r * g r) =
                     (∑r=m+1..m+k. F r * (g r - g (Suc r))) - 
                      F m * g (Suc m) + F (m + k) * g (Suc (m + k))"
          unfolding F_def by (subst abel_partial_summation) simp_all
        also have "norm … ≤ norm (∑r=m+1..m+k. F r * (g r - g (Suc r))) +
                     dist (F m * g (Suc m)) c + dist (F (m + k) * g (Suc (m + k))) c"
          by norm
        also have "… < ε / 2 + ε / 4 + ε / 4"
          using le by (intro add_strict_mono M1' M2) auto
        also have "… = ε"
          by simp
        finally show "dist (∑r≤m. f r * g r) (∑r≤n. f r * g r) < ε" .
      qed (simp add: dist_commute max.commute)
    qed
  qed
qed

corollary abel_summation_test:
  fixes f g :: "nat ⇒ real"
  assumes "summable f"
  assumes "incseq g" "g ∈ O(λ_. 1)"
  shows   "summable (λr. f r * g r)"
proof (rule abel_summation_test_strong)
  have "convergent g"
    by (rule incseq_convergent') fact+
  thus "convergent (λn. (∑k≤n. f k) * g (Suc n))" using assms(1)
    by (intro convergent_mult) (simp_all add: convergent_Suc_iff summable_iff_convergent')
  show "summable (λn. (∑k≤n. f k) * (g n - g (Suc n)))"
  proof (subst mult.commute, rule summable_norm_cancel, rule norm_summable_mult_bounded)
    have "summable (λn. g (Suc n) - g n)"
      using ‹convergent g› by (simp add: telescope_summable_iff)
    also have "(λn. g (Suc n) - g n) = (λn. norm (g n - g (Suc n)))"
      using ‹incseq g› by (auto simp: incseq_def fun_eq_iff)
    finally show "summable (λn. norm (g n - g (Suc n)))" .
  next
    have "bounded (range (λn. ∑k<n. f k))"
      by (rule summable_imp_sums_bounded) fact
    hence "(λn. ∑k<n. f k) ∈ O(λ_. 1)"
      by (simp add: seq_bigo_1_iff)
    hence "(λn. ∑k<Suc n. f k) ∈ O(λ_. 1)"
      by (rule landau_o.big.compose) (rule filterlim_Suc)
    also have "(λn. {..<Suc n}) = (λn. {..n})"
      by auto
    finally show "(λn. ∑k≤n. f k) ∈ O(λ_. 1)" .
  qed
qed

corollary dirichlet_summation_test:
  fixes f g :: "nat ⇒ real"
  assumes "(λn. ∑r≤n. f r) ∈ O(λ_. 1)"
  assumes "decseq g" "g ∈ o(λ_. 1)"
  shows   "summable (λr. f r * g r)"
proof (rule abel_summation_test_strong)
  have "(λx. g (Suc x)) ∈ o(λx. 1)"
    using assms(3) by (rule landau_o.small.compose) (rule filterlim_Suc)
  have "(λn. (∑r≤n. f r) * g (Suc n)) ∈ o(λ_. 1 * 1)"
    by (rule landau_o.big_small_mult) fact+
  thus "convergent (λr. sum f {..r} * g (Suc r))"
    by (auto dest!: smalloD_tendsto simp: convergent_def)
next
  have "g ⇢ 0"
    using assms(3) by (auto dest!: smalloD_tendsto simp: convergent_def)
  hence "convergent g"
    by (auto simp: convergent_def)
  show "summable (λn. (∑k≤n. f k) * (g n - g (Suc n)))"
  proof (subst mult.commute, rule summable_norm_cancel, rule norm_summable_mult_bounded)
    have "summable (λn. g n - g (Suc n))"
      using ‹convergent g› by (simp add: telescope_summable_iff')
    also have "(λn. g n - g (Suc n)) = (λn. norm (g n - g (Suc n)))"
      using ‹decseq g› by (auto simp: decseq_Suc_iff fun_eq_iff)
    finally show "summable (λn. norm (g n - g (Suc n)))" .
  qed fact
qed

corollary dubois_reymond_summation_test:
  fixes f g :: "nat ⇒ 'a :: {real_normed_field, banach}"
  assumes "summable f"
  assumes "summable (λr. norm (g r - g (Suc r)))"
  shows   "summable (λr. f r * g r)"
proof (rule abel_summation_test_strong)
  have "summable (λr. g r - g (Suc r))"
    using assms(2) by (rule summable_norm_cancel)
  hence "convergent g"
    by (subst (asm) telescope_summable_iff')
  show "convergent (λr. sum f {..r} * g (Suc r))"
    using assms(1) ‹convergent g›
    by (intro convergent_mult) (auto simp: convergent_Suc_iff summable_iff_convergent')

  show "summable (λn. (∑k≤n. f k) * (g n - g (Suc n)))"
  proof (subst mult.commute, rule summable_norm_cancel, rule norm_summable_mult_bounded)
    have "bounded (range (λn. ∑k<n. f k))"
      by (rule summable_imp_sums_bounded) fact
    hence "(λn. ∑k<n. f k) ∈ O(λ_. 1)"
      by (simp add: seq_bigo_1_iff)
    hence "(λn. ∑k<Suc n. f k) ∈ O(λ_. 1)"
      by (rule landau_o.big.compose) (rule filterlim_Suc)
    also have "(λn. {..<Suc n}) = (λn. {..n})"
      by auto
    finally show "(λn. ∑k≤n. f k) ∈ O(λ_. 1)" .
  qed fact
qed

corollary dedekind_summation_test:
  fixes f g :: "nat ⇒ 'a :: {real_normed_field, banach}"
  assumes "(λn. ∑k≤n. f k) ∈ O(λ_. 1)"
  assumes "summable (λr. norm (g r - g (Suc r)))"
  assumes "g ∈ o(λ_. 1)"
  shows   "summable (λr. f r * g r)"
proof (rule abel_summation_test_strong)
  have "(λx. g (Suc x)) ∈ o(λx. 1)"
    using assms(3) by (rule landau_o.small.compose) (rule filterlim_Suc)
  have "(λn. (∑r≤n. f r) * g (Suc n)) ∈ o(λ_. 1 * 1)"
    by (rule landau_o.big_small_mult) fact+
  thus "convergent (λr. sum f {..r} * g (Suc r))"
    by (auto dest!: smalloD_tendsto simp: convergent_def)
  show "summable (λn. (∑k≤n. f k) * (g n - g (Suc n)))"
    by (subst mult.commute, rule summable_norm_cancel, rule norm_summable_mult_bounded) fact+
qed

end