noncomputable def Hajos.hajosParam (n : ℕ) : ℕ

The threshold $t = \lceil 10 \sqrt{n} \rceil$ used in Theorem 5.3.2: we show that $G(n, 1/2)$ has no $K_t$-subdivision with high probability.

noncomputable def Hajos.subdivisionUnionBound (n : ℕ) : ℝ

The union bound on the probability that $G(n, 1/2)$ contains a $K_t$-subdivision, for $t = \lceil 10\sqrt n \rceil$: $\binom{n}{t} \cdot e^{-t^2/10}$.

theorem Hajos.hajosParam_ge (n : ℕ) : 10 * √↑n ≤ ↑(hajosParam n)

Lower bound on hajosParam: $10\sqrt n \leq \lceil 10\sqrt n \rceil$.

theorem Hajos.hajosParam_le (n : ℕ) : ↑(hajosParam n) ≤ 10 * √↑n + 1

Upper bound on hajosParam: $\lceil 10\sqrt n \rceil \leq 10\sqrt n + 1$.

theorem Hajos.hajosParam_sq_ge (n : ℕ) : 100 * ↑n ≤ ↑(hajosParam n) ^ 2

Squaring the lower bound on hajosParam: $100 n \leq t^2$.

theorem Hajos.subdivisionUnionBound_nonneg (n : ℕ) : 0 ≤ subdivisionUnionBound n

The union bound subdivisionUnionBound is nonnegative.

theorem Hajos.log_le_sqrt_div_ten : ∀ᶠ (n : ℕ) in Filter.atTop, Real.log ↑n ≤ 1 / 10 * √↑n

For all sufficiently large $n$, $\log n \leq \tfrac{1}{10} \sqrt n$.

theorem Hajos.hajosParam_log_bound : ∀ᶠ (n : ℕ) in Filter.atTop, ↑(hajosParam n) * Real.log ↑n ≤ 2 * ↑n

Asymptotic comparison: for all sufficiently large $n$, $t \log n \leq 2n$ where $t = \lceil 10\sqrt n \rceil$.

theorem Hajos.pow_eq_exp_mul_log (n : ℕ) (hn : 0 < ↑n) (t : ℕ) : ↑n ^ t = Real.exp (↑t * Real.log ↑n)

Rewrite a natural power as $n^t = \exp(t \log n)$ when $n > 0$.

theorem Hajos.tendsto_exp_neg_nat : Filter.Tendsto (fun (n : ℕ) => Real.exp (-↑n)) Filter.atTop (nhds 0)

The sequence $e^{-n}$ tends to $0$ as $n \to \infty$.

theorem Hajos.subdivisionUnionBound_le_exp : ∀ᶠ (n : ℕ) in Filter.atTop, subdivisionUnionBound n ≤ Real.exp (-↑n)

For all sufficiently large $n$, $\binom{n}{t} e^{-t^2/10} \leq e^{-n}$ with $t = \lceil 10\sqrt n \rceil$.

theorem Hajos.subdivision_union_bound_tendsto_zero : Filter.Tendsto subdivisionUnionBound Filter.atTop (nhds 0)

The union bound subdivisionUnionBound n tends to $0$ as $n \to \infty$.

theorem Hajos.hajos_conjecture_counterexample (probKtSubdiv : ℕ → ℝ) (hP_nonneg : ∀ (n : ℕ), 0 ≤ probKtSubdiv n) (hP_le : ∀ (n : ℕ), probKtSubdiv n ≤ subdivisionUnionBound n) : Filter.Tendsto probKtSubdiv Filter.atTop (nhds 0)

Counterexample to Hajós's conjecture (Theorem 5.3.2). If $\text{probKtSubdiv}(n)$ is the probability that $G(n, 1/2)$ contains a $K_t$-subdivision with $t = \lceil 10\sqrt n \rceil$, and is dominated by the union bound, then it tends to $0$, giving a $K_t$-subdivision-free graph of chromatic number $\Omega(n / \log n)$ asymptotically larger than $t$.