A Dirichlet moment bound uniform in the moment order

For fixed Q,t, the bound has the form L_q(σ) ≤ (Kq)^q (σ−1)^(−(2^t−t+t/q)). The same constants work for every eligible integer moment order.

theorem NairTenenbaum.exists_irreducible_hooley_reduced_uniform_bound {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {t : ℝ} (ht : 1 ≤ t) : ∃ (K : ℝ) (C : ℝ) (b : ℝ), 1 ≤ K ∧ 0 ≤ C ∧ 1 < b ∧ b ≤ 2 ∧ (∀ (σ : ℝ), 1 < σ → σ ≤ b → rootPrimePowerSum Q σ ≤ C - Real.log (σ - 1)) ∧ ∀ (q : ℕ), 2 < q → 2 * t ≤ ↑q → ∀ (σ : ℝ), 1 < σ → σ ≤ b → hooleyReducedMoment Q t q σ ≤ K * ↑q * (σ - 1) ^ (-hooleyMomentExponentGap t q)

theorem NairTenenbaum.exp_mul_momentPower_le {K C t : ℝ} (hK : 1 ≤ K) (hC : 0 ≤ C) {q : ℕ} (hq : 1 ≤ q) (htq : t ≤ ↑q) : Real.exp (2 ^ (t / ↑q) * C) * (K * ↑q) ^ (↑q - 1) ≤ (Real.exp (2 * C) * K * ↑q) ^ q

theorem NairTenenbaum.exists_irreducible_hooleyDirichlet_power_bound {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) (hirr : Irreducible (Polynomial.map (Int.castRingHom ℚ) Q)) {t : ℝ} (ht : 1 ≤ t) : ∃ (K : ℝ) (b : ℝ), 1 ≤ K ∧ 1 < b ∧ b ≤ 2 ∧ ∀ (q : ℕ), 2 < q → 2 * t ≤ ↑q → ∀ (σ : ℝ), 1 < σ → σ ≤ b → hooleyDirichlet Q t q σ ≤ (K * ↑q) ^ q * (σ - 1) ^ (-(2 ^ t - t + t / ↑q))