noncomputable def CrossingNumber.IsPlanarGraph (n m : ℕ) : Prop

Predicate stating that a graph with $n$ vertices and $m$ edges is planar (abstract placeholder for the planarity property used throughout this file).

theorem CrossingNumber.euler_formula_planar (n m : ℕ) (hn : 0 < n) (h : IsPlanarGraph n m) : m ≤ 3 * n

Euler's formula for planar graphs: a planar graph on $n \geq 1$ vertices has at most $3n$ edges, i.e., $m \leq 3n$.

theorem CrossingNumber.planarization_is_planar (n m cr : ℕ) : IsPlanarGraph n (m - cr)

A planarization of a graph: removing $cr$ crossing edges from a graph with $m$ edges yields a planar graph on the same $n$ vertices.

theorem CrossingNumber.euler_bound_planarized (n m cr : ℕ) (hn : 0 < n) : m - cr ≤ 3 * n

Combining planarization with Euler's bound: $m - cr \leq 3n$ for $n \geq 1$.

theorem CrossingNumber.cheap_bound (n m cr : ℕ) (hn : 0 < n) (_hm : 4 * n ≤ m) : m ≤ cr + 3 * n

The "cheap" crossing-number bound: if $4n \leq m$, then $m \leq cr + 3n$, i.e., $cr \geq m - 3n$.

noncomputable def CrossingNumber.expected_crossing_number (n m cr : ℕ) (p : ℝ) : ℝ

The expected number of crossings in a random subgraph where each vertex is kept independently with probability $p$ (abstract placeholder).

theorem CrossingNumber.expected_crossing_upper_bound (n m cr : ℕ) (hn : 0 < n) (hm : 4 * n ≤ m) (p : ℝ) (hp : 0 < p) (hp1 : p ≤ 1) : expected_crossing_number n m cr p ≤ p ^ 4 * ↑cr

Upper bound on the expected crossing number of a random induced subgraph: each of the $cr$ crossings survives with probability $p^4$, so $\mathbb{E}[cr'] \leq p^4 \cdot cr$.

theorem CrossingNumber.expected_crossing_lower_bound (n m cr : ℕ) (hn : 0 < n) (hm : 4 * n ≤ m) (p : ℝ) (hp : 0 < p) (hp1 : p ≤ 1) : p ^ 2 * ↑m - 3 * p * ↑n ≤ expected_crossing_number n m cr p

Lower bound for the expected crossing number from the cheap bound applied to the random subgraph: $p^2 m - 3 p n \leq \mathbb{E}[cr']$.

theorem CrossingNumber.random_subgraph_expectations (n m cr : ℕ) (hn : 0 < n) (hm : 4 * n ≤ m) (p : ℝ) (hp : 0 < p) (hp1 : p ≤ 1) : ∃ (E_cr : ℝ), p ^ 2 * ↑m - 3 * p * ↑n ≤ E_cr ∧ E_cr ≤ p ^ 4 * ↑cr

Combined expectations for the random subgraph: there exists $\mathbb{E}[cr']$ sandwiched between the linear lower bound and the $p^4 \cdot cr$ upper bound.

theorem CrossingNumber.subgraph_bound (n m cr : ℕ) (hn : 0 < n) (hm : 4 * n ≤ m) (p : ℝ) : 0 < p → p ≤ 1 → p ^ 4 * ↑cr ≥ p ^ 2 * ↑m - 3 * p * ↑n

For any $p \in (0,1]$, the random-subgraph inequality $p^4 \cdot cr \geq p^2 m - 3 p n$ holds, obtained by combining the two expectation bounds.

theorem CrossingNumber.crossing_number_inequality (n m cr : ℕ) (hn : 0 < n) (hm : 4 * n ≤ m) : 64 * n ^ 2 * cr ≥ m ^ 3

Crossing number inequality (Theorem 2.6.2). For any graph with $|V| = n \geq 1$ and $|E| = m \geq 4n$, the crossing number satisfies $64 n^2 \cdot cr(G) \geq m^3$, i.e., $cr(G) \gtrsim m^3 / n^2$.

theorem CrossingNumber.crossing_number_corollary (n m cr : ℕ) (hn : 4 ≤ n) (hm : n ^ 2 ≤ m) : 64 * cr ≥ n ^ 4

Corollary 2.6.4 of the crossing number inequality. If $n \geq 4$ and $|E| \geq n^2$, then the crossing number is bounded below by $cr(G) \geq n^4 / 64$.