Documentation

LeanPool.NaslundCounterexample.Asymptotics

The growth rate #

D_3(n) is the largest size of a square-difference-free set of polynomials of degree below n. It is nondecreasing, at most 3^n, and at least 810^e at n = 8e by the first family. Writing L = log 810 / log 3, the three facts give

log D_3(n) / (n log 3) ≥ (1/8 - 1/n) · L for n ≥ 8,

so the lower limit of the left side is at least L/8. Finally 16/21 ≤ L/8 is the natural-number comparison 3^128 ≤ 810^21, and 16/21 = 0.76190… is the stated bound.

source
theorem NaslundCounterexample.mem_polynomialsBelow (n : ℕ) (f : Polynomial (ZMod 3)) :
f ∈ polynomialsBelow n ↔ f.degree < ↑n

The finite set polynomialsBelow n is exactly the set of polynomials of degree below n.

source
theorem NaslundCounterexample.polynomialsBelow_card_le (n : ℕ) :
(polynomialsBelow n).card ≤ 3 ^ n

There are at most 3^n polynomials of degree below n.

source
theorem NaslundCounterexample.polynomialsBelow_mono {n n' : ℕ} (h : n ≤ n') :
polynomialsBelow n ⊆ polynomialsBelow n'

The polynomials of degree below n sit inside those of degree below n' for n ≤ n'.

source
theorem NaslundCounterexample.card_le_maximumCardinality {n : ℕ} {A : Finset (Polynomial (ZMod 3))} (hA : AllBelow n A) (hS : SquareDifferenceFree A) :
A.card ≤ maximumCardinality n

Every square-difference-free set of polynomials of degree below n is counted by D_3(n).

source
theorem NaslundCounterexample.maximumCardinality_mono :
Monotone maximumCardinality

D_3 is nondecreasing.

source
theorem NaslundCounterexample.maximumCardinality_le (n : ℕ) :
maximumCardinality n ≤ 3 ^ n

D_3(n) ≤ 3^n, the trivial upper bound.

source
theorem NaslundCounterexample.one_le_maximumCardinality (n : ℕ) :
1 ≤ maximumCardinality n

D_3(n) ≥ 1, witnessed by the one-element set {0}.

source
theorem NaslundCounterexample.pow_le_maximumCardinality (e : ℕ) :
810 ^ e ≤ maximumCardinality (8 * e)

The first family gives D_3(8e) ≥ 810^e.

source
noncomputable def NaslundCounterexample.growthExponent :
ℝ

The exponent supplied by repeated degree-eight lifts.

Equations
Instances For
    source
    theorem NaslundCounterexample.growthExponent_pos :
    0 < growthExponent

    The lift exponent is positive.

    source
    theorem NaslundCounterexample.rational_le_growthExponent :
    16 / 21 ≤ growthExponent

    The elementary integer comparison 3^128 ≤ 810^21 bounds the exponent.

    source
    theorem NaslundCounterexample.normalized_log_le_one (n : ℕ) (hn : 1 ≤ n) :
    Real.log ↑(maximumCardinality n) / (↑n * Real.log 3) ≤ 1

    Counting all coefficient vectors bounds the normalized logarithm by one.

    source
    theorem NaslundCounterexample.log_cardinality_lower (n : ℕ) :
    (↑n - 7) * (growthExponent * Real.log 3) ≤ Real.log ↑(maximumCardinality n)

    Rounding the degree down to a multiple of eight costs at most seven degrees.

    source
    theorem NaslundCounterexample.eventually_le_normalized_log (ρ : ℝ) (hρ : ρ < growthExponent) :
    ∀ᶠ (n : ℕ) in Filter.atTop, ρ ≤ Real.log ↑(maximumCardinality n) / (↑n * Real.log 3)

    Every smaller exponent eventually bounds the normalized logarithm from below.

    source
    theorem NaslundCounterexample.liminf_ge :
    16 / 21 ≤ Filter.liminf (fun (n : ℕ) => Real.log ↑(maximumCardinality n) / (↑n * Real.log 3)) Filter.atTop

    The growth rate. The lift exponent, and hence 16/21, bounds the normalized liminf.