The graph-family asymptotics in Proposition 3.1

This file proves equation (9) for the actual halved flag graphs, indexed by PrimePowerIndex. Thus atTop means that the field cardinality tends to infinity through all prime powers, as proved by tendsto_primePowerIndex_val.

The proof follows the write-up. Exact flag enumeration first shows that the order divided by the k-th power of the displayed degree cap tends to one. The Moore bound and regularity then squeeze the actual common degree against that cap. Substitution gives the second displayed asymptotic.

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.proposition31Amplitude (q k : ℕ) : ℕ

The factor A_q = (q+1)^k in Proposition 3.1.

Equations

• MooreBound.DegreeDiameter.proposition31Amplitude q k = (q + 1) ^ k

def MooreBound.DegreeDiameter.proposition31DegreeCap (q k : ℕ) : ℕ

The sharp displayed degree cap K_q = (q+1)^k ((q+1)^k-1).

Equations

• MooreBound.DegreeDiameter.proposition31DegreeCap q k = MooreBound.DegreeDiameter.proposition31Amplitude q k * (MooreBound.DegreeDiameter.proposition31Amplitude q k - 1)

@[reducible, inline]

noncomputable abbrev MooreBound.DegreeDiameter.proposition31PrimePowerOrder (k : ℕ) (q : PrimePowerIndex) : ℕ

The order of the concrete graph over the chosen field of order q.

Equations

• MooreBound.DegreeDiameter.proposition31PrimePowerOrder k q = Nat.card (MooreBound.DegreeDiameter.Proposition31Vertex (MooreBound.DegreeDiameter.PrimePowerField q) k)

@[reducible, inline]

noncomputable abbrev MooreBound.DegreeDiameter.proposition31PrimePowerDegree (k : ℕ) (q : PrimePowerIndex) : ℕ

The actual common degree of the concrete graph over the chosen field of order q.

Equations

• MooreBound.DegreeDiameter.proposition31PrimePowerDegree k q = MooreBound.DegreeDiameter.proposition31Degree (MooreBound.DegreeDiameter.PrimePowerField q) k

Polynomial form of exact flag enumeration

noncomputable def MooreBound.DegreeDiameter.proposition31QIntegerPolynomial (n : ℕ) : Polynomial ℝ

The real polynomial 1 + X + ... + X^(n-1).

Equations

• MooreBound.DegreeDiameter.proposition31QIntegerPolynomial n = ∑ i ∈ Finset.range n, Polynomial.X ^ i

noncomputable def MooreBound.DegreeDiameter.proposition31QFactorialPolynomial (n : ℕ) : Polynomial ℝ

The real polynomial whose value at a natural number q is qFactorial q n.

Equations

• MooreBound.DegreeDiameter.proposition31QFactorialPolynomial n = ∏ i ∈ Finset.range n, MooreBound.DegreeDiameter.proposition31QIntegerPolynomial (i + 1)

noncomputable def MooreBound.DegreeDiameter.proposition31AmplitudePolynomial (k : ℕ) : Polynomial ℝ

The polynomial (X+1)^k.

Equations

• MooreBound.DegreeDiameter.proposition31AmplitudePolynomial k = (Polynomial.X + 1) ^ k

noncomputable def MooreBound.DegreeDiameter.proposition31CapPolynomial (k : ℕ) : Polynomial ℝ

The polynomial version of the sharp degree cap.

Equations

• MooreBound.DegreeDiameter.proposition31CapPolynomial k = MooreBound.DegreeDiameter.proposition31AmplitudePolynomial k * (MooreBound.DegreeDiameter.proposition31AmplitudePolynomial k - 1)

noncomputable def MooreBound.DegreeDiameter.proposition31DenominatorPolynomial (k : ℕ) : Polynomial ℝ

The denominator polynomial A_q K_q^k occurring after the exact multiplication count is substituted into N_q / K_q^k.

Equations

• MooreBound.DegreeDiameter.proposition31DenominatorPolynomial k = MooreBound.DegreeDiameter.proposition31AmplitudePolynomial k * MooreBound.DegreeDiameter.proposition31CapPolynomial k ^ k

@[simp]

theorem MooreBound.DegreeDiameter.proposition31_eval_qIntegerPolynomial (x : ℝ) (n : ℕ) : Polynomial.eval x (proposition31QIntegerPolynomial n) = ∑ i ∈ Finset.range n, x ^ i

theorem MooreBound.DegreeDiameter.proposition31_eval_qIntegerPolynomial_nat (q n : ℕ) : Polynomial.eval (↑q) (proposition31QIntegerPolynomial n) = ↑(qInteger q n)

theorem MooreBound.DegreeDiameter.proposition31_qIntegerPolynomial_monic {n : ℕ} (hn : n ≠ 0) : (proposition31QIntegerPolynomial n).Monic

theorem MooreBound.DegreeDiameter.proposition31_qIntegerPolynomial_natDegree_succ (n : ℕ) : (proposition31QIntegerPolynomial (n + 1)).natDegree = n

@[simp]

theorem MooreBound.DegreeDiameter.proposition31_eval_qFactorialPolynomial_nat (q n : ℕ) : Polynomial.eval (↑q) (proposition31QFactorialPolynomial n) = ↑(qFactorial q n)

theorem MooreBound.DegreeDiameter.proposition31_qFactorialPolynomial_monic (n : ℕ) : (proposition31QFactorialPolynomial n).Monic

theorem MooreBound.DegreeDiameter.proposition31_qFactorialPolynomial_natDegree_eq_sum (n : ℕ) : (proposition31QFactorialPolynomial n).natDegree = ∑ i ∈ Finset.range n, i

theorem MooreBound.DegreeDiameter.proposition31_qFactorialPolynomial_natDegree_odd (k : ℕ) : (proposition31QFactorialPolynomial (2 * k + 1)).natDegree = 2 * k * k + k

theorem MooreBound.DegreeDiameter.proposition31_amplitudePolynomial_monic (k : ℕ) : (proposition31AmplitudePolynomial k).Monic

@[simp]

theorem MooreBound.DegreeDiameter.proposition31_amplitudePolynomial_natDegree (k : ℕ) : (proposition31AmplitudePolynomial k).natDegree = k

theorem MooreBound.DegreeDiameter.proposition31_amplitudePolynomial_sub_one_monic {k : ℕ} (hk : 0 < k) : (proposition31AmplitudePolynomial k - 1).Monic

@[simp]

theorem MooreBound.DegreeDiameter.proposition31_amplitudePolynomial_sub_one_natDegree {k : ℕ} (hk : 0 < k) : (proposition31AmplitudePolynomial k - 1).natDegree = k

theorem MooreBound.DegreeDiameter.proposition31_capPolynomial_monic {k : ℕ} (hk : 0 < k) : (proposition31CapPolynomial k).Monic

@[simp]

theorem MooreBound.DegreeDiameter.proposition31_capPolynomial_natDegree {k : ℕ} (hk : 0 < k) : (proposition31CapPolynomial k).natDegree = 2 * k

theorem MooreBound.DegreeDiameter.proposition31_denominatorPolynomial_monic {k : ℕ} (hk : 0 < k) : (proposition31DenominatorPolynomial k).Monic

@[simp]

theorem MooreBound.DegreeDiameter.proposition31_denominatorPolynomial_natDegree {k : ℕ} (hk : 0 < k) : (proposition31DenominatorPolynomial k).natDegree = 2 * k * k + k

@[simp]

theorem MooreBound.DegreeDiameter.proposition31_eval_amplitudePolynomial_nat (q k : ℕ) : Polynomial.eval (↑q) (proposition31AmplitudePolynomial k) = ↑(proposition31Amplitude q k)

@[simp]

theorem MooreBound.DegreeDiameter.proposition31_eval_capPolynomial_nat (q k : ℕ) : Polynomial.eval (↑q) (proposition31CapPolynomial k) = ↑(proposition31DegreeCap q k)

@[simp]

theorem MooreBound.DegreeDiameter.proposition31_eval_denominatorPolynomial_nat (q k : ℕ) : Polynomial.eval (↑q) (proposition31DenominatorPolynomial k) = ↑(proposition31Amplitude q k * proposition31DegreeCap q k ^ k)

theorem MooreBound.DegreeDiameter.proposition31_qFactorial_div_denominator_tendsto_one (k : ℕ) (hk : 0 < k) : Filter.Tendsto (fun (x : ℝ) => Polynomial.eval x (proposition31QFactorialPolynomial (2 * k + 1)) / Polynomial.eval x (proposition31DenominatorPolynomial k)) Filter.atTop (nhds 1)

Exact q-factorial enumeration and the cap have the same monic leading term after the multiplication count is substituted.

theorem MooreBound.DegreeDiameter.proposition31_qFactorial_div_capDenominator_tendsto_one (k : ℕ) (hk : 0 < k) : Filter.Tendsto (fun (q : PrimePowerIndex) => ↑(qFactorial (↑q) (2 * k + 1)) / ↑(proposition31Amplitude (↑q) k * proposition31DegreeCap (↑q) k ^ k)) Filter.atTop (nhds 1)

The purely algebraic ratio, restricted from all real q to prime-power cardinalities.

Exact order versus the cap

theorem MooreBound.DegreeDiameter.proposition31_order_div_cap_pow_tendsto_one (k : ℕ) (hk : 0 < k) : Filter.Tendsto (fun (q : PrimePowerIndex) => ↑(proposition31PrimePowerOrder k q) / ↑(proposition31DegreeCap (↑q) k) ^ k) Filter.atTop (nhds 1)

The exact graph order divided by the k-th power of the displayed cap tends to one. This is the algebraic input to the Moore squeeze.

The Moore squeeze for the actual common degree

theorem MooreBound.DegreeDiameter.proposition31_degree_div_cap_tendsto_one (k : ℕ) (hk : 0 < k) : Filter.Tendsto (fun (q : PrimePowerIndex) => ↑(proposition31Degree (PrimePowerField q) k) / ↑(proposition31DegreeCap (↑q) k)) Filter.atTop (nhds 1)

First asymptotic in Proposition 3.1, equation (9). For fixed positive k, the actual common degree of the concrete graph is asymptotic to the paper's sharp cap as q tends to infinity through prime powers.

theorem MooreBound.DegreeDiameter.proposition31_order_div_degree_pow_tendsto_one (k : ℕ) (hk : 0 < k) : Filter.Tendsto (fun (q : PrimePowerIndex) => ↑(Nat.card (Proposition31Vertex (PrimePowerField q) k)) / ↑(proposition31Degree (PrimePowerField q) k) ^ k) Filter.atTop (nhds 1)

Second asymptotic in Proposition 3.1, equation (9). For fixed positive k, the exact order of the concrete graph is asymptotic to the k-th power of its actual common degree as q tends to infinity through prime powers.