Fixed-order divisor means and coefficient square sums

The actual ordered divisor function is the Dirichlet convolution power ζ ^ k. The mean estimate uses only the elementary hyperbola identity and the harmonic sum bound. The square majorant is unrestricted: no squarefree support is needed.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau (k : ℕ) : ArithmeticFunction ℕ

The ordered k-fold divisor function, with the usual value zero at zero.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau k = ArithmeticFunction.zeta ^ k

@[simp]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_zero (k : ℕ) : (fouvryTau k) 0 = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_multiplicative (k : ℕ) : (fouvryTau k).IsMultiplicative

@[simp]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_one (k : ℕ) : (fouvryTau k) 1 = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_order_one {n : ℕ} (hn : n ≠ 0) : (fouvryTau 1) n = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_succ (k n : ℕ) : (fouvryTau (k + 1)) n = ∑ d ∈ n.divisors, (fouvryTau k) d

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_two (n : ℕ) : (fouvryTau 2) n = n.divisors.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_prime_pow {p : ℕ} (hp : Nat.Prime p) (k a : ℕ) : (fouvryTau k) (p ^ a) = k.multichoose a

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_mul_le (k l n : ℕ) : (fouvryTau k) n * (fouvryTau l) n ≤ (fouvryTau (k * l)) n

Products of divisor coefficients are dominated with explicit multiplied order. This holds without any squarefree restriction.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_sq_le (k n : ℕ) : (fouvryTau k) n ^ 2 ≤ (fouvryTau (k ^ 2)) n

The sharp fixed-order square majorant holds for every integer, not merely for squarefree integers.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_pow_le (k r : ℕ) {n : ℕ} (hn : n ≠ 0) : (fouvryTau k) n ^ r ≤ (fouvryTau (k ^ r)) n

All integral moments have an explicit divisor-function majorant. The nonzero hypothesis is needed only for the zeroth moment.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.le_totient_mul_fouvryTau_two (n : ℕ) : n ≤ n.totient * (fouvryTau 2) n

A divisor-sum consequence of ∑ d ∣ n, φ(d) = n.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_div_totient_le (k n : ℕ) : ↑((fouvryTau k) n) / ↑n.totient ≤ ↑((fouvryTau (2 * k)) n) / ↑n

Replace a totient denominator by an ordinary reciprocal while doubling the fixed divisor order.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_fouvryTau_div_le (k N : ℕ) : ∑ n ∈ Finset.Ioc 0 N, ↑((fouvryTau k) n) / ↑n ≤ (1 + Real.log ↑N) ^ k

The reciprocal mean needed when paying modulus weights. Order zero is allowed in this estimate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_fouvryTau_div_le_real (k : ℕ) {x : ℝ} (hx : 1 ≤ x) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, ↑((fouvryTau k) n) / ↑n ≤ (1 + Real.log x) ^ k

Reciprocal divisor means at a real endpoint.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_fouvryTau_div_totient_le_real (k : ℕ) {x : ℝ} (hx : 1 ≤ x) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, ↑((fouvryTau k) n) / ↑n.totient ≤ (1 + Real.log x) ^ (2 * k)

A global totient-weighted divisor mean, with no order-dependent implicit constant.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_fouvryTau_sq_div_le_real (k : ℕ) {x : ℝ} (hx : 1 ≤ x) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, ↑((fouvryTau k) n) ^ 2 / ↑n ≤ (1 + Real.log x) ^ k ^ 2

The reciprocal second moment, useful for sums of modulus weights.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_fouvryTau_sq_div_totient_le_real (k : ℕ) {x : ℝ} (hx : 1 ≤ x) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, ↑((fouvryTau k) n) ^ 2 / ↑n.totient ≤ (1 + Real.log x) ^ (2 * k ^ 2)

Totient-weighted second moments also retain a fixed logarithm exponent.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_fouvryTau_le (k N : ℕ) : ∑ n ∈ Finset.Ioc 0 N, ↑((fouvryTau (k + 1)) n) ≤ ↑N * (1 + Real.log ↑N) ^ k

The global mean has logarithm exponent exactly one less than the order.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_fouvryTau_le_real {k : ℕ} (hk : 1 ≤ k) {x : ℝ} (hx : 1 ≤ x) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, ↑((fouvryTau k) n) ≤ x * (1 + Real.log x) ^ (k - 1)

Real-endpoint form, uniform in x, with the order kept explicit.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_fouvryTau_pow_le_real {k : ℕ} (hk : 1 ≤ k) (r : ℕ) {x : ℝ} (hx : 1 ≤ x) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, ↑((fouvryTau k) n) ^ r ≤ x * (1 + Real.log x) ^ (k ^ r - 1)

Every fixed integral moment has a global logarithmic bound.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_fouvryTau_sq_le_real {k : ℕ} (hk : 1 ≤ k) {x : ℝ} (hx : 1 ≤ x) : ∑ n ∈ Finset.Ioc 0 ⌊x⌋₊, ↑((fouvryTau k) n) ^ 2 ≤ x * (1 + Real.log x) ^ (k ^ 2 - 1)

Unrestricted second moment with logarithm exponent k² - 1.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_alpha_sq_le_fouvryTau {k : ℕ} (hk : 1 ≤ k) {x : ℝ} (hx : 1 ≤ x) (S : Finset ℕ) (hS : S ⊆ Finset.Ioc 0 ⌊x⌋₊) (α : ℕ → ℝ) (hα : ∀ n ∈ S, |α n| ≤ ↑((fouvryTau k) n)) : ∑ n ∈ S, α n ^ 2 ≤ x * (1 + Real.log x) ^ (k ^ 2 - 1)

The coefficient square sum required by dispersion, for arbitrary finite support and signed coefficients dominated by the actual divisor function.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_alpha_sq_dyadic_le {k : ℕ} (hk : 1 ≤ k) {M : ℝ} (hM : 1 ≤ M) (S : Finset ℕ) (hS : ∀ n ∈ S, M ≤ ↑n ∧ ↑n ≤ 2 * M) (α : ℕ → ℝ) (hα : ∀ n ∈ S, |α n| ≤ ↑((fouvryTau k) n)) : ∑ n ∈ S, α n ^ 2 ≤ 2 * M * (1 + Real.log (2 * M)) ^ (k ^ 2 - 1)

Direct dyadic alpha payment; the constant is independent of the scale, the finite support, and the coefficients.