noncomputable def SzemerediTrotterProjection.orthProj (θ : ℝ) (p : ℝ × ℝ) : ℝ

The orthogonal projection $\pi_\theta(p) = p_1 \cos\theta + p_2 \sin\theta$ of a point $p \in \mathbb{R}^2$ in direction $\theta$, written in product form.

noncomputable def SzemerediTrotterProjection.projImage (θ : ℝ) (X : Finset (ℝ × ℝ)) : Finset ℝ

The image $\pi_\theta(X) \subset \mathbb{R}$ of a finite set $X \subset \mathbb{R}^2$ under the direction-$\theta$ projection.

noncomputable def SzemerediTrotterProjection.smallProjDirections (X : Finset (ℝ × ℝ)) (S : ℕ) : Set ℝ

The set $D = D(X, S) \subset [0, \pi)$ of directions $\theta$ along which the projection $\pi_\theta(X)$ has small image, $|\pi_\theta(X)| \le S$.

theorem SzemerediTrotterProjection.st_fiber_incidence_bound (X : Finset (ℝ × ℝ)) (S n : ℕ) (hn : n = (smallProjDirections X S).ncard) (hfin : (smallProjDirections X S).Finite) (hSlt : S < X.card) (hn2 : n ≥ 2) : ↑n * ↑X.card ≤ ↑X.card + ↑n * ↑S + ↑X.card ^ (2 / 3) * (↑n * ↑S) ^ (2 / 3)

Apply the Szemerédi--Trotter incidence theorem to the fiber-lines configuration: for $X \subset \mathbb{R}^2$ and $n$ small-projection directions, the count $n |X|$ is bounded by $|X| + nS + |X|^{2/3} (nS)^{2/3}$.

theorem SzemerediTrotterProjection.st_algebraic_bound (n P S : ℕ) (hP : ↑P > 0) (hSP : S < P) (hn2 : n ≥ 2) (hST : ↑n * ↑P ≤ ↑P + ↑n * ↑S + ↑P ^ (2 / 3) * (↑n * ↑S) ^ (2 / 3)) : ↑n ≤ ↑S ^ 2 / ↑P + 1

Algebraic lemma extracting the projection bound $n \le S^2/P + 1$ from the Szemerédi--Trotter incidence inequality $nP \le P + nS + P^{2/3}(nS)^{2/3}$.

theorem SzemerediTrotterProjection.szemeredi_trotter_projection_finite (X : Finset (ℝ × ℝ)) (S : ℕ) (hfin : (smallProjDirections X S).Finite) (hSlt : S < X.card) : ↑(smallProjDirections X S).ncard ≤ ↑S ^ 2 / ↑X.card + 1

Szemerédi--Trotter projection theorem (finite case). Under the assumption that the set of small-projection directions is finite and $S < |X|$, we have $|D(X, S)| \le S^2/|X| + 1$.

theorem SzemerediTrotterProjection.szemeredi_trotter_projection (X : Finset (ℝ × ℝ)) (S : ℕ) : ↑(smallProjDirections X S).ncard ≤ ↑S ^ 2 / ↑X.card + 1

Szemerédi--Trotter projection theorem. Let $X$ be a finite set of points in $\mathbb{R}^2$ and $D = D(X, S)$ the set of directions $\theta \in [0, \pi)$ with $|\pi_\theta(X)| \le S$. Then $|D| \le S^2/|X| + 1$ (with the convention that the bound is vacuously satisfied when $D$ is infinite, since then $S \ge |X|$).

theorem SzemerediTrotter.szemeredi_trotter_lines_lower_bound : ∃ C > 0, ∀ (E : Finset (Fin 2 → ℝ)) (S : ℕ), 1 < S → ∀ (L_x : ↥E → Finset Line2), (∀ (x : ↥E), (L_x x).card = S) → (∀ (x : ↥E), ∀ ℓ ∈ L_x x, ↑x ∈ ℓ) → ↑(Finset.univ.biUnion L_x).card ≥ C * min (↑E.card * ↑S) (↑E.card ^ (1 / 2) * ↑S ^ (3 / 2))

Beck's theorem / Szemerédi--Trotter lower bound on lines. There exists a constant $C > 0$ such that for any finite point set $E \subset \mathbb{R}^2$ and any choice of $S$ lines through each point $x \in E$, the union $L = \bigcup_{x \in E} L_x$ has size $|L| \gtrsim \min(|E| \cdot S, |E|^{1/2} S^{3/2})$.