Restricted sums of sets with distinct sizes

The Alon-Nathanson-Ruzsa lower bound restricted_sum_distinct_sizes on the set of sums a 0 + ... + a k with a i ∈ A i pairwise distinct, when the sets A i have distinct sizes.

def restrictedSumSet {p : ℕ} [Fact (Nat.Prime p)] (k : ℕ) (A : Fin (k + 1) → Finset (ZMod p)) : Finset (ZMod p)

S = {a + ... + a | a ∈ A, a ≠ a for all i ≠ j}

Equations

• restrictedSumSet k A = Finset.image (fun (f : Fin (k + 1) → ZMod p) => ∑ i : Fin (k + 1), f i) ({f ∈ Fintype.piFinset A | ∀ (i j : Fin (k + 1)), i < j → f i ≠ f j})

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

Vandermonde: ∏_{i>j} (X - X)

Equations

• vandermondePolynomial k = ∏ i : Fin (k + 1), ∏ j : Fin (k + 1), if ↑j < ↑i then MvPolynomial.X i - MvPolynomial.X j else 1

@[irreducible]

def compressedSizes {k : ℕ} (b : Fin (k + 1) → ℕ) : Fin (k + 1) → ℕ

(Used in CompressedSizesRestrictedSum and DiasDaSilvaHamidoune) The compressed sizes b'_i defined recursively: b'_0 = b_0, b'i = min{b'{i-1} - 1, b_i} for i ≥ 1

Equations

• compressedSizes b ⟨0, ⋯⟩ = b 0
• compressedSizes b ⟨i_2.succ, hi⟩ = min (compressedSizes b ⟨i_2, ⋯⟩ - 1) (b ⟨i_2 + 1, hi⟩)

theorem vandermonde_degree_eq (k p : ℕ) [Fact (Nat.Prime p)] : (vandermondePolynomial k).totalDegree = (k + 1).choose 2

theorem restricted_sum_m_bound {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ} (A : Fin (k + 1) → Finset (ZMod p)) (h_nonempty : ∀ (i : Fin (k + 1)), (A i).Nonempty) (h_sum_bound : ∑ i : Fin (k + 1), (A i).card ≤ p + (k + 2).choose 2 - 1) : have c := fun (i : Fin (k + 1)) => (A i).card - 1; have m := ∑ i : Fin (k + 1), c i - (k + 1).choose 2; m < p

theorem vandermonde_coeff_nonzero {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ} (c : Fin (k + 1) → ℕ) (m : ℕ) (hc : ∀ (i : Fin (k + 1)), c i < p) (h_distinct : ∀ (i j : Fin (k + 1)), i < j → c i ≠ c j) (hm : m < p) (h_sum : ∑ i : Fin (k + 1), c i = m + (k + 1).choose 2) : MvPolynomial.coeff (toFinsupp c) ((∑ i : Fin (k + 1), MvPolynomial.X i) ^ m * vandermondePolynomial k) ≠ 0

theorem restricted_sum_distinct_sizes {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ} (A : Fin (k + 1) → Finset (ZMod p)) (h_nonempty : ∀ (i : Fin (k + 1)), (A i).Nonempty) (h_sizes_distinct : ∀ (i j : Fin (k + 1)), i < j → (A i).card ≠ (A j).card) (h_sum_bound : ∑ i : Fin (k + 1), (A i).card ≤ p + (k + 2).choose 2 - 1) : (restrictedSumSet k A).card ≥ ∑ i : Fin (k + 1), (A i).card - (k + 2).choose 2 + 1