theorem ProjectionTheory.sum_product_contagious_lower_bound (s_A s_D : ℝ) (hs_A_pos : 0 < s_A) (hs_A_lt : s_A < 1) (hs_D_pos : 0 < s_D) : ∃ (r : ℝ) (c : ℝ), 0 < r ∧ 0 < c ∧ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (A D : Finset (ZMod p)), A.Nonempty → D.Nonempty → ↑A.card = ↑p ^ s_A → ↑D.card = ↑p ^ s_D → ∀ K ≥ 1, (∀ t ∈ D, ↑(A + t • A).card ≤ K * ↑A.card) → K ^ c ≥ ↑p ^ r

Contagious-structure lower bound underlying the dilated sumset expansion. For exponents 0 < s_A < 1 and 0 < s_D, there exist r, c > 0 such that for any prime p, any A, D ⊆ 𝔽_p with |A| = p^{s_A} and |D| = p^{s_D}, and any K ≥ 1 with |A + t·A| ≤ K|A| for all t ∈ D, one has K^c ≥ p^r. That is, small dilated sumsets across a sufficiently large set of directions force K itself to grow like a power of p.

theorem ProjectionTheory.exists_eps_dilated_sumset_expansion (s_A s_D : ℝ) (hs_A_pos : 0 < s_A) (hs_A_lt : s_A < 1) (hs_D_pos : 0 < s_D) : ∃ ε₁ > 0, ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (A D : Finset (ZMod p)), A.Nonempty → D.Nonempty → ↑A.card = ↑p ^ s_A → ↑D.card = ↑p ^ s_D → ∃ t ∈ D, ↑(A + t • A).card ≥ ↑p ^ ε₁ * ↑A.card

Dilated sumset expansion (Bourgain–Katz–Tao, finite field version). For exponents 0 < s_A < 1 and 0 < s_D, there exists ε₁ > 0 such that for any prime p, any A, D ⊆ 𝔽_p with |A| = p^{s_A} and |D| = p^{s_D}, there is some direction t ∈ D for which |A + t·A| ≥ p^{ε₁} |A|. In other words, one cannot have all dilated sumsets A + t·A simultaneously close in size to A.

noncomputable def ProjectionTheory.sumProductSet {p : ℕ} [Fact (Nat.Prime p)] (A : Finset (ZMod p)) : Finset (ZMod p)

The sum-product set A + A·A = {a + b·c : a, b, c ∈ A} of a finite subset A ⊆ 𝔽_p.

theorem ProjectionTheory.dilated_sumset_subset_sumProductSet {p : ℕ} [Fact (Nat.Prime p)] (A : Finset (ZMod p)) (t : ZMod p) (ht : t ∈ A) : A + t • A ⊆ sumProductSet A

For any t ∈ A, the dilated sumset A + t·A is contained in the sum-product set A + A·A.

theorem ProjectionTheory.sum_product_expansion (s_A : ℝ) (hs_A_pos : 0 < s_A) (hs_A_lt : s_A < 1) : ∃ ε > 0, ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (A : Finset (ZMod p)), A.Nonempty → ↑A.card = ↑p ^ s_A → ∃ t ∈ A, ↑(A + t • A).card ≥ ↑p ^ ε * ↑A.card

Specialization of exists_eps_dilated_sumset_expansion to the case D = A: for |A| = p^{s_A} with 0 < s_A < 1, there exists ε > 0 and some t ∈ A with |A + t·A| ≥ p^ε |A|.

theorem ProjectionTheory.sum_product_set_expansion (s_A : ℝ) (hs_A_pos : 0 < s_A) (hs_A_lt : s_A < 1) : ∃ ε > 0, ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (A : Finset (ZMod p)), A.Nonempty → ↑A.card = ↑p ^ s_A → ↑(sumProductSet A).card ≥ ↑p ^ (s_A + ε)

Sum-product expansion in 𝔽_p: if A ⊆ 𝔽_p with |A| = p^{s_A} for 0 < s_A < 1, then |A + A·A| ≥ p^{s_A + ε} for some ε = ε(s_A) > 0. This is the corollary |A + A·A| ≥ p^{s_A + ε} of the contagious-structure analysis.