Dense graph limits and graphons

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremThe Lovász–Szegedy characterization of homomorphism densities#

A graph parameter is the homomorphism density of a graphon on an atomless standard Borel carrier (Ω, μ), such as the unit interval, if and only if it is isomorphism invariant, multiplicative, normalized and reflection positive.

TauCeti.DenseGraphLimits.lovasz_szegedy_representability.{u_1} {Ω : Type u_1} [MeasurableSpace Ω]
  [StandardBorelSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.NullSingletonClass μ] (f : TauCeti.DenseGraphLimits.GraphParam) :
  (∃ W,
      ∀ (n : ℕ) (F : SimpleGraph (Fin n)) [inst : DecidableRel F.Adj],
        f n F = TauCeti.DenseGraphLimits.homDensity F W) ↔
    TauCeti.DenseGraphLimits.IsIsoInvariant f ∧
      TauCeti.DenseGraphLimits.IsMultiplicative f ∧
        TauCeti.DenseGraphLimits.IsNormalized f ∧ TauCeti.DenseGraphLimits.IsReflectionPositive f

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.lovasz_szegedy_representability.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.lovasz_szegedy_representability
• Source of TauCeti.DenseGraphLimits.lovasz_szegedy_representability in TauCeti/Combinatorics/DenseGraphLimits/Representability/Representation.lean
• Tau Ceti roadmap status: Dense graph limits and graphons

LeanTauCeti.DenseGraphLimits.lovasz_szegedy_representability

Uses 4

Proof usesFrieze--Kannan weak regularity · TauCeti.DenseGraphLimits.cutDist · TauCeti.DenseGraphLimits.cutDist_triangle · TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr

TheoremEvery exchangeable law on infinite graphs is a graphon mixture, for exactly one mixing measure#

The integral form of the Diaconis–Janson correspondence: the law is the bind of a unique probability measure on graphon space against the joint sampling laws.

TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.existsUnique_bind_infiniteSampleLawOnSpace
  (L : TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw) :
  ∃! P, (↑P).bind TauCeti.DenseGraphLimits.infiniteSampleLawOnSpace = L.law

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.existsUnique_bind_infiniteSampleLawOnSpace.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.existsUnique_bind_infiniteSampleLawOnSpace
• Source of TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.existsUnique_bind_infiniteSampleLawOnSpace in TauCeti/Combinatorics/DenseGraphLimits/ExchangeableGraphLaw/Infinite/Mixture.lean
• Tau Ceti roadmap status: Dense graph limits and graphons

LeanTauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.existsUnique_bind_infiniteSampleLawOnSpace

Uses 3

Proof usesFrieze--Kannan weak regularity · TauCeti.DenseGraphLimits.cutDist · TauCeti.DenseGraphLimits.cutDist_triangle

TheoremDissociated relational laws of graphs are graphon sampling laws#

An exchangeable relational law of the language of graphs whose marginals are concentrated on simple graphs is dissociated exactly when it is the relational law of the sampling law of a graphon, which may be taken on any atomless standard Borel carrier (Ω, μ), such as the unit interval.

TauCeti.DenseGraphLimits.isDissociated_iff_exists_toRelationalLaw_sampleExchangeableLaw.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Ω] [MeasureTheory.NullSingletonClass μ]
  {ν : TauCeti.Probability.ExchangeableRelationalLaw FirstOrder.Language.graph}
  (hν :
    ∀ (n : ℕ),
      ∀ᵐ (c : TauCeti.RelationalConfiguration FirstOrder.Language.graph (Fin n)) ∂ν.law n,
        c.IsSimpleGraph) :
  ν.IsDissociated ↔ ∃ W, ν = (TauCeti.DenseGraphLimits.sampleExchangeableLaw W).toRelationalLaw

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.isDissociated_iff_exists_toRelationalLaw_sampleExchangeableLaw.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.isDissociated_iff_exists_toRelationalLaw_sampleExchangeableLaw
• Source of TauCeti.DenseGraphLimits.isDissociated_iff_exists_toRelationalLaw_sampleExchangeableLaw in TauCeti/Combinatorics/DenseGraphLimits/ExchangeableGraphLaw/Relational/Dissociated.lean
• Tau Ceti roadmap status: Dense graph limits and graphons

LeanTauCeti.DenseGraphLimits.isDissociated_iff_exists_toRelationalLaw_sampleExchangeableLaw

Uses 5

Statement usesTauCeti.Probability.ExchangeableRelationalLaw

Proof usesFrieze--Kannan weak regularity · TauCeti.DenseGraphLimits.cutDist · TauCeti.DenseGraphLimits.cutDist_triangle · TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr

TheoremCut-distance convergence is convergence of all homomorphism densities#

Cut-distance convergence is convergence of all homomorphism densities, for graphons on arbitrary, possibly different, probability carriers, indexed by any type and taken along any filter: δ□(Wᵢ, W) → 0 if and only if t(F, Wᵢ) → t(F, W) for every finite simple graph F. Sequences are the case of atTop on ℕ.

TauCeti.DenseGraphLimits.tendsto_cutDist_iff_forall_homDensity_tendsto.{u_1, u_3, u_4}
  {Ω' : Type u_1} [MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'}
  [MeasureTheory.IsProbabilityMeasure μ'] {ι : Type u_3} {l : Filter ι} {Ωι : ι → Type u_4}
  [(i : ι) → MeasurableSpace (Ωι i)] {μι : (i : ι) → MeasureTheory.Measure (Ωι i)}
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μι i)]
  (Ws : (i : ι) → TauCeti.DenseGraphLimits.Graphon (Ωι i) (μι i))
  (W : TauCeti.DenseGraphLimits.Graphon Ω' μ') :
  Filter.Tendsto (fun i => TauCeti.DenseGraphLimits.cutDist (Ws i) W) l (nhds 0) ↔
    ∀ (n : ℕ) (F : SimpleGraph (Fin n)) [inst : DecidableRel F.Adj],
      Filter.Tendsto (fun i => TauCeti.DenseGraphLimits.homDensity F (Ws i)) l
        (nhds (TauCeti.DenseGraphLimits.homDensity F W))

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.tendsto_cutDist_iff_forall_homDensity_tendsto.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.tendsto_cutDist_iff_forall_homDensity_tendsto
• Source of TauCeti.DenseGraphLimits.tendsto_cutDist_iff_forall_homDensity_tendsto in TauCeti/Combinatorics/DenseGraphLimits/GraphonSpace/Convergence.lean
• Tau Ceti roadmap status: Dense graph limits and graphons

LeanTauCeti.DenseGraphLimits.tendsto_cutDist_iff_forall_homDensity_tendsto

Uses 4 · Used by 1

Statement usesTauCeti.DenseGraphLimits.cutDist

Proof usesFrieze--Kannan weak regularity · TauCeti.DenseGraphLimits.cutDist_triangle · TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr

Used byEvery convergent graph sequence has a limit graphon

TheoremEvery convergent graph sequence has a limit graphon#

Every convergent graph sequence has a limit graphon (Lovász--Szegedy), on every atomless standard Borel carrier (Ω, μ), such as the unit interval. A sequence of finite graphs on nonempty vertex sets converges in the cut distance of step graphons to some graphon on (Ω, μ) if and only if every finite homomorphism density t(F, Gₙ) is a Cauchy, hence convergent, sequence.

TauCeti.DenseGraphLimits.exists_graphon_tendsto_cutDist_finiteGraphGraphon_iff_forall_homDensityFin_cauchySeq.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure μ] {m : ℕ → ℕ} [StandardBorelSpace Ω]
  [MeasureTheory.NullSingletonClass μ] (hm : ∀ (n : ℕ), 0 < m n)
  (G : (n : ℕ) → SimpleGraph (Fin (m n))) :
  (∃ W,
      Filter.Tendsto
        (fun n =>
          TauCeti.DenseGraphLimits.cutDist (TauCeti.DenseGraphLimits.finiteGraphGraphon (G n)) W)
        Filter.atTop (nhds 0)) ↔
    ∀ (n : ℕ) (F : SimpleGraph (Fin n)) [DecidableRel F.Adj],
      CauchySeq fun k => TauCeti.DenseGraphLimits.homDensityFin F (G k)

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.exists_graphon_tendsto_cutDist_finiteGraphGraphon_iff_forall_homDensityFin_cauchySeq.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.exists_graphon_tendsto_cutDist_finiteGraphGraphon_iff_forall_homDensityFin_cauchySeq
• Source of TauCeti.DenseGraphLimits.exists_graphon_tendsto_cutDist_finiteGraphGraphon_iff_forall_homDensityFin_cauchySeq in TauCeti/Combinatorics/DenseGraphLimits/GraphonSpace/Convergence.lean
• Tau Ceti roadmap status: Dense graph limits and graphons

LeanTauCeti.DenseGraphLimits.exists_graphon_tendsto_cutDist_finiteGraphGraphon_iff_forall_homDensityFin_cauchySeq

Uses 5

Statement usesTauCeti.DenseGraphLimits.cutDist

Proof usesCut-distance convergence is convergence of all homomorphism densities · Frieze--Kannan weak regularity · TauCeti.DenseGraphLimits.cutDist_triangle · TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr

TheoremLovász--Szegedy compactness over atomless standard Borel carriers#

The cut-distance quotient of graphons on a standard Borel space with an atomless probability measure is a compact metric space, being isometric to GraphonSpaceI.

TauCeti.DenseGraphLimits.GraphonSpace.instCompactSpace.{u_1} {Ω : Type u_1} [MeasurableSpace Ω]
  [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.NullSingletonClass μ] : CompactSpace (TauCeti.DenseGraphLimits.GraphonSpace Ω μ)

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.GraphonSpace.instCompactSpace.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.GraphonSpace.instCompactSpace
• Source of TauCeti.DenseGraphLimits.GraphonSpace.instCompactSpace in TauCeti/Combinatorics/DenseGraphLimits/GraphonSpace/Compact.lean
• Tau Ceti roadmap status: Dense graph limits and graphons

LeanTauCeti.DenseGraphLimits.GraphonSpace.instCompactSpace

Uses 4

Proof usesFrieze--Kannan weak regularity · TauCeti.DenseGraphLimits.cutDist · TauCeti.DenseGraphLimits.cutDist_triangle · TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr

TheoremFrieze--Kannan weak regularity#

Every graphon has a measurable block-average step graphon within ε in cut norm, on a partition with at most 4 ^ ⌈1 / ε²⌉ parts.

TauCeti.DenseGraphLimits.weak_regularity_frieze_kannan.{u_1} {Ω : Type u_1} [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ]
  (W : TauCeti.DenseGraphLimits.Graphon Ω μ) {ε : ℝ} (hε : 0 < ε) :
  ∃ P,
    ∃ (hP : ∀ p ∈ P.parts, MeasurableSet p),
      P.parts.card ≤ 4 ^ ⌈1 / ε ^ 2⌉₊ ∧
        TauCeti.DenseGraphLimits.cutNorm μ
            (W.toSymmKernel - (TauCeti.DenseGraphLimits.stepGraphonAvg P hP W).toSymmKernel) ≤
          ε

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.weak_regularity_frieze_kannan.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.weak_regularity_frieze_kannan
• Source of TauCeti.DenseGraphLimits.weak_regularity_frieze_kannan in TauCeti/Combinatorics/DenseGraphLimits/StepGraphon/Regularity.lean
• Tau Ceti roadmap status: Dense graph limits and graphons

LeanTauCeti.DenseGraphLimits.weak_regularity_frieze_kannan

Used by 7

Used byCut-distance convergence is convergence of all homomorphism densities · Dissociated relational laws of graphs are graphon sampling laws · Every convergent graph sequence has a limit graphon · Every exchangeable law on infinite graphs is a graphon mixture, for exactly one mixing measure · Lovász--Szegedy compactness over atomless standard Borel carriers · TauCeti.DenseGraphLimits.cutDist_triangle · The Lovász–Szegedy characterization of homomorphism densities

DefinitionTauCeti.DenseGraphLimits.cutDist#

The cut distance of two graphons: the infimum, over couplings of their carriers, of the cut norm of the overlaid difference.

The two graphons may live on different probability spaces, and no standard Borel or atomless hypothesis is imposed on either.

TauCeti.DenseGraphLimits.cutDist.{u_1, u_2} {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁]
  [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂}
  [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂]
  (U : TauCeti.DenseGraphLimits.Graphon Ω₁ μ₁) (W : TauCeti.DenseGraphLimits.Graphon Ω₂ μ₂) : ℝ

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.cutDist.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.cutDist
• Source of TauCeti.DenseGraphLimits.cutDist in TauCeti/Combinatorics/DenseGraphLimits/CutMetric/Distance.lean
• Tau Ceti roadmap status: Dense graph limits and graphons

LeanTauCeti.DenseGraphLimits.cutDist

Used by 8

Used byCut-distance convergence is convergence of all homomorphism densities · Dissociated relational laws of graphs are graphon sampling laws · Every convergent graph sequence has a limit graphon · Every exchangeable law on infinite graphs is a graphon mixture, for exactly one mixing measure · Lovász--Szegedy compactness over atomless standard Borel carriers · TauCeti.DenseGraphLimits.cutDist_triangle · TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr · The Lovász–Szegedy characterization of homomorphism densities

TheoremTauCeti.DenseGraphLimits.cutDist_triangle#

The coupling-primary graphon cut distance satisfies the triangle inequality on arbitrary probability carriers.

TauCeti.DenseGraphLimits.cutDist_triangle.{u_1, u_2, u_3} {Ω₁ : Type u_1} {Ω₂ : Type u_2}
  {Ω₃ : Type u_3} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] [MeasurableSpace Ω₃]
  {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} {μ₃ : MeasureTheory.Measure Ω₃}
  [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂]
  [MeasureTheory.IsProbabilityMeasure μ₃] (U : TauCeti.DenseGraphLimits.Graphon Ω₁ μ₁)
  (W : TauCeti.DenseGraphLimits.Graphon Ω₂ μ₂) (X : TauCeti.DenseGraphLimits.Graphon Ω₃ μ₃) :
  TauCeti.DenseGraphLimits.cutDist U X ≤
    TauCeti.DenseGraphLimits.cutDist U W + TauCeti.DenseGraphLimits.cutDist W X

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.cutDist_triangle.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.cutDist_triangle
• Source of TauCeti.DenseGraphLimits.cutDist_triangle in TauCeti/Combinatorics/DenseGraphLimits/CutMetric/Triangle.lean
• Tau Ceti roadmap status: Dense graph limits and graphons

LeanTauCeti.DenseGraphLimits.cutDist_triangle

Uses 2 · Used by 7

Statement usesTauCeti.DenseGraphLimits.cutDist

Proof usesFrieze--Kannan weak regularity

Used byCut-distance convergence is convergence of all homomorphism densities · Dissociated relational laws of graphs are graphon sampling laws · Every convergent graph sequence has a limit graphon · Every exchangeable law on infinite graphs is a graphon mixture, for exactly one mixing measure · Lovász--Szegedy compactness over atomless standard Borel carriers · TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr · The Lovász–Szegedy characterization of homomorphism densities

DefinitionTauCeti.DenseGraphLimits.Graphon.unitIntervalRepr#

A graphon on the unit interval at cut distance zero from W, for W on an arbitrary probability carrier.

The representative is an arbitrary choice; cutDist_unitIntervalRepr_left and cutDist_unitIntervalRepr_right show that no cut distance depends on it.

TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr.{u_1} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  (W : TauCeti.DenseGraphLimits.Graphon Ω μ) :
  TauCeti.DenseGraphLimits.Graphon (↑unitInterval) MeasureTheory.volume

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr
• Source of TauCeti.DenseGraphLimits.Graphon.unitIntervalRepr in TauCeti/Combinatorics/DenseGraphLimits/GraphonSpace/UnitIntervalEmbedding.lean
• Tau Ceti roadmap status: Dense graph limits and graphons

LeanTauCeti.DenseGraphLimits.Graphon.unitIntervalRepr

Uses 2 · Used by 5

Statement usesTauCeti.DenseGraphLimits.cutDist

Proof usesTauCeti.DenseGraphLimits.cutDist_triangle

Used byCut-distance convergence is convergence of all homomorphism densities · Dissociated relational laws of graphs are graphon sampling laws · Every convergent graph sequence has a limit graphon · Lovász--Szegedy compactness over atomless standard Borel carriers · The Lovász–Szegedy characterization of homomorphism densities

StructureTauCeti.Probability.ExchangeableRelationalLaw#

An exchangeable random structure of L, presented by its consistent finite marginals: a probability law on the configurations on Fin k for every k, consistent under restriction along every injection of vertices.

TauCeti.Probability.ExchangeableRelationalLaw.{u_1, u_2} (L : FirstOrder.Language) : Type u_2

Lean

Formalized in Tau Ceti as TauCeti.Probability.ExchangeableRelationalLaw.

Sources

• Tau Ceti documentation: TauCeti.Probability.ExchangeableRelationalLaw
• Source of TauCeti.Probability.ExchangeableRelationalLaw in TauCeti/Probability/Exchangeability/RelationalLaw/Basic.lean
• Tau Ceti roadmap status: Dense graph limits and graphons

LeanTauCeti.Probability.ExchangeableRelationalLaw

Used by 1

Used byDissociated relational laws of graphs are graphon sampling laws

DefinitionExchangeable laws on infinite graphs are the exchangeable relational laws of the language of graphs on ℕ concentrated on simple graphs, that is, on symmetric irreflexive configurations#

The inverse pulls the law back along the encoding.

TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.relationalLawEquiv :
  TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw ≃
    { μ //
      ∀ᵐ (c : TauCeti.RelationalConfiguration FirstOrder.Language.graph ℕ) ∂μ.law, c.IsSimpleGraph }

Lean

Formalized in Tau Ceti as TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.relationalLawEquiv.

Sources

• Tau Ceti documentation: TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.relationalLawEquiv
• Source of TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.relationalLawEquiv in TauCeti/Combinatorics/DenseGraphLimits/ExchangeableGraphLaw/Relational/Basic.lean
• Tau Ceti roadmap status: Dense graph limits and graphons

LeanTauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.relationalLawEquiv

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.