Squarefree coefficients of the Hooley moment Dirichlet series

The subpolynomial bound is uniform in the positive integral moment order. This uniformity permits choosing that order later in the mean-value proof.

theorem NairTenenbaum.hooleyMoment_rpow_le_card_rpow (n : ℕ) {q : ℕ} (hq : 0 < q) {t : ℝ} (ht : 0 ≤ t) : hooleyMoment q n ^ (t / ↑q) ≤ ↑n.divisors.card ^ t

theorem NairTenenbaum.card_divisors_of_squarefree {n : ℕ} (hn : Squarefree n) : n.divisors.card = 2 ^ n.primeFactors.card

noncomputable def NairTenenbaum.hooleyMomentCoefficient (Q : Polynomial ℤ) (t : ℝ) (q n : ℕ) : ℝ

The asterisk in the source Dirichlet series means squarefree support.

Equations

• NairTenenbaum.hooleyMomentCoefficient Q t q n = if Squarefree n then NairTenenbaum.hooleyMoment q n ^ (t / ↑q) * ↑(NairTenenbaum.rootCount Q n) else 0

theorem NairTenenbaum.hooleyMomentCoefficient_nonneg (Q : Polynomial ℤ) (t : ℝ) (q n : ℕ) : 0 ≤ hooleyMomentCoefficient Q t q n

@[simp]

theorem NairTenenbaum.hooleyMomentCoefficient_zero (Q : Polynomial ℤ) (t : ℝ) (q : ℕ) : hooleyMomentCoefficient Q t q 0 = 0

@[simp]

theorem NairTenenbaum.hooleyMoment_at_one {q : ℕ} (hq : 0 < q) : hooleyMoment q 1 = 1

@[simp]

theorem NairTenenbaum.hooleyMomentCoefficient_one (Q : Polynomial ℤ) (t : ℝ) {q : ℕ} (hq : 0 < q) : hooleyMomentCoefficient Q t q 1 = 1

theorem NairTenenbaum.exists_hooleyMomentCoefficient_le_rpow (g : ℝ) {t η : ℝ} (ht : 0 ≤ t) (hη : 0 < η) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (Q : Polynomial ℤ), NoFixedPrimeDivisor Q → ↑Q.natDegree ≤ g → ∀ (q : ℕ), 0 < q → ∀ (n : ℕ), hooleyMomentCoefficient Q t q n ≤ C * ↑n ^ η

Uniformity includes the polynomial coefficients and the moment order q.