Sums of the Möbius function over divisors

Restricted Möbius sums over divisors and divisor antidiagonals, and the equal-size sign partition of the divisors of a squarefree number.

Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.

theorem beta_radical (n k n' : ℕ) (hn : 1 ≤ n) (hn' : n' = UniqueFactorizationMonoid.radical n) (hk : n = k * n') (F : ℕ → ℚ) : ∏ x ∈ n.divisorsAntidiagonal, F x.2 ^ ArithmeticFunction.moebius x.1 = ∏ t ∈ n'.divisors, F (k * t) ^ ArithmeticFunction.moebius (n' / t)

Rewrites the antidiagonal Möbius product ∏_{ed = n} F d ^ μ e as a product over the divisors of the radical n' = rad n: ∏_{t ∣ n'} F (k t) ^ μ (n'/t), where k = n / n'.

theorem moebius_antidiag_sum_zero (n : ℕ) (hn : 2 ≤ n) : ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 = 0

∑_{ed = n} μ e = 0 for n ≥ 2: the Möbius function is the Dirichlet inverse of ζ.

theorem moebius_sign_partition (n' : ℕ) (hn'1 : 1 < n') (hsf : Squarefree n') : ∃ (Sp : Finset ℕ) (Sm : Finset ℕ), Disjoint Sp Sm ∧ Sp ∪ Sm = n'.divisors ∧ Sp.card = Sm.card ∧ (∀ t ∈ Sp, ArithmeticFunction.moebius (n' / t) = 1) ∧ ∀ t ∈ Sm, ArithmeticFunction.moebius (n' / t) = -1

For squarefree n' > 1, the divisors of n' split into two halves of equal size according to the sign of μ(n'/t).

theorem prod_pow_moebius_eq_div (n k n' : ℕ) (hn : 1 ≤ n) (hn' : n' = UniqueFactorizationMonoid.radical n) (hk : n = k * n') (F : ℕ → ℚ) {Sp Sm : Finset ℕ} (hdisj : Disjoint Sp Sm) (hunion : Sp ∪ Sm = n'.divisors) (hSp : ∀ t ∈ Sp, ArithmeticFunction.moebius (n' / t) = 1) (hSm : ∀ t ∈ Sm, ArithmeticFunction.moebius (n' / t) = -1) : ∏ x ∈ n.divisorsAntidiagonal, F x.2 ^ ArithmeticFunction.moebius x.1 = (∏ t ∈ Sp, F (k * t)) / ∏ t ∈ Sm, F (k * t)

Under a sign partition (Sp, Sm) of the divisors of n' = rad n (as produced by moebius_sign_partition), the antidiagonal Möbius product ∏_{ed = n} F d ^ μ e splits as the quotient (∏_{t ∈ Sp} F (k t)) / (∏_{t ∈ Sm} F (k t)), where k = n / n'.

theorem moebius_restricted_sum (m n : ℕ) (hm : 1 ≤ m) (hn : 1 ≤ n) (hmn : m ∣ n) : ∑ x ∈ n.divisorsAntidiagonal with m ∣ x.2, ArithmeticFunction.moebius x.1 = if n = m then 1 else 0

The Möbius sum over antidiagonal pairs (e, d) with m ∣ d is 1 if n = m and 0 otherwise (assuming m ∣ n, m, n ≥ 1).

theorem indicator_moebius_nonneg (g : ℕ → ℕ) (hmin : ∀ x ≥ 1, ∀ y ≥ 1, g (x.gcd y) = min (g x) (g y)) (n : ℕ) (hn : 1 ≤ n) (k : ℕ) : 0 ≤ ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 * if k ≤ g x.2 then 1 else 0

For a level set {d : k ≤ g d} of a gcd-min function g, the antidiagonal Möbius transform of its indicator (in the second coordinate) over n is 0 or 1; in particular nonnegative.

theorem moebius_transform_nonneg (g : ℕ → ℕ) (hmin : ∀ x ≥ 1, ∀ y ≥ 1, g (x.gcd y) = min (g x) (g y)) (n : ℕ) (hn : 1 ≤ n) : 0 ≤ ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 * ↑(g x.2)

Nonnegativity of the Möbius transform of a gcd-min function. If g satisfies g (gcd x y) = min (g x) (g y), then ∑_{ed = n} μ e · g d ≥ 0. This is the arithmetic core of the integrality of the Möbius factors of a strong divisibility sequence.