Documentation

LeanPool.ErdosGinzburgZiv.EGZ.Main.UpperBound

The exact finite target for the main theorem #

The final section first proves a zero-sum assertion at a ceiling length. This is enough for MainUpperBound, but the ceiling must be absorbed using a smaller internal error parameter. It cannot simply be dropped.

source
def EGZ.EventualCeilZeroSum (d : ℕ) :
Prop

The finite multiplicity statement to be supplied by the structural argument. The prime threshold is uniform over the input multiset.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem EGZ.mainUpperBound_of_eventualCeilZeroSum (d : ℕ) (h : EventualCeilZeroSum d) :
    MainUpperBound d

    Absorb the ceiling by applying the finite theorem with half the requested error (or less), and then taking sufficiently large primes.

    source
    theorem EGZ.mainAsymptotic_of_eventualCeilZeroSum (d : ℕ) (hd : 0 < d) (h : EventualCeilZeroSum d) :
    MainAsymptotic d

    The completed lower estimate and polynomial bound turn the corrected finite target into the paper's asymptotic statement.