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{если } \\mathrm{turanDensity}(H) \\neq 0.$$$
Lean4
/-- `extremalNumber n H` is asymptotically equivalent to `turanDensity H * n.choose 2` as `n`
approaches `∞`. -/
theorem isEquivalent_extremalNumber (h : turanDensity H ≠ 0) :
(fun n ↦ (extremalNumber n H : ℝ)) ~[atTop] (fun n ↦ (turanDensity H * n.choose 2 : ℝ)) :=
by
have hπ := tendsto_turanDensity H
apply Tendsto.const_mul (1 / turanDensity H : ℝ)at hπ
simp_rw [one_div_mul_cancel h, div_mul_div_comm, one_mul] at hπ
have hz : ∀ᶠ (x : ℕ) in atTop, turanDensity H * x.choose 2 ≠ 0 :=
by
rw [eventually_atTop]
use 2
intro n hn
simp [h, Nat.choose_eq_zero_iff, hn]
simpa [isEquivalent_iff_tendsto_one hz] using hπ
