Main degree--diameter consequences

These wrappers discharge the abstract prime-interval premise of the analytic reduction using the proved prime-number-theorem consequence prime_between. Thus the only remaining hypothesis of the exported results is the finite-geometry construction AsymptoticHalvedWitnessHypothesis.

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

theorem MooreBound.DegreeDiameter.primeIntervalHypothesis_of_primeNumberTheorem : PrimeIntervalHypothesis

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

Theorem 1.1 reduced to the halved-flag construction.

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

Corollary 1.2 reduced to the halved-flag construction.