The asymptotic argument

This file derives Theorem 1.1 and Corollary 1.2 from AsymptoticHalvedWitnessHypothesis. Its only number-theoretic input is prime_between, the prime-number-theorem consequence saying that a prime lies in (x,(1+ε)x) for every sufficiently large x.

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.PrimeIntervalHypothesis : Prop

Abstract form of the sole PNT consequence used in the analytic reduction.

Equations

• MooreBound.DegreeDiameter.PrimeIntervalHypothesis = ∀ {η : ℝ}, 0 < η → ∀ᶠ (x : ℝ) in Filter.atTop, ∃ (p : ℕ), Nat.Prime p ∧ x < ↑p ∧ ↑p < (1 + η) * x

theorem MooreBound.DegreeDiameter.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.tendsto_nat_sub_one_atTop : Filter.Tendsto (fun (d : ℕ) => d - 1) Filter.atTop Filter.atTop

theorem MooreBound.DegreeDiameter.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 quotient r/(r+1) tends to one when r is a fixed positive integral root of a quantity tending to infinity.

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

A positive multiplicative prime gap can be chosen so small that its fixed power loses less than any prescribed amount.

theorem MooreBound.DegreeDiameter.eventually_prime_near_nthRoot (hprime : PrimeIntervalHypothesis) {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)

prime_between pulled back along a growing integral root. The +1 in the conclusion is important: it is what makes the construction's degree cap fit under the ambient degree.

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

The real comparison used in both lower-bound arguments.

Equations

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

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

theorem MooreBound.DegreeDiameter.rootComparison_lt_ratio {m t r p F d : ℕ} (hm : 0 < m) (ht : 0 < t) {η : ℝ} (hη : 0 < η) (hp : ↑r / (1 + η) < ↑p) (hd : d ≤ (r + 1) ^ m) (hdpos : 0 < d) (hF : p ^ (m * t) ≤ F) : (↑r / (↑r + 1) / (1 + η)) ^ (m * t) < ↑F / ↑d ^ t

The elementary comparison which turns a prime near an integral root into a lower bound for an extremal ratio.

theorem MooreBound.DegreeDiameter.eventually_lt_orderRatio (hprime : PrimeIntervalHypothesis) (hw : AsymptoticHalvedWitnessHypothesis) {k : ℕ} (hk : 0 < k) {y : ℝ} (hy : y < 1) : ∀ᶠ (d : ℕ) in Filter.atTop, y < ↑(nKD k d) / ↑d ^ k

Every number below one is eventually below the vertex-extremum ratio.

theorem MooreBound.DegreeDiameter.eventually_lt_edgeRatio (hprime : PrimeIntervalHypothesis) (hw : AsymptoticHalvedWitnessHypothesis) {k : ℕ} (hk : 0 < k) {y : ℝ} (hy : y < 1) : ∀ᶠ (d : ℕ) in Filter.atTop, y < ↑(h (k + 1) d) / ↑d ^ (k + 1)

Every number below one is eventually below the edge-extremum ratio.

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

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

Theorem 1.1: for every fixed positive diameter, the vertex degree--diameter extremum has leading term d^k.

theorem MooreBound.DegreeDiameter.edgeRatio_isBoundedUnder_le (ell : ℕ) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (d : ℕ) => ↑(h ell d) / ↑d ^ ell

theorem MooreBound.DegreeDiameter.corollary_1_2_of_prime_intervals (hprime : PrimeIntervalHypothesis) (hw : AsymptoticHalvedWitnessHypothesis) {ell : ℕ} (hell : 2 ≤ ell) : 1 ≤ Filter.liminf (fun (d : ℕ) => ↑(h ell d) / ↑d ^ ell) Filter.atTop

Corollary 1.2: for every fixed ell ≥ 2, the edge extremum has lower limiting ratio at least one.