(* 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