theorem
ST_grid_final
{p : ℕ}
[instpprime : Fact (Nat.Prime p)]
(β : ℝ)
(h : 0 < β)
(A : Finset (ZMod p))
(B : Finset (ZMod p))
(n : ℕ+)
(nhₗ : ↑p ^ β ≤ ↑↑n)
(nhᵤ : ↑↑n ≤ ↑p ^ (2 - β))
(hA : ↑A.card ≤ 4 * ↑↑n ^ (1 / 2 + 2 * ST_prime_field_eps β))
(hB : ↑B.card ≤ 4 * ↑↑n ^ (1 / 2 + 2 * ST_prime_field_eps β))
(b₁ : ZMod p)
(hb₁ : b₁ ∉ B)
(b₂ : ZMod p)
(hb₂ : b₂ ∉ B)
(neq : b₁ ≠ b₂)
(allInt : ∀ b ∈ B,
↑↑n ^ (1 - SG_eps₃ β) < Finset.sum (A ×ˢ A) fun (v : ZMod p × ZMod p) =>
if (b₂ - b) / (b₂ - b₁) * v.1 + (b - b₁) / (b₂ - b₁) * v.2 ∈ A then 1 else 0)
:
theorem
ST_grid_aux₂
{p : ℕ}
[instpprime : Fact (Nat.Prime p)]
(β : ℝ)
(h : 0 < β)
(A : Finset (ZMod p))
(B : Finset (ZMod p))
(L : Finset (Line (ZMod p)))
(n : ℕ+)
(nhₗ : ↑p ^ β ≤ ↑↑n)
(nhᵤ : ↑↑n ≤ ↑p ^ (2 - β))
(hA : ↑A.card ≤ 4 * ↑↑n ^ (1 / 2 + 2 * ST_prime_field_eps β))
(hB : ↑B.card ≤ 4 * ↑↑n ^ (1 / 2 + 2 * ST_prime_field_eps β))
(h₂ : L.card ≤ ↑n)
(hC : ∀ l ∈ L, ↑↑n ^ (1 / 2 - SG_eps β) < ↑(IntersectionsP (A ×ˢ B) l).card)
(hHoriz : ∀ l ∈ L, ¬Line.horiz l)
:
theorem
ST_grid_aux
{p : ℕ}
[instpprime : Fact (Nat.Prime p)]
(β : ℝ)
(h : 0 < β)
(A : Finset (ZMod p))
(B : Finset (ZMod p))
(L : Finset (Line (ZMod p)))
(n : ℕ+)
(nhₗ : ↑p ^ β ≤ ↑↑n)
(nhᵤ : ↑↑n ≤ ↑p ^ (2 - β))
(hA : ↑A.card ≤ 4 * ↑↑n ^ (1 / 2 + 2 * ST_prime_field_eps β))
(hB : ↑B.card ≤ 4 * ↑↑n ^ (1 / 2 + 2 * ST_prime_field_eps β))
(h₂ : L.card ≤ ↑n)
(hC : ∀ l ∈ L, ↑↑n ^ (1 / 2 - SG_eps β) < ↑(IntersectionsP (A ×ˢ B) l).card)
:
theorem
ST_grid
{p : ℕ}
[instpprime : Fact (Nat.Prime p)]
(β : ℝ)
(h : 0 < β)
(A : Finset (ZMod p))
(B : Finset (ZMod p))
(L : Finset (Line (ZMod p)))
(n : ℕ+)
(nhₗ : ↑p ^ β ≤ ↑↑n)
(nhᵤ : ↑↑n ≤ ↑p ^ (2 - β))
(hA : ↑A.card ≤ 4 * ↑↑n ^ (1 / 2 + 2 * ST_prime_field_eps β))
(hB : ↑B.card ≤ 4 * ↑↑n ^ (1 / 2 + 2 * ST_prime_field_eps β))
(h₂ : L.card ≤ ↑n)
: