Theory Dirichlet_Series.Arithmetic_Summatory

(*
    File:      Arithmetic_Summatory.thy
    Author:    Manuel Eberl, TU München
*)
section ‹Summatory arithmetic functions›
theory Arithmetic_Summatory
  imports 
    More_Totient
    Moebius_Mu
    Liouville_Lambda
    Divisor_Count 
    Dirichlet_Series
begin

subsection ‹Definition›

definition sum_upto :: "(nat ⇒ 'a :: comm_monoid_add) ⇒ real ⇒ 'a" where
  "sum_upto f x = (∑i | 0 < i ∧ real i ≤ x. f i)"

lemma sum_upto_altdef: "sum_upto f x = (∑i∈{0<..nat ⌊x⌋}. f i)"
  unfolding sum_upto_def
  by (cases "x ≥ 0"; intro sum.cong refl) (auto simp: le_nat_iff le_floor_iff)
    
lemma sum_upto_0 [simp]: "sum_upto f 0 = 0"
  by (simp add: sum_upto_altdef)

lemma sum_upto_cong [cong]:
  "(⋀n. n > 0 ⟹ f n = f' n) ⟹ n = n' ⟹ sum_upto f n = sum_upto f' n'"
  by (simp add: sum_upto_def)

lemma finite_Nats_le_real [simp,intro]: "finite {n. 0 < n ∧ real n ≤ x}"
proof (rule finite_subset)
  show "finite {n. n ≤ nat ⌊x⌋}" by auto
  show "{n. 0 < n ∧ real n ≤ x} ⊆ {n. n ≤ nat ⌊x⌋}" by safe linarith
qed

lemma sum_upto_ind: "sum_upto (ind P) x = of_nat (card {n. n > 0 ∧ real n ≤ x ∧ P n})"
proof -
  have "sum_upto (ind P :: nat ⇒ 'a) x = (∑n | 0 < n ∧ real n ≤ x ∧ P n. 1)"
    unfolding sum_upto_def by (intro sum.mono_neutral_cong_right) (auto simp: ind_def)
  also have "… = of_nat (card {n. n > 0 ∧ real n ≤ x ∧ P n})" by simp
  finally show ?thesis .
qed

lemma sum_upto_sum_divisors:
  "sum_upto (λn. ∑d | d dvd n. f n d) x = sum_upto (λk. sum_upto (λd. f (d * k) k) (x / k)) x"
proof -
  let ?B = "(SIGMA k:{k. 0 < k ∧ real k ≤ x}. {d. 0 < d ∧ real d ≤ x / real k})"
  let ?A = "(SIGMA k:{k. 0 < k ∧ real k ≤ x}. {d. d dvd k})"
  have *: "real a ≤ x" if "real (a * b) ≤ x" "b > 0" for a b
  proof -
    have "real a * 1 ≤ real (a * b)" unfolding of_nat_mult using that
      by (intro mult_left_mono) auto
    also have "… ≤ x" by fact
    finally show ?thesis by simp
  qed
  have bij: "bij_betw (λ(k,d). (d * k, k)) ?B ?A"
    by (rule bij_betwI[where g = "λ(k,d). (d, k div d)"])
       (auto simp: * divide_simps mult.commute elim!: dvdE)

  have "sum_upto (λn. ∑d | d dvd n. f n d) x = (∑(k,d)∈?A. f k d)"
    unfolding sum_upto_def by (rule sum.Sigma) auto
  also have "… = (∑(k,d)∈?B. f (d * k) k)"
    by (subst sum.reindex_bij_betw[OF bij, symmetric]) (auto simp: case_prod_unfold)
  also have "… = sum_upto (λk. sum_upto (λd. f (d * k) k) (x / k)) x"
    unfolding sum_upto_def by (rule sum.Sigma [symmetric]) auto
  finally show ?thesis .
qed

lemma sum_upto_dirichlet_prod:
  "sum_upto (dirichlet_prod f g) x = sum_upto (λd. f d * sum_upto g (x / real d)) x"
  unfolding dirichlet_prod_def
  by (subst sum_upto_sum_divisors) (simp add: sum_upto_def sum_distrib_left)

lemma sum_upto_real: 
  assumes "x ≥ 0"
  shows   "sum_upto real x = of_int (floor x) * (of_int (floor x) + 1) / 2"
proof -
  have A: "2 * ∑{1..n} = n * Suc n" for n by (induction n) simp_all
  have "2 * sum_upto real x = real (2 * ∑{0<..nat ⌊x⌋})" by (simp add: sum_upto_altdef)
  also have "{0<..nat ⌊x⌋} = {1..nat ⌊x⌋}" by auto
  also note A
  also have "real (nat ⌊x⌋ * Suc (nat ⌊x⌋)) = of_int (floor x) * (of_int (floor x) + 1)" using assms
    by (simp add: algebra_simps)
  finally show ?thesis by simp
qed

lemma summable_imp_convergent_sum_upto:
  assumes "summable (f :: nat ⇒ 'a :: real_normed_vector)"
  obtains c where "(sum_upto f ⤏ c) at_top"
proof -
  from assms have "summable (λn. f (Suc n))"
    by (subst summable_Suc_iff)
  then obtain c where "(λn. f (Suc n)) sums c" by (auto simp: summable_def)
  hence "(λn. ∑k<n. f (Suc k)) ⇢ c" by (auto simp: sums_def)
  also have "(λn. ∑k<n. f (Suc k)) = (λn. ∑k∈{0<..n}. f k)"
    by (subst sum.atLeast1_atMost_eq [symmetric]) (auto simp: atLeastSucAtMost_greaterThanAtMost)
  finally have "((λx. sum f {0<..nat ⌊x⌋}) ⤏ c) at_top"
    by (rule filterlim_compose)
       (auto intro!: filterlim_compose[OF filterlim_nat_sequentially] filterlim_floor_sequentially)
  also have "(λx. sum f {0<..nat ⌊x⌋}) = sum_upto f"
    by (intro ext) (simp_all add: sum_upto_altdef)
  finally show ?thesis using that[of c] by blast
qed


subsection ‹The Hyperbola method›

lemma hyperbola_method_semiring:
  fixes f g :: "nat ⇒ 'a :: comm_semiring_0"
  assumes "A ≥ 0" and "B ≥ 0" and "A * B = x"
  shows   "sum_upto (dirichlet_prod f g) x + sum_upto f A * sum_upto g B = 
             sum_upto (λn. f n * sum_upto g (x / real n)) A +
             sum_upto (λn. sum_upto f (x / real n) * g n) B"
proof -
  from assms have [simp]: "x ≥ 0" by auto
  {
    fix a b :: real assume ab: "a > 0" "b > 0" "x ≥ 0" "a * b ≤ x" "a > A" "b > B"
    hence "a * b > A * B" using assms by (intro mult_strict_mono) auto
    also from assms have "A * B = x" by simp
    finally have False using ‹a * b ≤ x› by simp
  } note * = this
  have *: "a ≤ A ∨ b ≤ B" if "a * b ≤ x" "a > 0" "b > 0" "x ≥ 0" for a b
    by (rule ccontr) (insert *[of a b] that, auto)
  
  have nat_mult_leD1: "real a ≤ x" if "real a * real b ≤ x" "b > 0" for a b
  proof -
    from that have "real a * 1 ≤ real a * real b" by (intro mult_left_mono) simp_all
    also have "… ≤ x" by fact
    finally show ?thesis by simp
  qed
  have nat_mult_leD2: "real b ≤ x" if "real a * real b ≤ x" "a > 0" for a b
    using nat_mult_leD1[of b a] that by (simp add: mult_ac)
  
  have le_sqrt_mult_imp_le: "a * b ≤ x" 
    if "a ≥ 0" "b ≥ 0" "a ≤ A" "b ≤ B" for a b :: real
  proof -
    from that and assms have "a * b ≤ A * B" by (intro mult_mono) auto
    with assms show "a * b ≤ x" by simp
  qed
  
  define F G where "F = sum_upto f" and "G = sum_upto g"  
  let ?Bound = "{0<..nat ⌊x⌋} × {0<..nat ⌊x⌋}"
  let ?B = "{(r,d). 0 < r ∧ real r ≤ A ∧ 0 < d ∧ real d ≤ x / real r}"
  let ?C = "{(r,d). 0 < d ∧ real d ≤ B ∧ 0 < r ∧ real r ≤ x / real d}"
  let ?B' = "SIGMA r:{r. 0 < r ∧ real r ≤ A}. {d. 0 < d ∧ real d ≤ x / real r}"
  let ?C' = "SIGMA d:{d. 0 < d ∧ real d ≤ B}. {r. 0 < r ∧ real r ≤ x / real d}"
  have "sum_upto (dirichlet_prod f g) x + F A * G B = 
          (∑(i,(r,d)) ∈ (SIGMA i:{i. 0 < i ∧ real i ≤ x}. {(r,d). r * d = i}). f r * g d) + 
          sum_upto f A * sum_upto g B" (is "_ = ?S + _")
    unfolding sum_upto_def dirichlet_prod_altdef2 F_def G_def
    by (subst sum.Sigma) (auto intro: finite_divisors_nat')
  also have "?S = (∑(r,d) | 0 < r ∧ 0 < d ∧ real (r * d) ≤ x. f r * g d)"
    (is "_ = sum _ ?A") by (intro sum.reindex_bij_witness[of _ "λ(r,d). (r*d,(r,d))" snd]) auto
  also have "?A = ?B ∪ ?C"  by (auto simp: field_simps dest: *)
  also have "sum_upto f A * sum_upto g B = 
               (∑r | 0 < r ∧ real r ≤ A. ∑d | 0 < d ∧ real d ≤ B. f r * g d)"
    by (simp add: sum_upto_def sum_product)
  also have "… = (∑(r,d)∈{r. 0 < r ∧ real r ≤ A} × {d. 0 < d ∧ real d ≤ B}. f r * g d)"
    (is "_ = sum _ ?X") by (rule sum.cartesian_product)
  also have "?X = ?B ∩ ?C" by (auto simp: field_simps le_sqrt_mult_imp_le)
  also have "(∑(r,d)∈?B ∪ ?C. f r * g d) + (∑(r,d)∈?B ∩ ?C. f r * g d) = 
               (∑(r,d)∈?B. f r * g d) + (∑(r,d)∈?C. f r * g d)"
    by (intro sum.union_inter finite_subset[of ?B ?Bound] finite_subset[of ?C ?Bound])
       (auto simp: field_simps le_nat_iff le_floor_iff dest: nat_mult_leD1 nat_mult_leD2)
  also have "?B = ?B'" by auto
  hence "(λf. sum f ?B) = (λf. sum f ?B')" by simp
  also have "(∑(r,d)∈?B'. f r * g d) = sum_upto (λn. f n * G (x / real n)) A"
    by (subst sum.Sigma [symmetric]) (simp_all add: sum_upto_def sum_distrib_left G_def)
  also have "(∑(r,d)∈?C. f r * g d) = (∑(d,r)∈?C'. f r * g d)"
    by (intro sum.reindex_bij_witness[of _ "λ(x,y). (y,x)" "λ(x,y). (y,x)"]) auto
  also have "… = sum_upto (λn. F (x / real n) * g n) B"
    by (subst sum.Sigma [symmetric]) (simp_all add: sum_upto_def sum_distrib_right F_def)
  finally show ?thesis by (simp only: F_def G_def)
qed

lemma hyperbola_method_semiring_sqrt:
  fixes f g :: "nat ⇒ 'a :: comm_semiring_0"
  assumes "x ≥ 0"
  shows   "sum_upto (dirichlet_prod f g) x + sum_upto f (sqrt x) * sum_upto g (sqrt x) = 
             sum_upto (λn. f n * sum_upto g (x / real n)) (sqrt x) +
             sum_upto (λn. sum_upto f (x / real n) * g n) (sqrt x)"
  using assms hyperbola_method_semiring[of "sqrt x" "sqrt x" x] by simp

lemma hyperbola_method:
  fixes f g :: "nat ⇒ 'a :: comm_ring"
  assumes "A ≥ 0" "B ≥ 0" "A * B = x"
  shows   "sum_upto (dirichlet_prod f g) x = 
             sum_upto (λn. f n * sum_upto g (x / real n)) A +
             sum_upto (λn. sum_upto f (x / real n) * g n) B -
             sum_upto f A * sum_upto g B"
  using hyperbola_method_semiring[OF assms, of f g] by (simp add: algebra_simps)

lemma hyperbola_method_sqrt:
  fixes f g :: "nat ⇒ 'a :: comm_ring"
  assumes "x ≥ 0"
  shows   "sum_upto (dirichlet_prod f g) x = 
             sum_upto (λn. f n * sum_upto g (x / real n)) (sqrt x) +
             sum_upto (λn. sum_upto f (x / real n) * g n) (sqrt x) -
             sum_upto f (sqrt x) * sum_upto g (sqrt x)"
  using assms hyperbola_method[of "sqrt x" "sqrt x" x] by simp

end