Theory Partial_Summation

theory Partial_Summation
imports Analysis Arithmetic_Summatory
(*
    File:      Partial_Summation.thy
    Author:    Manuel Eberl, TU M√ľnchen
    
    The partial summation rule as given by Apostol in "Introduction to Analytic Number Theory"
*)
section ‹Partial summation›
theory Partial_Summation
  imports
    "HOL-Analysis.Analysis"
    Arithmetic_Summatory
begin

lemma finite_vimage_real_of_nat_greaterThanAtMost: "finite (real -` {y<..x})"
proof (rule finite_subset)
  show "real -` {y<..x} ⊆ {nat ⌊y⌋..nat ⌈x⌉}"
    by (cases "x ≥ 0"; cases "y ≥ 0")
        (auto simp: nat_le_iff le_nat_iff le_ceiling_iff floor_le_iff)
qed auto

context
  fixes a :: "nat ⇒ 'a :: {banach, real_normed_algebra}"
  fixes f f' :: "real ⇒ 'a"
  fixes A
  fixes X :: "real set"
  fixes x y :: real
  defines "A ≡ sum_upto a"
  assumes fin: "finite X"
  assumes xy: "0 ≤ y" "y < x"
  assumes deriv: "⋀z. z ∈ {y..x} - X ⟹ (f has_vector_derivative f' z) (at z)"
  assumes cont_f: "continuous_on {y..x} f"
begin

lemma partial_summation_strong:
  "((λt. A t * f' t) has_integral 
       (A x * f x - A y * f y - (∑n ∈ real -` {y<..x}. a n * f n))) {y..x}"
proof -
  define chi :: "nat ⇒ real ⇒ real" where "chi = (λn t. if n ≤ t then 1 else 0)"
  have "((λt. sum_upto (λn. a n * (chi n t *R f' t)) x) has_integral 
          (sum_upto (λn. a n * (f x - f (max n y))) x)) {y..x}" (is "(_ has_integral ?I) _")
    unfolding sum_upto_def
  proof (intro has_integral_sum ballI finite_Nats_le_real, goal_cases)
    case (1 n)
    have "(f' has_integral (f x - f (max n y))) {max n y..x}"
      using xy 1
      by (intro fundamental_theorem_of_calculus_strong[OF fin])
         (auto intro!: continuous_on_subset[OF cont_f] deriv)
    also have "?this ⟷ ((λt. (if t ∈ {max n y..x} then 1 else 0) *R f' t) 
                  has_integral (f x - f (max n y))) {max n y..x}"
      by (intro has_integral_cong) (simp_all add: chi_def)
    finally have "((λt. (if t ∈ {max n y..x} then 1 else 0) *R f' t) 
                     has_integral (f x - f (max n y))) {y..x}"
      by (rule has_integral_on_superset) auto
    also have "?this ⟷ ((λt. chi n t *R f' t) has_integral (f x - f (max n y))) {y..x}"
      by (intro has_integral_cong) (auto simp: chi_def)
    finally show ?case by (intro has_integral_mult_right)
  qed
  also have "?this ⟷ ((λt. A t * f' t) has_integral ?I) {y..x}"
    unfolding sum_upto_def A_def chi_def sum_distrib_right using xy
    by (intro has_integral_cong sum.mono_neutral_cong_right finite_Nats_le_real) auto
  also have "sum_upto (λn. a n * (f x - f (max (real n) y))) x =
               A x * f x - (∑n | n > 0 ∧ real n ≤ x.  a n * f (max (real n) y))"
    by (simp add: sum_upto_def ring_distribs sum_subtractf sum_distrib_right A_def)
  also have "{n. n > 0 ∧ real n ≤ x} = {n. n > 0 ∧ real n ≤ y} ∪ real -` {y<..x}"
    using xy by auto
  also have "sum (λn. a n * f (max (real n) y)) … = 
               (∑n | 0 < n ∧ real n ≤ y. a n * f (max (real n) y)) +
               (∑n ∈ real -` {y<..x}. a n * f (max (real n) y))" (is "_ = ?S1 + ?S2")
    by (intro sum.union_disjoint finite_Nats_le_real finite_vimage_real_of_nat_greaterThanAtMost) 
       auto
  also have "?S1 = sum_upto (λn. a n * f y) y" unfolding sum_upto_def 
    by (intro sum.cong refl) (auto simp: max_def)
  also have "… = A y * f y" by (simp add: A_def sum_upto_def sum_distrib_right)
  also have "?S2 = (∑n ∈ real -` {y<..x}. a n * f n)"
    by (intro sum.cong refl) (auto simp: max_def)
  finally show ?thesis by (simp add: algebra_simps)
qed

lemma partial_summation_integrable_strong: 
        "(λt. A t * f' t) integrable_on {y..x}"
  and partial_summation_strong': 
        "(∑n∈real -` {y<..x}. a n * f n) = 
            A x * f x - A y * f y - integral {y..x} (λt. A t * f' t)"
  using partial_summation_strong by (simp_all add: has_integral_iff algebra_simps)

end


context
  fixes a :: "nat ⇒ 'a :: {banach, real_normed_algebra}"
  fixes f f' :: "real ⇒ 'a"
  fixes A
  fixes X :: "real set"
  fixes x :: real
  defines "A ≡ sum_upto a"
  assumes fin: "finite X"
  assumes x: "x > 0"
  assumes deriv: "⋀z. z ∈ {0..x} - X ⟹ (f has_vector_derivative f' z) (at z)"
  assumes cont_f: "continuous_on {0..x} f"
begin

lemma partial_summation_sum_upto_strong:
  "((λt. A t * f' t) has_integral (A x * f x - sum_upto (λn. a n * f n) x)) {0..x}"
proof -
  have "(∑n∈real -` {0<..x}. a n * f n) = sum_upto (λn. a n * f n) x"
    unfolding sum_upto_def by (intro sum.cong refl) auto
  thus ?thesis
  using partial_summation_strong[OF fin order.refl x deriv cont_f, of a]
  by (simp_all add: A_def)
qed

lemma partial_summation_integrable_sum_upto_strong: 
        "(λt. A t * f' t) integrable_on {0..x}"
  and partial_summation_sum_upto_strong': 
        "sum_upto (λn. a n * f n) x = 
            A x * f x - integral {0..x} (λt. A t * f' t)"
  using partial_summation_sum_upto_strong by (simp_all add: has_integral_iff algebra_simps)
  
end

end