Constants uniform in the Hooley moment order

After division by the exponent gap, the integrated coefficient grows at most linearly in q. This is the dependence needed for the sharp optimization.

theorem NairTenenbaum.rpow_le_max_one_self {x u : ℝ} (hx : 0 ≤ x) (hu : 0 ≤ u) (hu₁ : u ≤ 1) : x ^ u ≤ max 1 x

noncomputable def NairTenenbaum.hooleyPoleUniformConstant (Q : Polynomial ℤ) (t C : ℝ) : ℝ

A pole-bound constant uniform in the permitted moment orders.

Equations

• NairTenenbaum.hooleyPoleUniformConstant Q t C = max 1 (↑Q.natDegree * (Real.log 4 * Real.exp 2)) * 4 ^ t * max 1 (2 * ↑Q.natDegree * (Real.log 4 * Real.exp 2)) * Real.exp (2 ^ t * C)

theorem NairTenenbaum.hooleyPoleUniformConstant_nonneg (Q : Polynomial ℤ) (t C : ℝ) : 0 ≤ hooleyPoleUniformConstant Q t C

theorem NairTenenbaum.hooleyPrimeErrorConstant_rpow_le (Q : Polynomial ℤ) {t : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 0 < q) (htq : t ≤ ↑q) : hooleyPrimeErrorConstant Q q ^ (t / ↑q) ≤ max 1 (↑Q.natDegree * (Real.log 4 * Real.exp 2)) * 4 ^ t

theorem NairTenenbaum.hooleyPoleCoefficient_le_uniform (Q : Polynomial ℤ) {t C : ℝ} (ht : 0 ≤ t) (hC : 0 ≤ C) {q : ℕ} (hq : 2 < q) (htq : t ≤ ↑q) : hooleyPoleCoefficient Q t q C ≤ hooleyPoleUniformConstant Q t C / (↑q - 1)

theorem NairTenenbaum.hooleyPoleCoefficient_div_gap_le (Q : Polynomial ℤ) {t C : ℝ} (ht : 1 ≤ t) (hC : 0 ≤ C) {q : ℕ} (hq : 2 < q) (hqt : 2 * t ≤ ↑q) : hooleyPoleCoefficient Q t q C / hooleyMomentExponentGap t q ≤ 7 * hooleyPoleUniformConstant Q t C * ↑q

theorem NairTenenbaum.hooleyReducedMoment_le_endpoint_uniform {Q : Polynomial ℤ} (hQ : NoFixedPrimeDivisor Q) {t b : ℝ} (ht : 0 ≤ t) {q : ℕ} (hq : 2 < q) (hb : 1 < b) : hooleyReducedMoment Q t q b ≤ Real.exp (2 ^ t * rootPrimePowerSum Q b)