Documentation

LeanPool.ErdosGinzburgZiv.EGZ.ZeroSum.Constants

Constants #

source
noncomputable def EGZ.egzConstant (p d : β„•) :
β„•

The ErdΕ‘s--Ginzburg--Ziv constant 𝔰(𝔽_p^d): the least exact sequence length with the EGZ property. exists_egzProperty supplies the witness used by Nat.find, so the definition does not depend on the default behavior of an infimum of an empty set.

Equations
Instances For
    source
    theorem EGZ.egzConstant_spec (p d : β„•) :
    EGZProperty p d (egzConstant p d)

    The least EGZ length itself has the EGZ property.

    source
    theorem EGZ.egzConstant_min {p d n : β„•} (h : EGZProperty p d n) :
    egzConstant p d ≀ n

    Minimality of the EGZ constant.

    source
    theorem EGZ.egzConstant_le_pigeonhole_bound (p d : β„•) :
    egzConstant p d ≀ (p - 1) * p ^ d + 1

    The crude pigeonhole construction gives an explicit finite upper bound.

    source
    theorem EGZ.egzProperty_of_egzConstant_le {p d n : β„•} (h : egzConstant p d ≀ n) :
    EGZProperty p d n

    Every exact length at least the EGZ constant has the EGZ property.

    source
    theorem EGZ.lt_egzConstant_of_not_egzProperty {p d n : β„•} (h : Β¬EGZProperty p d n) :
    n < egzConstant p d

    A failed exact length lies strictly below the EGZ constant.

    source
    noncomputable def EGZ.hollowConstant (p d : β„•) :
    β„•

    The extremal p-hollow number 𝔴(𝔽_p^d).

    The paper only uses this at primes. We search through the natural ambient bound p ^ d; for prime p, injectivity of hollow families proves that this cutoff loses nothing. This bounded definition is total even at the degenerate moduli 0 and 1, where hollow lengths need not be bounded.

    Equations
    Instances For
      source
      theorem EGZ.hollowConstant_le_pow (p d : β„•) :
      hollowConstant p d ≀ p ^ d

      The bounded-search definition is always at most the ambient cutoff.

      source
      theorem EGZ.hollowConstant_spec {p d : β„•} (hp : Nat.Prime p) :
      AdmitsPHollowLength p d (hollowConstant p d)

      At a prime, the extremal hollow length is attained.

      source
      theorem EGZ.hollowConstant_max {p d s : β„•} (hp : Nat.Prime p) (h : AdmitsPHollowLength p d s) :
      s ≀ hollowConstant p d

      At a prime, every admitted hollow length is at most the hollow constant.

      source
      theorem EGZ.hollowLength_mul_add_one_le_egzConstant {p d s : β„•} (hp : 0 < p) (h : AdmitsPHollowLength p d s) :
      s * (p - 1) + 1 ≀ egzConstant p d

      Any positive-modulus hollow family gives the elementary EGZ lower bound.

      source
      theorem EGZ.hollowConstant_mul_add_one_le_egzConstant {p d : β„•} (hp : Nat.Prime p) :
      hollowConstant p d * (p - 1) + 1 ≀ egzConstant p d

      The standard lower comparison between the two constants.