Theory Arithmetic_Summatory
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_1 [simp]: "sum_upto f 1 = f 1"
proof -
have "{0<..Suc 0} = {1}" by auto
thus ?thesis by (simp add: sum_upto_altdef)
qed
lemma sum_upto_cong [cong]:
"(⋀n. n > 0 ⟹ real n ≤ x ⟹ f n = f' n) ⟹ x = x' ⟹ sum_upto f x = sum_upto f' x'"
unfolding sum_upto_def by (intro sum.cong) auto
lemma sum_upto_0 [simp]: "sum_upto f 0 = 0"
by (simp add: sum_upto_altdef)
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
lemma sum_upto_divisor_sum1:
"sum_upto (λn. ∑d | d dvd n. f d :: real) x = sum_upto (λn. f n * floor (x / n)) x"
proof -
have "sum_upto (λn. ∑d | d dvd n. f d :: real) x =
sum_upto (λn. f n * real (nat (floor (x / n)))) x"
using sum_upto_dirichlet_prod[of f "λ_. 1" x]
by (simp add: dirichlet_prod_def sum_upto_altdef)
also have "… = sum_upto (λn. f n * floor (x / n)) x"
unfolding sum_upto_def by (intro sum.cong) auto
finally show ?thesis .
qed
lemma sum_upto_divisor_sum2:
"sum_upto (λn. ∑d | d dvd n. f d :: real) x = sum_upto (λn. sum_upto f (x / n)) x"
using sum_upto_dirichlet_prod[of "λ_. 1" f x] by (simp add: dirichlet_prod_altdef1)
lemma ln_fact_conv_sum_mangoldt:
"sum_upto (λn. mangoldt n * ⌊x / real n⌋) x = ln (fact (nat ⌊x⌋))"
proof -
have "sum_upto (λn. mangoldt n * of_int ⌊x / real n⌋) x =
sum_upto (λn. ∑d | d dvd n. mangoldt d :: real) x"
using sum_upto_divisor_sum1[of mangoldt x] by auto
also have "… = sum_upto (λn. of_real (ln (real n))) x"
by (intro sum_upto_cong mangoldt_sum refl) auto
also have "… = (∑n∈{0<..nat ⌊x⌋}. ln n)"
by (simp add: sum_upto_altdef)
also have "… = ln (∏{0<..nat ⌊x⌋})"
unfolding of_nat_prod by (subst ln_prod) auto
also have "{0<..nat ⌊x⌋} = {1..nat ⌊x⌋}" by auto
also have "∏… = fact (nat ⌊x⌋)"
by (simp add: fact_prod)
finally show ?thesis by simp
qed
subsection ‹Generalised Dirichlet products›
definition dirichlet_prod' :: "(nat ⇒ 'a :: comm_semiring_1) ⇒ (real ⇒ 'a) ⇒ real ⇒ 'a" where
"dirichlet_prod' f g x = sum_upto (λm. f m * g (x / real m)) x"
lemma dirichlet_prod'_one_left:
"dirichlet_prod' (λn. if n = 1 then 1 else 0) f x = (if x ≥ 1 then f x else 0)"
proof -
have "dirichlet_prod' (λn. if n = 1 then 1 else 0) f x =
(∑i | 0 < i ∧ real i ≤ x. (if i = Suc 0 then 1 else 0) * f (x / real i))"
by (simp add: dirichlet_prod'_def sum_upto_def)
also have "… = (∑i∈(if x ≥ 1 then {1::nat} else {}). f x)"
by (intro sum.mono_neutral_cong_right) (auto split: if_splits)
also have "… = (if x ≥ 1 then f x else 0)"
by simp
finally show ?thesis .
qed
lemma dirichlet_prod'_cong:
assumes "⋀n. n > 0 ⟹ real n ≤ x ⟹ f n = f' n"
assumes "⋀y. y ≥ 1 ⟹ y ≤ x ⟹ g y = g' y"
assumes "x = x'"
shows "dirichlet_prod' f g x = dirichlet_prod' f' g' x'"
unfolding dirichlet_prod'_def
by (intro sum_upto_cong assms, (subst assms | simp add: assms field_simps)+)
lemma dirichlet_prod'_assoc:
"dirichlet_prod' f (λy. dirichlet_prod' g h y) x = dirichlet_prod' (dirichlet_prod f g) h x"
proof -
have "dirichlet_prod' f (λy. dirichlet_prod' g h y) x =
(∑m | m > 0 ∧ real m ≤ x. ∑n | n > 0 ∧ real n ≤ x / m. f m * g n * h (x / (m * n)))"
by (simp add: algebra_simps dirichlet_prod'_def dirichlet_prod_def
sum_upto_def sum_distrib_left sum_distrib_right)
also have "… = (∑(m,n)∈(SIGMA m:{m. m > 0 ∧ real m ≤ x}. {n. n > 0 ∧ real n ≤ x / m}).
f m * g n * h (x / (m * n)))"
by (subst sum.Sigma) auto
also have "… = (∑(mn, m)∈(SIGMA mn:{mn. mn > 0 ∧ real mn ≤ x}. {m. m dvd mn}).
f m * g (mn div m) * h (x / mn))"
by (rule sum.reindex_bij_witness[of _ "λ(mn, m). (m, mn div m)" "λ(m, n). (m * n, m)"])
(auto simp: case_prod_unfold field_simps dest: dvd_imp_le)
also have "… = dirichlet_prod' (dirichlet_prod f g) h x"
by (subst sum.Sigma [symmetric])
(simp_all add: dirichlet_prod'_def dirichlet_prod_def sum_upto_def
algebra_simps sum_distrib_left sum_distrib_right)
finally show ?thesis .
qed
lemma dirichlet_prod'_inversion1:
assumes "∀x≥1. g x = dirichlet_prod' a f x" "x ≥ 1"
"dirichlet_prod a ainv = (λn. if n = 1 then 1 else 0)"
shows "f x = dirichlet_prod' ainv g x"
proof -
have "dirichlet_prod' ainv g x = dirichlet_prod' ainv (dirichlet_prod' a f) x"
using assms by (intro dirichlet_prod'_cong) auto
also have "… = dirichlet_prod' (λn. if n = 1 then 1 else 0) f x"
using assms by (simp add: dirichlet_prod'_assoc dirichlet_prod_commutes)
also have "… = f x"
using assms by (subst dirichlet_prod'_one_left) auto
finally show ?thesis ..
qed
lemma dirichlet_prod'_inversion2:
assumes "∀x≥1. f x = dirichlet_prod' ainv g x" "x ≥ 1"
"dirichlet_prod a ainv = (λn. if n = 1 then 1 else 0)"
shows "g x = dirichlet_prod' a f x"
proof -
have "dirichlet_prod' a f x = dirichlet_prod' a (dirichlet_prod' ainv g) x"
using assms by (intro dirichlet_prod'_cong) auto
also have "… = dirichlet_prod' (λn. if n = 1 then 1 else 0) g x"
using assms by (simp add: dirichlet_prod'_assoc dirichlet_prod_commutes)
also have "… = g x"
using assms by (subst dirichlet_prod'_one_left) auto
finally show ?thesis ..
qed
lemma dirichlet_prod'_inversion:
assumes "dirichlet_prod a ainv = (λn. if n = 1 then 1 else 0)"
shows "(∀x≥1. g x = dirichlet_prod' a f x) ⟷ (∀x≥1. f x = dirichlet_prod' ainv g x)"
using dirichlet_prod'_inversion1[of g a f _ ainv] dirichlet_prod'_inversion2[of f ainv g _ a]
assms by blast
lemma dirichlet_prod'_inversion':
assumes "a 1 * y = 1"
defines "ainv ≡ dirichlet_inverse a y"
shows "(∀x≥1. g x = dirichlet_prod' a f x) ⟷ (∀x≥1. f x = dirichlet_prod' ainv g x)"
unfolding ainv_def
by (intro dirichlet_prod'_inversion dirichlet_prod_inverse assms)
lemma dirichlet_prod'_floor_conv_sum_upto:
"dirichlet_prod' f (λx. real_of_int (floor x)) x = sum_upto (λn. sum_upto f (x / n)) x"
proof -
have [simp]: "sum_upto (λ_. 1 :: real) x = real (nat ⌊x⌋)" for x
by (simp add: sum_upto_altdef)
show ?thesis
using sum_upto_dirichlet_prod[of "λn. 1::real" f] sum_upto_dirichlet_prod[of f "λn. 1::real"]
by (simp add: dirichlet_prod'_def dirichlet_prod_commutes)
qed
lemma dirichlet_prod_inversion_completely_multiplicative:
fixes a :: "nat ⇒ 'a :: comm_ring_1"
assumes "completely_multiplicative_function a"
shows "(∀x≥1. g x = dirichlet_prod' a f x) ⟷
(∀x≥1. f x = dirichlet_prod' (λn. moebius_mu n * a n) g x)"
by (intro dirichlet_prod'_inversion ext completely_multiplicative_imp_moebius_mu_inverse assms)
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
subsection ‹A weighted sum of the Möbius ‹μ› function›
lemma sum_upto_moebius_times_floor_linear:
"sum_upto (λn. moebius_mu n * ⌊x / real n⌋) x = (if x ≥ 1 then 1 else 0)"
proof -
have "real_of_int (sum_upto (λn. moebius_mu n * ⌊x / real n⌋) x) =
sum_upto (λn. moebius_mu n * of_int ⌊x / real n⌋) x"
by (simp add: sum_upto_def)
also have "… = sum_upto (λn. ∑d | d dvd n. moebius_mu d :: real) x"
using sum_upto_divisor_sum1[of moebius_mu x] by auto
also have "… = sum_upto (λn. if n = 1 then 1 else 0) x"
by (intro sum_upto_cong sum_moebius_mu_divisors' refl)
also have "… = real_of_int (if x ≥ 1 then 1 else 0)"
by (auto simp: sum_upto_def)
finally show ?thesis unfolding of_int_eq_iff .
qed
context
fixes M :: "real ⇒ real"
defines "M ≡ (λx. sum_upto (λn. moebius_mu n / n) x)"
begin
lemma abs_sum_upto_moebius_mu_over_n_less:
assumes x: "x ≥ 2"
shows "¦M x¦ < 1"
proof -
have "x * sum_upto (λn. moebius_mu n / n) x - sum_upto (λn. moebius_mu n * frac (x / n)) x =
sum_upto (λn. moebius_mu n * (x / n - frac (x / n))) x"
by (subst mult.commute[of x])
(simp add: sum_upto_def sum_distrib_right sum_subtractf ring_distribs)
also have "(λn. x / real n - frac (x / real n)) = (λn. of_int (floor (x / real n)))"
by (simp add: frac_def)
also have "sum_upto (λn. moebius_mu n * real_of_int ⌊x / real n⌋) x =
real_of_int (sum_upto (λn. moebius_mu n * ⌊x / real n⌋) x)"
by (simp add: sum_upto_def)
also have "… = 1"
using x by (subst sum_upto_moebius_times_floor_linear) auto
finally have eq: "x * M x = 1 + sum_upto (λn. moebius_mu n * frac (x / n)) x"
by (simp add: M_def)
have "x * ¦M x¦ = ¦x * M x¦"
using x by (simp add: abs_mult)
also note eq
also have "¦1 + sum_upto (λn. moebius_mu n * frac (x / n)) x¦ ≤
1 + ¦sum_upto (λn. moebius_mu n * frac (x / n)) x¦"
by linarith
also have "¦sum_upto (λn. moebius_mu n * frac (x / n)) x¦ ≤
sum_upto (λn. ¦moebius_mu n * frac (x / n)¦) x"
unfolding sum_upto_def by (rule sum_abs)
also have "… ≤ sum_upto (λn. frac (x / n)) x"
unfolding sum_upto_def by (intro sum_mono) (auto simp: moebius_mu_def abs_mult)
also have "… = (∑n∈{0<..nat ⌊x⌋}. frac (x / n))"
by (simp add: sum_upto_altdef)
also have "{0<..nat ⌊x⌋} = insert 1 {1<..nat ⌊x⌋}"
using x by (auto simp: le_nat_iff le_floor_iff)
also have "(∑n∈…. frac (x / n)) = frac x + (∑n∈{1<..nat ⌊x⌋}. frac (x / n))"
by (subst sum.insert) auto
also have "(∑n∈{1<..nat ⌊x⌋}. frac (x / n)) < (∑n∈{1<..nat ⌊x⌋}. 1)"
using x by (intro sum_strict_mono frac_lt_1) auto
also have "… = nat ⌊x⌋ - 1" by simp
also have "1 + (frac x + real (nat ⌊x⌋ - 1)) = x"
using x by (subst of_nat_diff) (auto simp: le_nat_iff le_floor_iff frac_def)
finally have "x * ¦M x¦ < x * 1" by simp
with x show "¦M x¦ < 1"
by (subst (asm) mult_less_cancel_left_pos) auto
qed
lemma sum_upto_moebius_mu_over_n_eq:
assumes "x < 2"
shows "M x = (if x ≥ 1 then 1 else 0)"
proof (cases "x ≥ 1")
case True
have "M x = (∑n∈{n. n > 0 ∧ real n ≤ x}. moebius_mu n / n)"
by (simp add: M_def sum_upto_def)
also from assms True have "{n. n > 0 ∧ real n ≤ x} = {1}"
by auto
thus ?thesis using True by (simp add: M_def sum_upto_def)
next
case False
have "M x = (∑n∈{n. n > 0 ∧ real n ≤ x}. moebius_mu n / n)"
by (simp add: M_def sum_upto_def)
also from False have "{n. n > 0 ∧ real n ≤ x} = {}"
by auto
finally show ?thesis using False by (simp add: M_def)
qed
lemma abs_sum_upto_moebius_mu_over_n_le: "¦M x¦ ≤ 1"
using sum_upto_moebius_mu_over_n_eq[of x] abs_sum_upto_moebius_mu_over_n_less[of x]
by (cases "x < 2") auto
end
end