def Heilbronn.unitSquare : Set (ℝ × ℝ)

The closed unit square $[0,1]^2 \subseteq \mathbb{R}^2$.

noncomputable def Heilbronn.triangleArea (p q r : ℝ × ℝ) : ℝ

The area of the triangle with vertices $p, q, r \in \mathbb{R}^2$, computed via the absolute value of half the cross product of $(q-p)$ and $(r-p)$.

noncomputable def Heilbronn.minTriangleArea (S : Finset (ℝ × ℝ)) : ℝ

The minimum triangle area among all triples of distinct points in a finite set $S \subseteq \mathbb{R}^2$.

noncomputable def Heilbronn.heilbronnNumber (n : ℕ) : ℝ

The Heilbronn number $H(n)$: the supremum, over all $n$-point configurations in the unit square, of the minimum triangle area among triples of points in the configuration.

noncomputable def Heilbronn.parabolaPoint (p : ℕ) (i : Fin p) : ℝ × ℝ

For prime $p$ and $i \in \{0, 1, \dots, p-1\}$, the point $(i/p, (i^2 \bmod p)/p)$ on the discretized parabola in the unit square.

def Heilbronn.intDetFin {p : ℕ} (a b c : Fin p) : ℤ

The integer cross-product determinant associated with three points on the parabola at indices $a, b, c \in \mathbb{F}_p$.

theorem Heilbronn.intDetFin_cast_eq_vandermonde {p : ℕ} (a b c : Fin p) : ↑(intDetFin a b c) = (↑↑b - ↑↑a) * (↑↑c - ↑↑a) * (↑↑c - ↑↑b)

Modulo $p$, the determinant intDetFin a b c equals the Vandermonde-type product $(b-a)(c-a)(c-b)$ in $\mathbb{F}_p$.

theorem Heilbronn.fin_eq_of_zmod_eq {p : ℕ} (a b : Fin p) (h : ↑↑a = ↑↑b) : a = b

Two elements of Fin p are equal whenever their values agree in $\mathbb{Z}/p\mathbb{Z}$.

theorem Heilbronn.intDetFin_ne_zero {p : ℕ} (hp : Nat.Prime p) (a b c : Fin p) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : intDetFin a b c ≠ 0

For prime $p$ and pairwise distinct $a, b, c \in \mathbb{F}_p$, the determinant intDetFin a b c is nonzero, since the Vandermonde product modulo $p$ is nonzero.

theorem Heilbronn.cross_product_formula (p : ℕ) (hp : 0 < p) (a b c : Fin p) : ((parabolaPoint p b).1 - (parabolaPoint p a).1) * ((parabolaPoint p c).2 - (parabolaPoint p a).2) - ((parabolaPoint p b).2 - (parabolaPoint p a).2) * ((parabolaPoint p c).1 - (parabolaPoint p a).1) = ↑(intDetFin a b c) / ↑p ^ 2

The signed area cross-product of three parabola points equals the integer determinant intDetFin a b c divided by $p^2$.

theorem Heilbronn.triangleArea_parabolaPoint_bound {p : ℕ} (hp : Nat.Prime p) (a b c : Fin p) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : triangleArea (parabolaPoint p a) (parabolaPoint p b) (parabolaPoint p c) ≥ 1 / (2 * ↑p ^ 2)

For prime $p$ and pairwise distinct indices, any triangle formed by three parabola points has area at least $\frac{1}{2p^2}$.

theorem Heilbronn.parabolaPoint_injective {p : ℕ} (hp : 0 < p) : Function.Injective (parabolaPoint p)

The map parabolaPoint p from Fin p to $\mathbb{R}^2$ is injective.

theorem Heilbronn.parabolaPoint_mem_unitSquare {p : ℕ} (hp : Nat.Prime p) (i : Fin p) : parabolaPoint p i ∈ unitSquare

Each parabola point $(i/p, (i^2 \bmod p)/p)$ lies in the closed unit square $[0,1]^2$.

theorem Heilbronn.heilbronn_lower_bound : ∃ c > 0, ∀ n ≥ 3, ∃ (S : Finset (ℝ × ℝ)), S.card = n ∧ ↑S ⊆ unitSquare ∧ ∀ x ∈ S, ∀ y ∈ S, ∀ z ∈ S, x ≠ y → x ≠ z → y ≠ z → triangleArea x y z ≥ c / ↑n ^ 2

Theorem 3.2.3 (Heilbronn lower bound). There exists a constant $c > 0$ such that for every $n \geq 3$ there are $n$ points in the unit square $[0,1]^2$ with every triangle they form having area at least $c/n^2$.