Consequences of the polynomial bound

def EGZ.atTopAlongPrimes : Filter ℕ

The filter for a natural number tending to infinity through prime values.

Equations

• EGZ.atTopAlongPrimes = Filter.atTop ⊓ Filter.principal {p : ℕ | Nat.Prime p}

def EGZ.MainUpperBound (d : ℕ) : Prop

The upper-bound form used in Section 9 of the paper. Together with the elementary lower bound hollowConstant p d * (p - 1) + 1 ≤ egzConstant p d and a bound on hollowConstant p d that is uniform in p for fixed d (Proposition thw in the paper), this implies the little-o formulation of Theorem 1.2.

Equations

• EGZ.MainUpperBound d = ∀ (ε : ℝ), 0 < ε → ∀ᶠ (p : ℕ) in EGZ.atTopAlongPrimes, ↑(EGZ.egzConstant p d) ≤ (↑(EGZ.hollowConstant p d) + ε) * ↑p

def EGZ.MainAsymptotic (d : ℕ) : Prop

The direct little-o formulation of Theorem 1.2.

Equations

• EGZ.MainAsymptotic d = (fun (p : ℕ) => ↑(EGZ.egzConstant p d) - ↑p * ↑(EGZ.hollowConstant p d)) =o[EGZ.atTopAlongPrimes] fun (p : ℕ) => ↑p

theorem EGZ.eventually_hollowConstant_le_choose_add_one (d : ℕ) (hd : 1 ≤ d) : ∀ᶠ (p : ℕ) in atTopAlongPrimes, hollowConstant p d ≤ (2 * d - 1).choose d + 1

The polynomial-method bound holds eventually (in fact, pointwise) along the primes.

theorem EGZ.isLittleO_natCast_of_eventually_norm_le {f : ℕ → ℝ} {C : ℝ} (hC : ∀ᶠ (p : ℕ) in atTopAlongPrimes, ‖f p‖ ≤ C) : f =o[atTopAlongPrimes] fun (p : ℕ) => ↑p

A uniformly bounded real-valued function is o(p) as p → ∞ along the prime filter.

noncomputable def EGZ.elementaryHollowLowerBound (p d : ℕ) : ℕ

The explicit lower benchmark furnished by an extremal hollow family.

Equations

• EGZ.elementaryHollowLowerBound p d = EGZ.hollowConstant p d * (p - 1) + 1

theorem EGZ.elementaryHollowLowerBound_le_egzConstant {p d : ℕ} (hp : Nat.Prime p) : elementaryHollowLowerBound p d ≤ egzConstant p d

theorem EGZ.elementaryHollowLowerBound_error_isLittleO (d : ℕ) (hd : 1 ≤ d) : (fun (p : ℕ) => ↑p * ↑(hollowConstant p d) - ↑(elementaryHollowLowerBound p d)) =o[atTopAlongPrimes] fun (p : ℕ) => ↑p

The elementary hollow-family lower benchmark differs from p * w by o(p), thanks to the uniform polynomial-method bound on w.

The asymptotic bridge

theorem EGZ.eventually_neg_mul_le_mainError (d : ℕ) (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (p : ℕ) in atTopAlongPrimes, -ε * ↑p ≤ ↑(egzConstant p d) - ↑p * ↑(hollowConstant p d)

The elementary lower bound gives the lower half of the asymptotic squeeze.

theorem EGZ.mainAsymptotic_of_mainUpperBound (d : ℕ) (hd : 1 ≤ d) (hUpper : MainUpperBound d) : MainAsymptotic d

Once the paper's upper estimate is available, the elementary lower estimate and the polynomial bound complete Theorem 1.2.