structure SzemerediTrotter.Line2 : Type

A line in $\mathbb{R}^2$: a $1$-dimensional non-empty affine subspace of $\mathbb{R}^2$.

• carrier : AffineSubspace ℝ (Fin 2 → ℝ)
• dim_eq : Module.finrank ℝ ↥self.carrier.direction = 1
• nonempty : (↑self.carrier).Nonempty

@[implicit_reducible]

instance SzemerediTrotter.instMembershipForallFinOfNatNatRealLine2 : Membership (Fin 2 → ℝ) Line2

Membership of a point in a Line2: $p \in \ell$ iff $p$ belongs to the underlying affine subspace.

noncomputable def SzemerediTrotter.incidenceCount (X : Finset (Fin 2 → ℝ)) (L : Finset Line2) : ℕ

The incidence count $I(X, L) = \#\{(x, \ell) \in X \times L : x \in \ell\}$ between a finite set of points $X \subset \mathbb{R}^2$ and a finite set of lines $L$.

theorem SzemerediTrotter.two_points_unique_line (p q : Fin 2 → ℝ) (hpq : p ≠ q) (ℓ₁ ℓ₂ : Line2) (hp1 : p ∈ ℓ₁) (hq1 : q ∈ ℓ₁) (hp2 : p ∈ ℓ₂) (hq2 : q ∈ ℓ₂) : ℓ₁.carrier = ℓ₂.carrier

Two distinct points determine a unique line: if $p \ne q$ and both lie on two lines $\ell_1, \ell_2$, then $\ell_1$ and $\ell_2$ have the same underlying affine subspace.

theorem SzemerediTrotter.Line2.ext' (ℓ₁ ℓ₂ : Line2) (h : ℓ₁.carrier = ℓ₂.carrier) : ℓ₁ = ℓ₂

Extensionality for Line2: two lines are equal iff their carrier affine subspaces are equal.

theorem SzemerediTrotter.weak_bound_incidence (X : Finset (Fin 2 → ℝ)) (L : Finset Line2) : ↑(incidenceCount X L) ≤ ↑X.card * ↑L.card ^ (1 / 2) + ↑L.card

Weak incidence bound. For any finite set of points $X$ and lines $L$ in $\mathbb{R}^2$, the incidence count satisfies $I(X, L) \le |X| |L|^{1/2} + |L|$, obtained by Cauchy--Schwarz together with the uniqueness of the line through two points.

theorem SzemerediTrotter.cell_parametric_bound_sharp (X : Finset (Fin 2 → ℝ)) (L : Finset Line2) (s : ℝ) (hs : s ≥ 1) : ↑(incidenceCount X L) ≤ ↑X.card ^ (2 / 3) * ↑L.card ^ (2 / 3) + ↑X.card / s + s * ↑L.card

Parametric cell-decomposition bound. For any parameter $s \ge 1$, $I(X, L) \le |X|^{2/3} |L|^{2/3} + |X|/s + s|L|$. Optimizing in $s$ yields the Szemerédi--Trotter bound.

theorem SzemerediTrotter.szemeredi_trotter (X : Finset (Fin 2 → ℝ)) (L : Finset Line2) : ↑(incidenceCount X L) ≤ ↑X.card + ↑L.card + ↑X.card ^ (2 / 3) * ↑L.card ^ (2 / 3)

Szemerédi--Trotter incidence theorem. For any finite set of points $X \subset \mathbb{R}^2$ and lines $L$, $I(X, L) \le |X| + |L| + |X|^{2/3} |L|^{2/3}$.

noncomputable def SzemerediTrotter.rRichLines (X : Finset (Fin 2 → ℝ)) (L : Finset Line2) (R : ℕ) : Finset Line2

The subset of $R$-rich lines: lines $\ell \in L$ containing at least $R$ points of $X$.

theorem SzemerediTrotter.incidence_ge_R_mul_rRichLines (X : Finset (Fin 2 → ℝ)) (L : Finset Line2) (R : ℕ) : R * (rRichLines X L R).card ≤ incidenceCount X (rRichLines X L R)

Lower bound: the total incidence count restricted to $R$-rich lines is at least $R \cdot |L_R(X)|$, since each rich line contributes at least $R$ incidences.

theorem SzemerediTrotter.r_rich_lines_bound (X : Finset (Fin 2 → ℝ)) (L : Finset Line2) (R : ℕ) (hR : 2 ≤ R) : ∃ C > 0, ↑(rRichLines X L R).card ≤ C * (↑X.card ^ 2 / ↑R ^ 3 + ↑X.card / ↑R)

Bound on the number of $R$-rich lines. As a corollary of Szemerédi--Trotter: for $R \ge 2$, $|L_R(X)| \lesssim |X|^2/R^3 + |X|/R$. Here the constant is explicit ($C = 64$).

noncomputable def SzemerediTrotter.allLinesFromPairs (X : Finset (Fin 2 → ℝ)) : Finset Line2

The finite set of all lines spanned by pairs of distinct points of $X$.

noncomputable def SzemerediTrotter.allRichLines (X : Finset (Fin 2 → ℝ)) (R : ℕ) : Finset Line2

The set of $R$-rich lines among all lines spanned by pairs of points of $X$.

theorem SzemerediTrotter.r_rich_lines_bound_all (X : Finset (Fin 2 → ℝ)) (R : ℕ) (hR : 2 ≤ R) : ∃ C > 0, ↑(allRichLines X R).card ≤ C * (↑X.card ^ 2 / ↑R ^ 3 + ↑X.card / ↑R)

Bound on the number of $R$-rich lines (among all lines through point pairs of $X$): $|L_R(X)| \lesssim |X|^2/R^3 + |X|/R$.

noncomputable def ProjectionTheory.projR2 (θ : ℝ) (p : Fin 2 → ℝ) : ℝ

The orthogonal projection of $p \in \mathbb{R}^2$ in the direction $\theta$, i.e. $\pi_\theta(p) = p_0 \cos\theta + p_1 \sin\theta$.

noncomputable def ProjectionTheory.projImageR2 (θ : ℝ) (X : Finset (Fin 2 → ℝ)) : Finset ℝ

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

noncomputable def ProjectionTheory.projR2Lin (θ : ℝ) : (Fin 2 → ℝ) →ₗ[ℝ] ℝ

The direction-$\theta$ projection $\pi_\theta : \mathbb{R}^2 \to \mathbb{R}$ packaged as a linear map.

theorem ProjectionTheory.projR2Lin_surjective (θ : ℝ) : Function.Surjective ⇑(projR2Lin θ)

The projection map $\pi_\theta : \mathbb{R}^2 \to \mathbb{R}$ is surjective.

theorem ProjectionTheory.projR2Lin_ker_finrank (θ : ℝ) (hθ : 0 ≤ θ ∧ θ < Real.pi) : Module.finrank ℝ ↥(projR2Lin θ).ker = 1

For $\theta \in [0, \pi)$, the kernel of $\pi_\theta$ is a $1$-dimensional subspace of $\mathbb{R}^2$, so its fibers are honest lines.

noncomputable def ProjectionTheory.mkProjLine (θ : ℝ) (hθ : 0 ≤ θ ∧ θ < Real.pi) (p₀ : Fin 2 → ℝ) : SzemerediTrotter.Line2

The line through $p_0$ in direction $\theta \in [0, \pi)$: the fiber of $\pi_\theta$ passing through $p_0$, packaged as a Line2.

theorem ProjectionTheory.mem_mkProjLine_iff (θ : ℝ) (hθ : 0 ≤ θ ∧ θ < Real.pi) (p₀ q : Fin 2 → ℝ) : q ∈ (mkProjLine θ hθ p₀).carrier ↔ projR2 θ q = projR2 θ p₀

A point $q$ lies on the line mkProjLine θ p₀ iff $\pi_\theta(q) = \pi_\theta(p_0)$, i.e. iff $q$ is on the same projection fiber as $p_0$.

theorem ProjectionTheory.mkProjLine_eq_iff (θ : ℝ) (hθ : 0 ≤ θ ∧ θ < Real.pi) (p₀ q₀ : Fin 2 → ℝ) : mkProjLine θ hθ p₀ = mkProjLine θ hθ q₀ ↔ projR2 θ p₀ = projR2 θ q₀

Two projection lines through $p_0$ and $q_0$ in direction $\theta$ coincide iff $\pi_\theta(p_0) = \pi_\theta(q_0)$.

theorem ProjectionTheory.card_image_le_of_eq_imp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] (s : Finset α) (f : α → β) (g : α → γ) (h : ∀ a₁ ∈ s, ∀ a₂ ∈ s, g a₁ = g a₂ → f a₁ = f a₂) (hs : s.Nonempty) : (Finset.image f s).card ≤ (Finset.image g s).card

General image-counting lemma: if $g(a_1) = g(a_2)$ implies $f(a_1) = f(a_2)$ on $s$, then $|f(s)| \le |g(s)|$. Used to compare the cardinality of two images via a factoring through one of them.

theorem ProjectionTheory.proj_bound_of_st_ineq (Xr Sr Dr : ℝ) (hXr : Xr > 0) (hSr : Sr ≥ 1) (hDr : Dr ≥ 2) (h2S : 2 * Sr < Xr) (hST : Xr * Dr ≤ Xr + Sr * Dr + Xr ^ (2 / 3) * (Sr * Dr) ^ (2 / 3)) : Dr ≤ 144 * Sr ^ 2 * Xr⁻¹ + 1

Algebraic key lemma: from the Szemerédi--Trotter incidence inequality $X D \le X + S D + X^{2/3} (SD)^{2/3}$ with $2S < X$ and $D \ge 2$, deduce the projection bound $D \le 144 \cdot S^2 / X + 1$.

theorem ProjectionTheory.fiber_lines_st_bound (X : Finset (Fin 2 → ℝ)) (S : ℕ) (D : Finset ℝ) (hDr : ∀ θ ∈ D, 0 ≤ θ ∧ θ < Real.pi) (hSb : ∀ θ ∈ D, (projImageR2 θ X).card ≤ S) (hX : X.Nonempty) : ∃ (L : Finset SzemerediTrotter.Line2), L.card ≤ S * D.card ∧ X.card * D.card ≤ SzemerediTrotter.incidenceCount X L

Fiber lines construction. Given a set $X \subset \mathbb{R}^2$, a set of directions $D \subset [0, \pi)$, and an upper bound $|\pi_\theta(X)| \le S$ for every $\theta \in D$, one can construct a set of lines $L$ with $|L| \le S |D|$ and $|X| \cdot |D| \le I(X, L)$ (each point lies on exactly $|D|$ fibers).

theorem ProjectionTheory.szemeredi_trotter_proj : ∃ C > 0, ∀ (X : Finset (Fin 2 → ℝ)) (S : ℕ) (D : Finset ℝ), (∀ θ ∈ D, 0 ≤ θ ∧ θ < Real.pi) → (∀ θ ∈ D, (projImageR2 θ X).card ≤ S) → 2 * S < X.card → ↑D.card ≤ C * ↑S ^ 2 * (↑X.card)⁻¹ + 1

Szemerédi--Trotter projection theorem. There exists a universal constant $C > 0$ such that for any finite point set $X \subset \mathbb{R}^2$, set of directions $D \subset [0, \pi)$, and bound $|\pi_\theta(X)| \le S$ for $\theta \in D$, if $2S < |X|$ then $|D| \le C \cdot S^2 / |X| + 1$.