English
If Turán density is nonzero, extremalNumber(n,H) is asymptotically equivalent to Turán density(H) times n choose 2; i.e., extremalNumber(n,H) ~ turanDensity(H) · (n choose 2) as n → ∞.
Русский
Если Турванская плотность ненулевая, экстремальное число асимптотически эквивалентно Турванской плотности умноженной на (n choose 2).
LaTeX
$$$\\mathrm{extremalNumber}(n,H) \\sim \\mathrm{turanDensity}(H) \\cdot {n \\choose 2} \\quad (n \\to \\infty), \\quad \\text{provided } \\mathrm{turanDensity}(H) \\neq 0.$$$
Lean4
/-- The **Turán density** of a simple graph `H` is well-defined. -/
theorem tendsto_turanDensity (H : SimpleGraph W) :
Tendsto (fun n ↦ (extremalNumber n H / n.choose 2 : ℝ)) atTop (𝓝 (turanDensity H)) :=
by
let f := fun n ↦ (extremalNumber n H / n.choose 2 : ℝ)
suffices h : ∃ x, Tendsto (fun n ↦ f (n + 2)) atTop (𝓝 x)
by
obtain ⟨_, h⟩ := by simpa [tendsto_add_atTop_iff_nat 2] using h
simpa [← Tendsto.limUnder_eq h] using h
use ⨅ n, f (n + 2)
apply tendsto_atTop_ciInf
· rw [antitone_add_nat_iff_antitoneOn_nat_Ici]
exact antitoneOn_extremalNumber_div_choose_two H
· use 0
intro n ⟨_, hn⟩
rw [← hn]
positivity
