Turán density

This file 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 ∞.

• SimpleGraph.isContained_of_card_edgeFinset: simple graphs on n vertices with at least (turanDensity H + o(1)) * n ^ 2 edges contain H, for all sufficently large n.

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

noncomputable def SimpleGraph.turanDensity {W : Type u_1} (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.isGLB_turanDensity {W : Type u_1} (H : SimpleGraph W) : IsGLB {x : ℝ | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x} H.turanDensity

theorem SimpleGraph.turanDensity_eq_csInf {W : Type u_1} (H : SimpleGraph W) : H.turanDensity = sInf {x : ℝ | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}

theorem SimpleGraph.tendsto_turanDensity {W : Type u_1} (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_1} {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 ∞.

theorem SimpleGraph.eventually_isContained_of_card_edgeFinset {W : Type u_1} (H : SimpleGraph W) {ε : ℝ} (hε_pos : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj], ↑G.edgeFinset.card ≥ (H.turanDensity + ε) * ↑(n.choose 2) → H.IsContained G

Simple graphs on n vertices having at least (turanDensity H + o(1)) * n ^ 2 edges contain H, for sufficiently large n.

@[reducible, inline]

noncomputable abbrev SimpleGraph.turanDensityConst {W : Type u_1} (H : SimpleGraph W) (ε : ℝ) : ℕ

The edge density of H-free simple graphs on turanDensityConst H ε vertices is at most turanDensity H + ε.

Contrapositively, turanDensity H + ε is the density at which H is always contained in simple graphs on turanDensityConst H ε vertices.

Note that this value is only defined for positive ε and turanDensityConst H ε = 0 for non positive ε.

Equations

• H.turanDensityConst ε = if h : ε > 0 then Nat.find ⋯ else 0

theorem SimpleGraph.isContained_of_card_edgeFinset {W : Type u_1} (H : SimpleGraph W) {ε : ℝ} (hε_pos : 0 < ε) {V : Type u_2} [Fintype V] (h_verts : Fintype.card V ≥ H.turanDensityConst ε) (G : SimpleGraph V) [DecidableRel G.Adj] : ↑G.edgeFinset.card ≥ (H.turanDensity + ε) * ↑((Fintype.card V).choose 2) → H.IsContained G

Simple graphs on card V vertices having at least (turanDensity H + o(1)) * (card V) ^ 2 edges contain H, for sufficiently large card V.