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