theorem
ST_prime_field_proj
(p : ℕ)
[Fact (Nat.Prime p)]
(β : ℝ)
(h : 0 < β)
(P : Finset (ZMod p × ZMod p))
(L : Finset (Line (ZMod p)))
(n : ℕ+)
(nhₗ : ↑p ^ β ≤ ↑↑n)
(nhᵤ : ↑↑n ≤ ↑p ^ (2 - β))
(h₂ : L.card ≤ ↑n)
(p₁ : ZMod p × ZMod p)
(p₂ : ZMod p × ZMod p)
(neq : p₁ ≠ p₂)
(nml₁ : ↑(IntersectionsL p₁ L).card ≤ 4 * ↑↑n ^ (1 / 2 + 2 * ST_prime_field_eps β))
(nml₂ : ↑(IntersectionsL p₂ L).card ≤ 4 * ↑↑n ^ (1 / 2 + 2 * ST_prime_field_eps β))
(all_int : ∀ p_1 ∈ P, (∃ l ∈ L, p_1 ∈ l ∧ p₁ ∈ l) ∧ ∃ l ∈ L, p_1 ∈ l ∧ p₂ ∈ l)
(nl : ∀ p_1 ∈ P, p_1 ∉ Line.of p₁ p₂ neq)
:
theorem
ST_prime_field_aux
(p : ℕ)
[Fact (Nat.Prime p)]
(β : ℝ)
(h : 0 < β)
(P : Finset (ZMod p × ZMod p))
(L : Finset (Line (ZMod p)))
(n : ℕ+)
(nhₗ : ↑p ^ β ≤ ↑↑n)
(nhᵤ : ↑↑n ≤ ↑p ^ (2 - β))
(h₁ : P.card ≤ ↑n)
(h₂ : L.card ≤ ↑n)
(hc : ∀ l ∈ P, ↑↑n ^ (1 / 2 - ST_prime_field_eps β) ≤ ↑(IntersectionsL l L).card)
(hd : ∀ l ∈ P, ↑(IntersectionsL l L).card ≤ 4 * ↑↑n ^ (1 / 2 + 2 * ST_prime_field_eps β))
:
↑(Intersections P L).card ≤ ↑ST_C₃ * ↑↑n ^ (3 / 2 - ST_prime_field_eps₂ β)
theorem
ST_prime_field_aux₂'
(p : ℕ)
[Fact (Nat.Prime p)]
(β : ℝ)
(h : 0 < β)
(P : Finset (ZMod p × ZMod p))
(L : Finset (Line (ZMod p)))
(n : ℕ+)
(nhₗ : ↑p ^ β ≤ ↑↑n)
(nhᵤ : ↑↑n ≤ ↑p ^ (2 - β))
(h₁ : P.card ≤ ↑n)
(h₂ : L.card ≤ ↑n)
(hc : ∀ l ∈ P, ↑↑n ^ (1 / 2 - ST_prime_field_eps β) ≤ ↑(IntersectionsL l L).card)
:
↑(Intersections P L).card ≤ ↑ST_C₂ * ↑↑n ^ (3 / 2 - ST_prime_field_eps β)
theorem
ST_prime_field
(p : ℕ)
[Fact (Nat.Prime p)]
(β : ℝ)
(h : 0 < β)
(P : Finset (ZMod p × ZMod p))
(L : Finset (Line (ZMod p)))
(n : ℕ+)
(nhₗ : ↑p ^ β ≤ ↑↑n)
(nhᵤ : ↑↑n ≤ ↑p ^ (2 - β))
(h₁ : P.card ≤ ↑n)
(h₂ : L.card ≤ ↑n)
:
↑(Intersections P L).card ≤ ↑ST_C * ↑↑n ^ (3 / 2 - ST_prime_field_eps β)