theorem BourgainKatzTaoRobust.bkt2_robust_projection_bound (s_X s_D : ℝ) (hs_X : 0 < s_X) (hs_X' : s_X < 2) (hs_D : 0 < s_D) : ∃ ε > 0, ∀ (p : ℕ) [Fact (Nat.Prime p)] (X : Finset (ZMod p × ZMod p)) (D : Finset (ZMod p)), X.card = ⌊↑p ^ s_X⌋₊ → D.card = ⌊↑p ^ s_D⌋₊ → ∃ t ∈ D, ∀ Y ⊆ X, ↑Y.card ≥ ↑p ^ (-ε) * ↑X.card → ↑(Finset.image (fun (x : ZMod p × ZMod p) => x.1 + t * x.2) Y).card ≥ ↑p ^ ε * ↑X.card ^ (1 / 2)

Bourgain–Katz–Tao 2 (robust version). With the same setup as BKT (X ⊂ 𝔽_p² of size p^{s_X}, D ⊂ 𝔽_p of size p^{s_D} with 0 < s_X < 2, 0 < s_D), there exists ε = ε(s_X, s_D) > 0 and a direction t ∈ D such that the projection π_t : (x₁, x₂) ↦ x₁ + t·x₂ is robust: for every Y ⊆ X with |Y| ≥ p^{-ε} |X|, |π_t(Y)| ≥ p^ε |X|^{1/2}.