# Theory Arithmetic_Summatory

theory Arithmetic_Summatory
imports Liouville_Lambda Divisor_Count
```(*
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"

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

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
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)"
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
```