Restricted sums with compressed sizes

Theorem 3.2 of Alon-Nathanson-Ruzsa: a lower bound on the restricted sum set in terms of the "compressed sizes" of the summand sets.

The main theorem of this file was originally proved by Aristotle (Lean v4.24.0, project request uuid 08cb15be-5c46-4619-9dbf-e523d453b544).

def ValidSeq (k : ℕ) (b : Fin (k + 1) → ℕ) : Prop

A sequence b is valid if it is strictly decreasing and the last element is positive.

Equations

• ValidSeq k b = ((∀ (i j : Fin (k + 1)), i < j → b j < b i) ∧ 0 < b (Fin.last k))

def baseSeq (k : ℕ) : Fin (k + 1) → ℕ

The base sequence b_i = k + 1 - i. Its sum equals (k + 2).choose 2.

Equations

• baseSeq k i = k + 1 - ↑i

theorem sum_baseSeq (k : ℕ) : ∑ i : Fin (k + 1), baseSeq k i = (k + 2).choose 2

theorem valid_seq_ge_base {k : ℕ} {b : Fin (k + 1) → ℕ} (h : ValidSeq k b) (i : Fin (k + 1)) : b i ≥ baseSeq k i

theorem exists_gt_base_of_ne_base {k : ℕ} {b : Fin (k + 1) → ℕ} (h_valid : ValidSeq k b) (h_ne : b ≠ baseSeq k) : ∃ (j : Fin (k + 1)), baseSeq k j < b j

noncomputable def transformSeq (k : ℕ) (b : Fin (k + 1) → ℕ) : Fin (k + 1) → ℕ

The transformation T maps a sequence b to b' by finding the largest index j such that b_j > k + 1 - j and setting b'_j = b_j - 1. If no such j exists (i.e. b is the base sequence), it returns b.

Equations

• transformSeq k b = if h : {j : Fin (k + 1) | baseSeq k j < b j}.Nonempty then have j := {j : Fin (k + 1) | baseSeq k j < b j}.max' h; Function.update b j (b j - 1) else b

theorem transformSeq_props {k : ℕ} {b : Fin (k + 1) → ℕ} (h_valid : ValidSeq k b) (h_not_base : b ≠ baseSeq k) : have b' := transformSeq k b; ValidSeq k b' ∧ ∑ i : Fin (k + 1), b' i = ∑ i : Fin (k + 1), b i - 1 ∧ ∀ (i : Fin (k + 1)), b' i ≤ b i

theorem compressedSizes_le {k : ℕ} {b : Fin (k + 1) → ℕ} (i : Fin (k + 1)) : compressedSizes b i ≤ b i

theorem compressedSizes_succ {k : ℕ} {b : Fin (k + 1) → ℕ} (i : Fin k) : compressedSizes b i.succ = min (compressedSizes b i.castSucc - 1) (b i.succ)

theorem compressedSizes_pos {k : ℕ} {b : Fin (k + 1) → ℕ} (h_last_pos : compressedSizes b (Fin.last k) > 0) (i : Fin (k + 1)) : 0 < compressedSizes b i

theorem polynomialMethod_reduction_lemma {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ} {b : Fin (k + 1) → ℕ} (h_valid : ValidSeq k b) (h_sum : ∑ i : Fin (k + 1), b i > p + (k + 2).choose 2 - 1) : ∃ (b'' : Fin (k + 1) → ℕ), ValidSeq k b'' ∧ ∑ i : Fin (k + 1), b'' i = p + (k + 2).choose 2 - 1 ∧ ∀ (i : Fin (k + 1)), b'' i ≤ b i

theorem compressedSizes_is_valid {k : ℕ} {b : Fin (k + 1) → ℕ} (h_last_pos : compressedSizes b (Fin.last k) > 0) : ValidSeq k (compressedSizes b)

theorem compressedSizes_restricted_sum {p : ℕ} [Fact (Nat.Prime p)] {k : ℕ} (A : Fin (k + 1) → Finset (ZMod p)) (_h_nonempty : ∀ (i : Fin (k + 1)), (A i).Nonempty) (_h_sizes_noninc : ∀ (i j : Fin (k + 1)), i ≤ j → (A j).card ≤ (A i).card) (h_last_pos : compressedSizes (fun (i : Fin (k + 1)) => (A i).card) (Fin.last k) > 0) : (restrictedSumSet k A).card ≥ min p (∑ i : Fin (k + 1), compressedSizes (fun (i : Fin (k + 1)) => (A i).card) i - (k + 2).choose 2 + 1)