The Dias da Silva-Hamidoune theorem

Derives the Dias da Silva-Hamidoune lower bound dias_da_silva_hamidoune on sums of s distinct elements of a subset of ZMod p.

The main theorem of this file was originally proved by Aristotle (Lean v4.24.0, project request uuid 7257b62c-6371-4fa8-a5b5-ea19029f0f1f).

def distinctSumSet {p : ℕ} [Fact (Nat.Prime p)] (A : Finset (ZMod p)) (s : ℕ) : Finset (ZMod p)

The set of all sums of s distinct elements of A

Equations

• distinctSumSet A s = Finset.image (fun (B : Finset (ZMod p)) => ∑ x ∈ B, x) ({B ∈ A.powerset | B.card = s})

theorem dias_da_silva_hamidoune {p : ℕ} [Fact (Nat.Prime p)] (A : Finset (ZMod p)) (s : ℕ) (_h_nonempty : A.Nonempty) (h_s_le_card : s ≤ A.card) : (distinctSumSet A s).card ≥ min p (s * A.card - s ^ 2 + 1)

Theorem 3.3 (Dias da Silva and Hamidoune): Let p be a prime and let A be a nonempty subset of Z_p. Let s∧A denote the set of all sums of s distinct elements of A. Then |s∧A| ≥ min{p, s|A| - s² + 1}.

Proof from the paper: If |A| < s there is nothing to prove. Otherwise put s = k + 1 and apply Theorem 3.2 with A_i = A for all i. Here b′i = |A| - i for all 0 ≤ i ≤ k and hence |(k + 1)∧A| = |⊕{i=0}^k A_i| ≥ min{p, ∑_{i=0}^k (|A| - i) - (k + 2 choose 2) + 1} = min{p, (k + 1)|A| - (k + 1 choose 2) - (k + 2 choose 2) + 1} = min{p, (k + 1)|A| - (k + 1)² + 1}.

Detailed calculation: Let k = s - 1, so s = k + 1. For Theorem 3.2 with all A_i = A, we have b_i = |A| for all i. The compressed sizes are: b′₀ = |A| b′₁ = min{b′₀ - 1, |A|} = |A| - 1 b′₂ = min{b′₁ - 1, |A|} = |A| - 2 ... b′k = min{b′{k-1} - 1, |A|} = |A| - k = |A| - (s - 1)

Then ∑{i=0}^k b′i = ∑{i=0}^k (|A| - i) = (k + 1)|A| - ∑{i=0}^k i = (k + 1)|A| - (k(k + 1))/2 = (k + 1)|A| - (k + 1 choose 2)

Now (k + 2 choose 2) = (k + 1)(k + 2)/2 = (k + 1 choose 2) + (k + 1)

So ∑ b′_i - (k + 2 choose 2) + 1 = [(k + 1)|A| - (k + 1 choose 2)] - [(k + 1 choose 2) + (k + 1)] + 1 = (k + 1)|A| - 2*(k + 1 choose 2) - (k + 1) + 1 = (k + 1)|A| - [2*(k(k + 1))/2] - k = (k + 1)|A| - k(k + 1) - k = (k + 1)|A| - (k + 1)k - k = (k + 1)|A| - (k + 1)² + 1 = s|A| - s² + 1

Thus by Theorem 3.2, we get the desired bound.