Dense Graph Limits

Results named in Tau Ceti's TauCeti.Combinatorics.DenseGraphLimits modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremGoodman's inequality#

For every graphon, triangle density is at least 2 * t(K₂, W)^2 - t(K₂, W).

TauCeti.DenseGraphLimits.goodman_triangle_density.{u_1} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  (W : TauCeti.DenseGraphLimits.Graphon Ω μ) :
  2 * TauCeti.DenseGraphLimits.homDensity ⊤ W ^ 2 - TauCeti.DenseGraphLimits.homDensity ⊤ W ≤
    TauCeti.DenseGraphLimits.homDensity ⊤ W

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.goodman_triangle_density.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.goodman_triangle_density
• Source of TauCeti.DenseGraphLimits.goodman_triangle_density in TauCeti/Combinatorics/DenseGraphLimits/Applications.lean

LeanTauCeti.DenseGraphLimits.goodman_triangle_density

Used by 1

Used byMantel's inequality for graphons

TheoremMantel's inequality for graphons#

A graphon with zero triangle density has edge density at most 1 / 2.

TauCeti.DenseGraphLimits.mantel_triangle_free.{u_1} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  (W : TauCeti.DenseGraphLimits.Graphon Ω μ)
  (htriangle : TauCeti.DenseGraphLimits.homDensity ⊤ W = 0) :
  TauCeti.DenseGraphLimits.homDensity ⊤ W ≤ 1 / 2

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.mantel_triangle_free.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.mantel_triangle_free
• Source of TauCeti.DenseGraphLimits.mantel_triangle_free in TauCeti/Combinatorics/DenseGraphLimits/Applications.lean

LeanTauCeti.DenseGraphLimits.mantel_triangle_free

Uses 1

Proof usesGoodman's inequality

TheoremSidorenko's inequality for the 4-cycle#

The 4-cycle homomorphism density is at least the fourth power of the edge density, on every probability carrier. This is the graphon form of the K_{2,2} case in Y. Zhao, Graph Theory and Additive Combinatorics, Theorem 5.2.1.

TauCeti.DenseGraphLimits.sidorenko_cycleGraph_four.{u_1} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  (W : TauCeti.DenseGraphLimits.Graphon Ω μ) :
  TauCeti.DenseGraphLimits.homDensity (SimpleGraph.cycleGraph 4) W ≥
    TauCeti.DenseGraphLimits.homDensity ⊤ W ^ 4

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.sidorenko_cycleGraph_four.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.sidorenko_cycleGraph_four
• Source of TauCeti.DenseGraphLimits.sidorenko_cycleGraph_four in TauCeti/Combinatorics/DenseGraphLimits/Applications.lean

LeanTauCeti.DenseGraphLimits.sidorenko_cycleGraph_four

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.