turanDensity — Mathlib

English

The Turán density of a graph H is defined as the limit of extremalNumber(n,H) divided by n choose 2 as n tends to infinity.

Русский

Турaновская плотность графа H определяется как предел отношения экстремального числа к \\binom{n}{2} при $n\\to\\infty$.

LaTeX

$$$\\operatorname{turanDensity}(H) = \\lim_{n\\to\\infty} \\frac{\\mathrm{extremalNumber}(n,H)}{\\binom{n}{2}}.$$$

Lean4

/-- The **Turán density** of a simple graph `H` is the limit of `extremalNumber n H / n.choose 2`
as `n` approaches `∞`.

See `SimpleGraph.tendsto_turanDensity` for proof of existence. -/
noncomputable def turanDensity (H : SimpleGraph W) :=
  limUnder atTop fun n ↦ (extremalNumber n H / n.choose 2 : ℝ)

Похожие утверждения