Documentation

LeanPool.PolynomialMethodRestrictedSums.ANRPolynomialMethod

The Alon-Nathanson-Ruzsa polynomial method #

The core of the polynomial method for restricted sums in ZMod p: elimination polynomials, the vanishing-coefficient lemma on product grids, and the main theorem ANR_polynomial_method giving a non-vanishing-coefficient criterion for lower-bounding restricted sumsets.

theorem eq_zero_of_eval_zero_at_prod_finset {R : Type u_1} [CommRing R] {σ : Type u_2} [Finite σ] [IsDomain R] (P : MvPolynomial σ R) (S : σFinset R) (Hdeg : ∀ (i : σ), MvPolynomial.degreeOf i P < (S i).card) (Heval : ∀ (x : σR), (∀ (i : σ), x i S i)(MvPolynomial.eval x) P = 0) :
P = 0

Lemma 2.2 : A multivariate polynomial that vanishes on a large product finset is the zero polynomial

noncomputable def eliminationPolynomials {p : } [Fact (Nat.Prime p)] {k : } (A : Fin (k + 1)Finset (ZMod p)) :
Fin (k + 1)MvPolynomial (Fin (k + 1)) (ZMod p)

Definition of elimination polynomials g_i

Equations
Instances For
    noncomputable def sumXPolynomial {p : } [Fact (Nat.Prime p)] {k : } :
    MvPolynomial (Fin (k + 1)) (ZMod p)

    The sum of variables polynomial

    Equations
    Instances For
      noncomputable def restrictedSumset {p : } [Fact (Nat.Prime p)] {k : } (h : MvPolynomial (Fin (k + 1)) (ZMod p)) (A : Fin (k + 1)Finset (ZMod p)) :

      The restricted sumset S from the ANR theorem

      Equations
      Instances For
        noncomputable def constructionPolynomial {p : } [Fact (Nat.Prime p)] {k : } (h : MvPolynomial (Fin (k + 1)) (ZMod p)) (E : Multiset (ZMod p)) :
        MvPolynomial (Fin (k + 1)) (ZMod p)

        The polynomial Q = h * ∏_{e∈E} (∑X_i - e)

        Equations
        Instances For
          def extendToSize {p : } [Fact (Nat.Prime p)] (S : Finset (ZMod p)) (m : ) :

          The construction of E from S when |S| ≤ m

          Equations
          Instances For
            noncomputable def productPolynomial {p : } [Fact (Nat.Prime p)] (k : ) (E : Multiset (ZMod p)) :
            MvPolynomial (Fin (k + 1)) (ZMod p)

            Alternative name for clarity. Here use k explicitly

            Equations
            Instances For
              theorem constructionPolynomial_vanishes {p : } [Fact (Nat.Prime p)] {k : } (h : MvPolynomial (Fin (k + 1)) (ZMod p)) (A : Fin (k + 1)Finset (ZMod p)) (E : Multiset (ZMod p)) (hE_sub : (restrictedSumset h A).val E) (x : Fin (k + 1)ZMod p) :
              (∀ (i : Fin (k + 1)), x i A i)(MvPolynomial.eval x) (h * (Multiset.map (fun (e : ZMod p) => sumXPolynomial - MvPolynomial.C e) E).prod) = 0

              Lemma 2.1.1 : Construction_polynomial vanishes on ∏ A_i

              theorem productPolynomial_ne_zero {p : } [Fact (Nat.Prime p)] (k : ) (E : Multiset (ZMod p)) :

              Lemma 2.1.2 : The product polynomial ∏_{e∈E} (∑X_i - C e) is always nonzero

              Lemma 2.1.3.1 : About total degree of sumX

              theorem totalDegree_sumX_sub_C_second {p : } [Fact (Nat.Prime p)] {k : } (e : ZMod p) :

              Lemma 2.1.3.2 : Another version of the previous lemma

              theorem totalDegree_prod_sumX_sub_C_eq_card {p : } [Fact (Nat.Prime p)] {k : } (E : Multiset (ZMod p)) :
              (Multiset.map (fun (e : ZMod p) => i : Fin (k + 1), MvPolynomial.X i - MvPolynomial.C e) E).prod.totalDegree = E.card

              Lemma 2.1.3.3 : The total degree of the product polynomial ∏_{e∈E} (∑X_i - C e) is equal to |E| (Induction steps from J.J. Zhang).

              theorem constructionPolynomial_totalDegree {p : } [Fact (Nat.Prime p)] {k : } (h : MvPolynomial (Fin (k + 1)) (ZMod p)) (h_ne_zero : h 0) (c : Fin (k + 1)) (m : ) (E : Multiset (ZMod p)) (hm : m + h.totalDegree = i : Fin (k + 1), c i) (hE_card : E.card = m) (h_prod_ne_zero : productPolynomial k E 0) :
              (constructionPolynomial h E).totalDegree = i : Fin (k + 1), c i

              Lemma 2.1.4 : The total degree of the construction polynomial is equal to the sum of c_i

              theorem coeff_prod_sumX_minus_C_eq_coeff_sumX_pow_of_degree_eq {p : } [Fact (Nat.Prime p)] {k : } (E : Multiset (ZMod p)) (x : Fin (k + 1) →₀ ) (hx : i : Fin (k + 1), x i = E.card) :
              MvPolynomial.coeff x (Multiset.map (fun (e : ZMod p) => i : Fin (k + 1), MvPolynomial.X i - MvPolynomial.C e) E).prod = MvPolynomial.coeff x ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ E.card)

              Lemma 2.1.5 : The coefficient of a term of maximal degree in the product $\prod (S - e)$ is the same as in $S^{|E|}$

              theorem constructionPolynomial_coeff_target_generalized {p : } [Fact (Nat.Prime p)] {k : } (h : MvPolynomial (Fin (k + 1)) (ZMod p)) (c : Fin (k + 1)) (m : ) (hm : m + h.totalDegree = i : Fin (k + 1), c i) (h_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ m * h) 0) (E : Multiset (ZMod p)) (hE_card : E.card = m) (coeff_prod_sumX_minus_C_target : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) (Multiset.map (fun (e : ZMod p) => i : Fin (k + 1), MvPolynomial.X i - MvPolynomial.C e) E).prod = MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ m)) (other_terms_vanish : ∀ (d : Fin (k + 1) →₀ ), d 0MvPolynomial.coeff d h * MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c - d) (Multiset.map (fun (e : ZMod p) => i : Fin (k + 1), MvPolynomial.X i - MvPolynomial.C e) E).prod = 0) (h_constant_term_nonzero : MvPolynomial.coeff 0 h 0) :

              Lemma 2.1.6 : The coefficient of a specific term in the construction polynomial is non-zero under certain conditions

              theorem elimination_polynomial_properties {p : } [Fact (Nat.Prime p)] {k : } (A : Fin (k + 1)Finset (ZMod p)) (i : Fin (k + 1)) (h_card : (A i).card > 0) :
              have g := eliminationPolynomials A i; MvPolynomial.degreeOf i g = (A i).card MvPolynomial.coeff (fun₀ | i => (A i).card) g = 1 (∀ (x : Fin (k + 1)ZMod p), x i A i(MvPolynomial.eval x) g = 0) (g - MvPolynomial.X i ^ (A i).card).totalDegree < (A i).card

              Lemma 2.1.7 : The elimination polynomial $g_i$ for a given index $i$ and set $A_i$

              theorem monomial_reduction_step {p : } [Fact (Nat.Prime p)] {k : } (m : Fin (k + 1) →₀ ) (i : Fin (k + 1)) (A : Fin (k + 1)Finset (ZMod p)) (c : Fin (k + 1)) (hA : ∀ (j : Fin (k + 1)), (A j).card = c j + 1) (hi : m i > c i) :
              ∃ (Q : MvPolynomial (Fin (k + 1)) (ZMod p)), (Q.totalDegree < m.sum fun (x : Fin (k + 1)) (n : ) => n) (∀ (x : Fin (k + 1)ZMod p), (∀ (j : Fin (k + 1)), x j A j)(MvPolynomial.eval x) Q = (MvPolynomial.eval x) ((MvPolynomial.monomial m) 1)) ((m.sum fun (x : Fin (k + 1)) (n : ) => n) j : Fin (k + 1), c jMvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) Q = MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) ((MvPolynomial.monomial m) 1))

              Lemma 2.1.8 : A single step in the monomial reduction process, reducing the degree in variable i

              theorem exists_remainder {p : } [Fact (Nat.Prime p)] {k : } (Q : MvPolynomial (Fin (k + 1)) (ZMod p)) (A : Fin (k + 1)Finset (ZMod p)) (c : Fin (k + 1)) (hA : ∀ (i : Fin (k + 1)), (A i).card = c i + 1) (hQ_deg : Q.totalDegree i : Fin (k + 1), c i) :
              ∃ (R : MvPolynomial (Fin (k + 1)) (ZMod p)), (∀ (i : Fin (k + 1)), MvPolynomial.degreeOf i R c i) (∀ (x : Fin (k + 1)ZMod p), (∀ (i : Fin (k + 1)), x i A i)(MvPolynomial.eval x) R = (MvPolynomial.eval x) Q) MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) R = MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) Q

              Lemma 2.1.9 : Existence of a remainder polynomial R with bounded degrees matching Q on specified points

              theorem coeff_target_eq_zero_of_vanishes_on_grid {p : } [Fact (Nat.Prime p)] {k : } (Q : MvPolynomial (Fin (k + 1)) (ZMod p)) (A : Fin (k + 1)Finset (ZMod p)) (c : Fin (k + 1)) (hA : ∀ (i : Fin (k + 1)), (A i).card = c i + 1) (hQ_deg : Q.totalDegree i : Fin (k + 1), c i) (hQ_vanishes : ∀ (x : Fin (k + 1)ZMod p), (∀ (i : Fin (k + 1)), x i A i)(MvPolynomial.eval x) Q = 0) :

              Lemma 2.1.10 : If a polynomial Q vanishes on a grid defined by sets A_i and has total degree at most the sum of the sizes of these sets minus one, then the coefficient of the monomial defined by these sizes is zero

              theorem coeff_mul_eq_of_degree_bound {p : } [Fact (Nat.Prime p)] {k : } (h P Q : MvPolynomial (Fin (k + 1)) (ZMod p)) (c : Fin (k + 1)) (m : ) (h_deg : h.totalDegree + m = i : Fin (k + 1), c i) (h_diff : P = Q (P - Q).totalDegree < m) :

              Lemma 2.1.11 : If two polynomials P and Q are equal or their difference has a total degree less than m, then the coefficients of the monomial defined by c in h * P and h * Q are equal, given that h.totalDegree + m equals the sum of c_i

              Lemma 2.1.12 : The total degree of the difference between the product of linear terms and the corresponding power of the sum polynomial is less than the size of the multiset

              theorem ANR_polynomial_method {p : } [Fact (Nat.Prime p)] {k : } (h : MvPolynomial (Fin (k + 1)) (ZMod p)) (A : Fin (k + 1)Finset (ZMod p)) (c : Fin (k + 1)) (hA : ∀ (i : Fin (k + 1)), (A i).card = c i + 1) (m : ) (hm : m + h.totalDegree = i : Fin (k + 1), c i) (h_coeff : MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm c) ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ m * h) 0) :
              have S := Finset.image (fun (f : Fin (k + 1)ZMod p) => i : Fin (k + 1), f i) ({fFintype.piFinset A | (MvPolynomial.eval f) h 0}); S.card m + 1 m < p

              Alon-Nathanson-Ruzsa Polynomial Method (Theorem 2.1)

              Proof outline (by contradiction):

              1. Assume the conclusion is false, so the restricted sumset S has at most m elements; extend S to a multiset E of Z_p with |E| = m (extendToSize).
              2. Construct the polynomial Q(x_0,...,x_k) = h(x_0,...,x_k) * prod_{e in E} (x_0+...+x_k - e) (constructionPolynomial):
              3. By Lemma 2.1.10 (coeff_target_eq_zero_of_vanishes_on_grid), a polynomial of total degree at most sum c_i that vanishes on prod A_i has zero coefficient at prod x_i^{c_i}: reducing Q modulo the elimination polynomials g_i = prod_{a in A_i} (x_i - a) leaves the target coefficient unchanged (exists_remainder), and the reduced polynomial vanishes identically by Lemma 2.2 (eq_zero_of_eval_zero_at_prod_finset).
              4. Steps 2 and 3 contradict each other, so |S| >= m + 1; m < p follows since S is a subset of Z_p.