Theorem 1.1 directly from Proposition 3.1

This module follows the dependency route in the paper. For every large ambient degree d, the prime-number theorem supplies a prime p just below the (2k)-th root of d. The concrete graph Proposition31Graph over the field of order p has degree at most its displayed cap, and that cap is at most d. Its exact order-to-cap asymptotic then gives the lower bound. The Moore bound gives the matching upper bound.

Lean Pool port of wewantmoore commit d59bd80ea93fabb9faf769e790ab47692645e022. The port adds a namespace and adapts proofs to the current Mathlib APIs and repository style.

def MooreBound.DegreeDiameter.proposition31PrimePowerIndexOfPrime (p : ℕ) (hp : Nat.Prime p) : PrimePowerIndex

A prime, viewed as one of the prime-power field orders used in Proposition 3.1.

Equations

• MooreBound.DegreeDiameter.proposition31PrimePowerIndexOfPrime p hp = ⟨p, ⋯⟩

@[simp]

theorem MooreBound.DegreeDiameter.proposition31PrimePowerIndexOfPrime_val (p : ℕ) (hp : Nat.Prime p) : ↑(proposition31PrimePowerIndexOfPrime p hp) = p

instance MooreBound.DegreeDiameter.proposition31PrimePowerIndex_nonempty : Nonempty PrimePowerIndex

theorem MooreBound.DegreeDiameter.proposition31_cap_le_succ_pow_two_mul (q : PrimePowerIndex) (k : ℕ) : proposition31DegreeCap (↑q) k ≤ (↑q + 1) ^ (2 * k)

The cap is bounded above by the power used to fit the construction below an ambient degree.

theorem MooreBound.DegreeDiameter.proposition31_pow_two_mul_le_cap (q : PrimePowerIndex) (k : ℕ) (hk : 0 < k) : ↑q ^ (2 * k) ≤ proposition31DegreeCap (↑q) k

For positive k, the cap also dominates q^(2k). This is the scale comparison needed after choosing a prime close to the relevant root.

theorem MooreBound.DegreeDiameter.proposition31_orderAdmissible (q : PrimePowerIndex) (k : ℕ) (hk : 0 < k) {d : ℕ} (hcap : proposition31DegreeCap (↑q) k ≤ d) : OrderAdmissible k d (proposition31PrimePowerOrder k q)

The concrete graph in Proposition 3.1 is admissible whenever its displayed cap is at most the ambient maximum degree. In particular, this lemma uses the actual common degree and the exact diameter of that graph.

Prime interpolation

theorem MooreBound.DegreeDiameter.proposition31_tendsto_nthRoot_comp_atTop {D : ℕ → ℕ} (hD : Filter.Tendsto D Filter.atTop Filter.atTop) {m : ℕ} (hm : 0 < m) : Filter.Tendsto (fun (d : ℕ) => m.nthRoot (D d)) Filter.atTop Filter.atTop

Taking a fixed positive integral root preserves divergence to infinity.

theorem MooreBound.DegreeDiameter.proposition31_tendsto_nthRoot_div_add_one {D : ℕ → ℕ} (hD : Filter.Tendsto D Filter.atTop Filter.atTop) {m : ℕ} (hm : 0 < m) : Filter.Tendsto (fun (d : ℕ) => ↑(m.nthRoot (D d)) / (↑(m.nthRoot (D d)) + 1)) Filter.atTop (nhds 1)

The small root-normalization factor which occurs in the interpolation argument tends to one.

theorem MooreBound.DegreeDiameter.proposition31_exists_pos_inv_one_add_pow_gt {M : ℕ} {y : ℝ} (hy : y < 1) : ∃ (η : ℝ), 0 < η ∧ y < (1 + η)⁻¹ ^ M

A positive multiplicative prime gap can be made small enough for any fixed power.

theorem MooreBound.DegreeDiameter.proposition31_eventually_prime_near_nthRoot {D : ℕ → ℕ} (hD : Filter.Tendsto D Filter.atTop Filter.atTop) {m : ℕ} (hm : 0 < m) {η : ℝ} (hη : 0 < η) : ∀ᶠ (d : ℕ) in Filter.atTop, ∃ (p : ℕ), Nat.Prime p ∧ ↑(m.nthRoot (D d)) / (1 + η) < ↑p ∧ p + 1 ≤ m.nthRoot (D d)

The PNT prime interval pulled back along a growing integral root.

noncomputable def MooreBound.DegreeDiameter.proposition31RootComparison (D : ℕ → ℕ) (m t : ℕ) (η : ℝ) (d : ℕ) : ℝ

The root comparison factor used in the lower bound.

Equations

• MooreBound.DegreeDiameter.proposition31RootComparison D m t η d = (↑(m.nthRoot (D d)) / (↑(m.nthRoot (D d)) + 1) / (1 + η)) ^ (m * t)

theorem MooreBound.DegreeDiameter.proposition31_tendsto_rootComparison {D : ℕ → ℕ} (hD : Filter.Tendsto D Filter.atTop Filter.atTop) {m : ℕ} (hm : 0 < m) (t : ℕ) {η : ℝ} (_hη : 0 < η) : Filter.Tendsto (proposition31RootComparison D m t η) Filter.atTop (nhds ((1 + η)⁻¹ ^ (m * t)))

The lower and upper extremal comparisons

theorem MooreBound.DegreeDiameter.proposition31_mul_rootComparison_lt_order_ratio (q : PrimePowerIndex) {k r d : ℕ} (hk : 0 < k) {η s : ℝ} (hη : 0 < η) (hs : 0 < s) (hqLower : ↑r / (1 + η) < ↑↑q) (hrPos : 0 < r) (hdUpper : d ≤ (r + 1) ^ (2 * k)) (hdPos : 0 < d) (horder : s < ↑(proposition31PrimePowerOrder k q) / ↑(proposition31DegreeCap (↑q) k) ^ k) : s * (↑r / (↑r + 1) / (1 + η)) ^ (2 * k * k) < ↑(proposition31PrimePowerOrder k q) / ↑d ^ k

The pointwise multiplication step combining the exact order/cap ratio with the PNT scale comparison.

theorem MooreBound.DegreeDiameter.proposition31_tendsto_orderRatio_upper (k : ℕ) : Filter.Tendsto (fun (d : ℕ) => (1 + (↑d)⁻¹) ^ k) Filter.atTop (nhds 1)

theorem MooreBound.DegreeDiameter.theorem_1_1_from_proposition_3_1 {k : ℕ} (hk : 0 < k) : Filter.Tendsto (fun (d : ℕ) => ↑(nKD k d) / ↑d ^ k) Filter.atTop (nhds 1)

Theorem 1.1, directly from Proposition 3.1.