Documentation

LeanPool.ErdosGinzburgZiv.EGZ.Polynomial.HollowBound

A polynomial bound for hollow families #

This file formalizes Proposition thw from the paper. For every positive dimension d and prime p, it proves

𝔴(𝔽_p^d) ≀ choose (2 * d - 1) d + 1.

The right-hand side is independent of p, which is the fact needed when the elementary lower bound for the ErdΕ‘s--Ginzburg--Ziv constant is converted into an asymptotic statement.

The proof follows the paper's polynomial method. Stars and bars counts the low-degree monomials. A kernel-dimension argument produces a nonzero weight annihilating them and vanishing at one prescribed point. Contracting the zero-sum detector polynomial in all but its last vector block is constant in that last block, while hollowness identifies it with h(t)^q; these two facts contradict the choice of h.

Low-degree monomials and the annihilator #

source
@[reducible, inline]
abbrev EGZ.Polynomial.LowExponent (d : β„•) :
Type

Stars-and-bars indices for monomials in d variables of total degree at most d - 1. The final coordinate is a slack exponent.

Equations
Instances For
    source
    noncomputable def EGZ.Polynomial.lowExponentTuple (d : β„•) (a : LowExponent d) :
    Fin (d + 1) β†’ β„•

    The exponent tuple, including its final slack coordinate.

    Equations
    Instances For
      source
      noncomputable def EGZ.Polynomial.lowExponentMonomial (d : β„•) (a : LowExponent d) :
      Fin d β†’ β„•

      The actual exponent tuple in the first d coordinates.

      Equations
      Instances For
        source
        theorem EGZ.Polynomial.lowExponentTuple_sum (d : β„•) (a : LowExponent d) :
        βˆ‘ j : Fin (d + 1), lowExponentTuple d a j = d - 1
        source
        noncomputable def EGZ.Polynomial.lowExponentOfFun (d : β„•) (e : Fin d β†’ β„•) (he : βˆ‘ j : Fin d, e j ≀ d - 1) :
        LowExponent d

        Pad an exponent tuple of total degree at most d - 1 with a slack coordinate.

        Equations
        Instances For
          source
          @[simp]
          theorem EGZ.Polynomial.lowExponentMonomial_lowExponentOfFun (d : β„•) (e : Fin d β†’ β„•) (he : βˆ‘ j : Fin d, e j ≀ d - 1) :
          lowExponentMonomial d (lowExponentOfFun d e he) = e
          source
          theorem EGZ.Polynomial.card_lowExponent (d : β„•) (hd : 1 ≀ d) :
          Fintype.card (LowExponent d) = (2 * d - 1).choose d

          The number of monomials in d variables of degree at most d - 1.

          source
          def EGZ.Polynomial.monomialValue {K : Type u_1} [Field K] {d : β„•} (e : Fin d β†’ β„•) (x : Fin d β†’ K) :
          K

          Value of a coordinate monomial.

          Equations
          Instances For
            source
            noncomputable def EGZ.Polynomial.equationMap {K : Type u_1} [Field K] {d n : β„•} (v : Fin n β†’ Fin d β†’ K) (tβ‚€ : Fin n) :
            (Fin n β†’ K) β†’β‚—[K] Option (LowExponent d) β†’ K

            The linear system consisting of every low-monomial moment and one prescribed zero coordinate.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem EGZ.Polynomial.exists_annihilator {K : Type u_1} [Field K] {d n : β„•} (hd : 1 ≀ d) (hn : (2 * d - 1).choose d + 2 ≀ n) (v : Fin n β†’ Fin d β†’ K) (tβ‚€ : Fin n) :
              βˆƒ (h : Fin n β†’ K), h β‰  0 ∧ h tβ‚€ = 0 ∧ βˆ€ (e : LowExponent d), βˆ‘ i : Fin n, h i * monomialValue (lowExponentMonomial d e) (v i) = 0

              More variables than equations give a nonzero annihilating weight.

              source
              def EGZ.Polynomial.AnnihilatesLow {K : Type u_1} [Field K] {d n : β„•} (h : Fin n β†’ K) (v : Fin n β†’ Fin d β†’ K) :
              Prop

              A weight annihilates every ordinary exponent tuple of total degree at most d - 1.

              Equations
              Instances For
                source
                theorem EGZ.Polynomial.exists_annihilator' {K : Type u_1} [Field K] {d n : β„•} (hd : 1 ≀ d) (hn : (2 * d - 1).choose d + 2 ≀ n) (v : Fin n β†’ Fin d β†’ K) (tβ‚€ : Fin n) :
                βˆƒ (h : Fin n β†’ K), h β‰  0 ∧ h tβ‚€ = 0 ∧ AnnihilatesLow h v

                The detector polynomial #

                source
                noncomputable def EGZ.Polynomial.zeroSumDetector (q d : β„•) :
                MvPolynomial (Fin (q + 1) Γ— Fin d) (ZMod (q + 1))

                The polynomial detecting whether q + 1 vector blocks sum to zero over ZMod (q + 1).

                Equations
                Instances For
                  source
                  theorem EGZ.Polynomial.totalDegree_zeroSumDetector_le (q d : β„•) [Fact (Nat.Prime (q + 1))] :
                  (zeroSumDetector q d).totalDegree ≀ d * q

                  Total-degree bound for the detector.

                  source
                  theorem EGZ.Polynomial.eval_zeroSumDetector (q d : β„•) (y : Fin (q + 1) β†’ FpVec (q + 1) d) :
                  (MvPolynomial.eval fun (ij : Fin (q + 1) Γ— Fin d) => y ij.1 ij.2) (zeroSumDetector q d) = ∏ j : Fin d, (1 - (βˆ‘ i : Fin (q + 1), y i j) ^ q)
                  source
                  theorem EGZ.Polynomial.eval_zeroSumDetector_eq_one_iff (q d : β„•) [Fact (Nat.Prime (q + 1))] (y : Fin (q + 1) β†’ FpVec (q + 1) d) :
                  (MvPolynomial.eval fun (ij : Fin (q + 1) Γ— Fin d) => y ij.1 ij.2) (zeroSumDetector q d) = 1 ↔ βˆ‘ i : Fin (q + 1), y i = 0

                  The detector is 1 exactly on tuples whose vector sum is zero.

                  Monomial contraction #

                  source
                  def EGZ.Polynomial.blockDegree {q d : β„•} (e : Fin (q + 1) Γ— Fin d β†’β‚€ β„•) (i : Fin (q + 1)) :
                  β„•

                  Degree contributed by one vector block.

                  Equations
                  Instances For
                    source
                    def EGZ.Polynomial.blockValue {K : Type u_1} [Field K] {q d : β„•} (e : Fin (q + 1) Γ— Fin d β†’β‚€ β„•) (i : Fin (q + 1)) (x : Fin d β†’ K) :
                    K

                    Value of the part of a monomial belonging to one vector block.

                    Equations
                    Instances For
                      source
                      theorem EGZ.Polynomial.sum_blockDegree {q d : β„•} (e : Fin (q + 1) Γ— Fin d β†’β‚€ β„•) :
                      βˆ‘ i : Fin (q + 1), blockDegree e i = e.sum fun (x : Fin (q + 1) Γ— Fin d) (n : β„•) => n
                      source
                      theorem EGZ.Polynomial.fullMonomialValue_eq_blocks {K : Type u_1} [Field K] {q d : β„•} (e : Fin (q + 1) Γ— Fin d β†’β‚€ β„•) (y : Fin (q + 1) β†’ Fin d β†’ K) :
                      ∏ ij : Fin (q + 1) Γ— Fin d, y ij.1 ij.2 ^ e ij = ∏ i : Fin (q + 1), blockValue e i (y i)
                      source
                      theorem EGZ.Polynomial.low_block_or_last_zero {q d : β„•} [Fact (Nat.Prime (q + 1))] {e : Fin (q + 1) Γ— Fin d β†’β‚€ β„•} (he : e ∈ (zeroSumDetector q d).support) :
                      (βˆƒ (k : Fin q), blockDegree e k.castSucc ≀ d - 1) ∨ blockDegree e (Fin.last q) = 0

                      Every supported detector monomial either has low degree in one of the first q blocks, or degree zero in the last block.

                      source
                      theorem EGZ.Polynomial.blockValue_last_eq_one_of_degree_zero {K : Type u_1} [Field K] {q d : β„•} (e : Fin (q + 1) Γ— Fin d β†’β‚€ β„•) (x : Fin d β†’ K) (he : blockDegree e (Fin.last q) = 0) :
                      blockValue e (Fin.last q) x = 1
                      source
                      def EGZ.Polynomial.weightedMonomialSum {K : Type u_1} [Field K] {q d n : β„•} (h : Fin n β†’ K) (v : Fin n β†’ Fin d β†’ K) (e : Fin (q + 1) Γ— Fin d β†’β‚€ β„•) (t : Fin n) :
                      K

                      Contribution of one detector monomial after contracting its first q blocks.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem EGZ.Polynomial.sum_weighted_blockValues_eq_prod_sums {K : Type u_1} [Field K] {q d n : β„•} (h : Fin n β†’ K) (v : Fin n β†’ Fin d β†’ K) (e : Fin (q + 1) Γ— Fin d β†’β‚€ β„•) :
                        βˆ‘ a : Fin q β†’ Fin n, (∏ k : Fin q, h (a k)) * ∏ k : Fin q, blockValue e k.castSucc (v (a k)) = ∏ k : Fin q, βˆ‘ i : Fin n, h i * blockValue e k.castSucc (v i)
                        source
                        theorem EGZ.Polynomial.weightedMonomialSum_eq_of_support {q d n : β„•} [Fact (Nat.Prime (q + 1))] {h : Fin n β†’ ZMod (q + 1)} {v : Fin n β†’ FpVec (q + 1) d} (ha : AnnihilatesLow h v) {e : Fin (q + 1) Γ— Fin d β†’β‚€ β„•} (he : e ∈ (zeroSumDetector q d).support) (t u : Fin n) :
                        weightedMonomialSum h v e t = weightedMonomialSum h v e u

                        The contracted detector #

                        source
                        def EGZ.Polynomial.tupleWithLast {q d n : β„•} (v : Fin n β†’ FpVec (q + 1) d) (a : Fin q β†’ Fin n) (t : Fin n) :
                        Fin (q + 1) β†’ FpVec (q + 1) d

                        Append the final vector block to the q contracted blocks.

                        Equations
                        Instances For
                          source
                          def EGZ.Polynomial.indexTuple {q n : β„•} (a : Fin q β†’ Fin n) (t : Fin n) :
                          Fin (q + 1) β†’ Fin n

                          The corresponding tuple of indices.

                          Equations
                          Instances For
                            source
                            noncomputable def EGZ.Polynomial.phi {q d n : β„•} (h : Fin n β†’ ZMod (q + 1)) (v : Fin n β†’ FpVec (q + 1) d) (t : Fin n) :
                            ZMod (q + 1)

                            Contract the detector against h in its first q blocks.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              theorem EGZ.Polynomial.phi_eq_support_sum {q d n : β„•} [Fact (Nat.Prime (q + 1))] (h : Fin n β†’ ZMod (q + 1)) (v : Fin n β†’ FpVec (q + 1) d) (t : Fin n) :
                              phi h v t = βˆ‘ e ∈ (zeroSumDetector q d).support, (zeroSumDetector q d).coeff e * weightedMonomialSum h v e t
                              source
                              theorem EGZ.Polynomial.phi_eq_of_annihilatesLow {q d n : β„•} [Fact (Nat.Prime (q + 1))] {h : Fin n β†’ ZMod (q + 1)} {v : Fin n β†’ FpVec (q + 1) d} (ha : AnnihilatesLow h v) (t u : Fin n) :
                              phi h v t = phi h v u

                              The low-moment conditions make phi independent of its final argument.

                              source
                              theorem EGZ.Polynomial.isPHollow_sum_zero_iff_constant {q d n : β„•} {v : Fin n β†’ FpVec (q + 1) d} (hv : IsPHollow (q + 1) v) (a : Fin (q + 1) β†’ Fin n) :
                              βˆ‘ k : Fin (q + 1), v (a k) = 0 ↔ βˆƒ (i : Fin n), βˆ€ (k : Fin (q + 1)), a k = i

                              Operational hollowness specialized to a Fin (q + 1) tuple.

                              source
                              theorem EGZ.Polynomial.isPHollow_detector_on_tuple {q d n : β„•} [Fact (Nat.Prime (q + 1))] {v : Fin n β†’ FpVec (q + 1) d} (hv : IsPHollow (q + 1) v) (a : Fin (q + 1) β†’ Fin n) :
                              (MvPolynomial.eval fun (ij : Fin (q + 1) Γ— Fin d) => v (a ij.1) ij.2) (zeroSumDetector q d) = if βˆƒ (i : Fin n), βˆ€ (k : Fin (q + 1)), a k = i then 1 else 0

                              On a hollow family, the detector is supported exactly on constant index tuples.

                              source
                              theorem EGZ.Polynomial.isPHollow_detector_tupleWithLast {q d n : β„•} [Fact (Nat.Prime (q + 1))] {v : Fin n β†’ FpVec (q + 1) d} (hv : IsPHollow (q + 1) v) (a : Fin q β†’ Fin n) (t : Fin n) :
                              (MvPolynomial.eval fun (ij : Fin (q + 1) Γ— Fin d) => tupleWithLast v a t ij.1 ij.2) (zeroSumDetector q d) = if a = fun (x : Fin q) => t then 1 else 0
                              source
                              theorem EGZ.Polynomial.phi_eq_pow_of_isPHollow {q d n : β„•} [Fact (Nat.Prime (q + 1))] {v : Fin n β†’ FpVec (q + 1) d} (hv : IsPHollow (q + 1) v) (h : Fin n β†’ ZMod (q + 1)) (t : Fin n) :
                              phi h v t = h t ^ q

                              Hollowness gives the first computation of the contraction: phi(t) = h(t)^q.

                              source
                              theorem EGZ.Polynomial.phollow_length_le_succ_choose {q d n : β„•} [Fact (Nat.Prime (q + 1))] (hd : 1 ≀ d) {v : Fin n β†’ FpVec (q + 1) d} (hv : IsPHollow (q + 1) v) :
                              n ≀ (2 * d - 1).choose d + 1

                              Pointwise polynomial bound for a modulus written as the prime q + 1.

                              Proposition thw and the bound on 𝔴 #

                              source
                              theorem EGZ.IsPHollow.card_le_choose_add_one {p d s : β„•} (hp : Nat.Prime p) (hd : 1 ≀ d) {v : Fin s β†’ FpVec p d} (hv : IsPHollow p v) :
                              s ≀ (2 * d - 1).choose d + 1

                              Proposition thw. Every p-hollow family in positive dimension has at most choose (2d - 1) d + 1 members.

                              source
                              theorem EGZ.hollowConstant_le_choose_add_one {p d : β„•} (hp : Nat.Prime p) (hd : 1 ≀ d) :
                              hollowConstant p d ≀ (2 * d - 1).choose d + 1

                              The polynomial upper bound on the extremal hollow number.

                              source
                              theorem EGZ.exists_uniform_hollowConstant_bound (d : β„•) (hd : 1 ≀ d) :
                              βˆƒ (C : β„•), βˆ€ (p : β„•), Nat.Prime p β†’ hollowConstant p d ≀ C

                              For fixed positive d, 𝔴(𝔽_p^d) is bounded independently of the prime. This is the form used by the asymptotic bridge.