Turán density

This files defines the Turán density of a simple graph.

Main definitions

• SimpleGraph.turanDensity H is the Turán density of the simple graph H, defined as the limit of extremalNumber n H / n.choose 2 as n approaches ∞.

• SimpleGraph.tendsto_turanDensity is the proof that SimpleGraph.turanDensity is well-defined.

• SimpleGraph.isEquivalent_extremalNumber is the proof that extremalNumber n H is asymptotically equivalent to turanDensity H * n.choose 2 as n approaches ∞.

theorem SimpleGraph.antitoneOn_extremalNumber_div_choose_two {W : Type u_2} (H : SimpleGraph W) : AntitoneOn (fun (n : ℕ) => ↑(extremalNumber n H) / ↑(n.choose 2)) (Set.Ici 2)

noncomputable def SimpleGraph.turanDensity {W : Type u_2} (H : SimpleGraph W) : ℝ

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.

Equations

• H.turanDensity = limUnder Filter.atTop fun (n : ℕ) => ↑(SimpleGraph.extremalNumber n H) / ↑(n.choose 2)

theorem SimpleGraph.tendsto_turanDensity {W : Type u_2} (H : SimpleGraph W) : Filter.Tendsto (fun (n : ℕ) => ↑(extremalNumber n H) / ↑(n.choose 2)) Filter.atTop (nhds H.turanDensity)

The Turán density of a simple graph H is well-defined.

theorem SimpleGraph.isEquivalent_extremalNumber {W : Type u_2} {H : SimpleGraph W} (h : H.turanDensity ≠ 0) : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(extremalNumber n H)) fun (n : ℕ) => H.turanDensity * ↑(n.choose 2)

extremalNumber n H is asymptotically equivalent to turanDensity H * n.choose 2 as n approaches ∞.