def BeckTheorem.IsLine (L : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2))) : Prop

An affine subspace L ⊆ ℝ² is a line iff its direction has dimension 1.

noncomputable def BeckTheorem.pointsOnLine (E : Finset (EuclideanSpace ℝ (Fin 2))) (L : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2))) : ℕ

The number of points of the finite set E ⊂ ℝ² lying on the line L.

def BeckTheorem.determinedLines (E : Finset (EuclideanSpace ℝ (Fin 2))) : Set (AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)))

The set of lines determined by E: lines that contain at least two points of E.

noncomputable def BeckTheorem.linesThrough (E : Finset (EuclideanSpace ℝ (Fin 2))) (x : EuclideanSpace ℝ (Fin 2)) : Set (AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)))

The set of lines through x ∈ ℝ² which are determined by E, i.e. pass through x and at least one other point of E.

theorem BeckTheorem.beck_theorem : ∃ (c : ℝ), 0 < c ∧ ∀ (E : Finset (EuclideanSpace ℝ (Fin 2))), (∃ (L : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2))), IsLine L ∧ ↑E.card / 100 ≤ ↑(pointsOnLine E L)) ∨ c * ↑E.card ^ 2 ≤ ↑(determinedLines E).ncard

Beck's theorem (1982). There exists c > 0 such that for every finite point set E ⊂ ℝ², either some line contains at least |E|/100 points of E, or E determines at least c · |E|² distinct lines.

theorem BeckTheorem.st_uniformization_per_point (c : ℝ) (hc : 0 < c) : ∃ (c' : ℝ), 0 < c' ∧ ∀ (E : Finset (EuclideanSpace ℝ (Fin 2))), (∀ (L : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2))), IsLine L → ↑(pointsOnLine E L) ≤ ↑E.card / 2) → c * ↑E.card ^ 2 ≤ ↑(determinedLines E).ncard → ∀ x ∈ E, c' * ↑E.card ≤ ↑(linesThrough E x).ncard

Per-point uniformization of the Szemerédi–Trotter consequence of Beck: if no line contains more than |E|/2 points and E determines ≥ c |E|² lines, then through every point of E there pass ≳ |E| determined lines.

theorem BeckTheorem.lines_per_point_from_rich_line (E : Finset (EuclideanSpace ℝ (Fin 2))) (hconc : ∀ (L : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2))), IsLine L → ↑(pointsOnLine E L) ≤ ↑E.card / 2) (L : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2))) (hL_line : IsLine L) (hL_rich : ↑E.card / 100 ≤ ↑(pointsOnLine E L)) (x : EuclideanSpace ℝ (Fin 2)) (hx : x ∈ E) : 1 / 100 * ↑E.card ≤ ↑(linesThrough E x).ncard

If no line contains more than |E|/2 points yet some line L contains at least |E|/100 points, then every x ∈ E has at least |E|/100 lines through it determined by E (using the rich line L to construct many such lines through x).

theorem BeckTheorem.beck_theorem_lines_per_point : ∃ (c : ℝ), 0 < c ∧ ∀ (E : Finset (EuclideanSpace ℝ (Fin 2))), (∀ (L : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2))), IsLine L → ↑(pointsOnLine E L) ≤ ↑E.card / 2) → ∀ x ∈ E, c * ↑E.card ≤ ↑(linesThrough E x).ncard

Beck's theorem, per-point form. There is c > 0 such that for any finite E ⊂ ℝ² with no line containing more than |E|/2 points, every point x ∈ E has at least c · |E| lines through it that are determined by E (i.e. pass through x and another point of E).