Homomorphism densities of a graphon

The homomorphism density t(F, W) of a finite graph F in a graphon W: integrate, over all maps x : V(F) → Ω, the product of W along the edges of F.

t(F, W) = ∫ ∏_{e ∈ E(F)} W (x eᵢ) (x eⱼ) dμ^{V(F)}

Edges are Sym2, and no orientation is chosen. An edge of a SimpleGraph is a Sym2 element, with no distinguished endpoint. Rather than pick a representative, edgeFactor is built with Sym2.lift from the symmetric function fun a b => W (x a) (x b) — symmetric exactly because a graphon is. Choosing an orientation would work numerically but would leave every later proof carrying a well-definedness obligation that the Sym2.lift formulation discharges once.

The empty cases are not special-cased. The empty product is 1, and the probability-measure instance for Measure.pi makes its integral 1, including when the vertex type is empty. Nothing here needs a nonempty-carrier hypothesis.

Main definitions

• TauCeti.DenseGraphLimits.edgeFactor — the value of W on one edge, orientation-free;
• TauCeti.DenseGraphLimits.homDensity — the density t(F, W).

Main results

• edgeFactor_congr — an edge factor depends only on the assignment along that edge;
• edgeFactor_map — an edge factor is read along a map of vertex sets by pulling the assignment back;
• measurable_prod_edgeFactor, prod_edgeFactor_nonneg, prod_edgeFactor_le_one and integrable_prod_edgeFactor — the basic analytic facts about a finite product of edge factors, each edge read in its own graphon. The integrand of homDensity is the special case of one graphon on the edges of F, and the telescoping proof of the counting lemma needs the general form;
• homDensity_nonneg, homDensity_le_one — t(F, W) ∈ [0, 1], with no hypotheses;
• homDensity_const — the Erdős–Rényi value t(F, W_p) = p ^ e(F), the first real consumer of both the graphon carrier and this definition.

References

• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 1 — homDensity and the constant-graphon value. The counting lemmas, cutNorm, finite-graph compatibility with homDensityFin, disjoint-union multiplicativity, and the catalogue of small-graph integrals are separate targets and are not built here.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §7.2.

def TauCeti.DenseGraphLimits.edgeFactor {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} (W : Graphon Ω μ) (x : V → Ω) (e : Sym2 V) : ℝ

The value of a graphon on a single edge, as a function of the vertex assignment.

Built with Sym2.lift from fun a b => W (x a) (x b), which is symmetric because W is, so no orientation of the edge is chosen.

Equations

• TauCeti.DenseGraphLimits.edgeFactor W x e = Sym2.lift ⟨fun (a b : V) => W (x a) (x b), ⋯⟩ e

@[simp]

theorem TauCeti.DenseGraphLimits.edgeFactor_mk {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} (W : Graphon Ω μ) (x : V → Ω) (a b : V) : edgeFactor W x s(a, b) = W (x a) (x b)

theorem TauCeti.DenseGraphLimits.edgeFactor_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} (W : Graphon Ω μ) (x : V → Ω) (e : Sym2 V) : 0 ≤ edgeFactor W x e

Each edge factor is nonnegative, since a graphon is.

theorem TauCeti.DenseGraphLimits.edgeFactor_le_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} (W : Graphon Ω μ) (x : V → Ω) (e : Sym2 V) : edgeFactor W x e ≤ 1

Each edge factor is at most 1, since a graphon is.

theorem TauCeti.DenseGraphLimits.measurable_edgeFactor {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} (W : Graphon Ω μ) (e : Sym2 V) : Measurable fun (x : V → Ω) => edgeFactor W x e

Each edge factor depends measurably on the vertex assignment.

theorem TauCeti.DenseGraphLimits.edgeFactor_congr {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} (W : Graphon Ω μ) {x y : V → Ω} {e : Sym2 V} (h : ∀ v ∈ e, x v = y v) : edgeFactor W x e = edgeFactor W y e

The value of a graphon on an edge depends only on the vertex assignment along that edge. This is what lets an edge factor be read off after the assignment has been altered away from the edge.

@[simp]

theorem TauCeti.DenseGraphLimits.edgeFactor_map {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} {V' : Type u_3} (W : Graphon Ω μ) (f : V → V') (x : V' → Ω) (e : Sym2 V) : edgeFactor W x (Sym2.map f e) = edgeFactor W (x ∘ f) e

Reading an edge after pushing it forward along a map of vertex sets is reading the original edge in the pulled-back assignment.

theorem TauCeti.DenseGraphLimits.measurable_prod_edgeFactor {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} (E : Finset (Sym2 V)) (G : Sym2 V → Graphon Ω μ) : Measurable fun (x : V → Ω) => ∏ e ∈ E, edgeFactor (G e) x e

A finite product of edge factors, each edge read in its own graphon, depends measurably on the vertex assignment.

theorem TauCeti.DenseGraphLimits.prod_edgeFactor_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} (E : Finset (Sym2 V)) (G : Sym2 V → Graphon Ω μ) (x : V → Ω) : 0 ≤ ∏ e ∈ E, edgeFactor (G e) x e

A finite product of edge factors is nonnegative.

theorem TauCeti.DenseGraphLimits.prod_edgeFactor_le_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} (E : Finset (Sym2 V)) (G : Sym2 V → Graphon Ω μ) (x : V → Ω) : ∏ e ∈ E, edgeFactor (G e) x e ≤ 1

A finite product of edge factors is at most 1: every factor lies in [0, 1].

theorem TauCeti.DenseGraphLimits.integrable_prod_edgeFactor {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (E : Finset (Sym2 V)) (G : Sym2 V → Graphon Ω μ) : MeasureTheory.Integrable (fun (x : V → Ω) => ∏ e ∈ E, edgeFactor (G e) x e) (MeasureTheory.Measure.pi fun (x : V) => μ)

A finite product of edge factors is integrable against the product measure: it is measurable and [0, 1]-valued on a probability space.

noncomputable def TauCeti.DenseGraphLimits.homDensity {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon Ω μ) : ℝ

The homomorphism density t(F, W): the integral, over vertex assignments, of the product of W along the edges of F.

Outside this module, use homDensity_def to unfold homDensity; its definition is intentionally not exposed across module boundaries.

Equations

• TauCeti.DenseGraphLimits.homDensity F W = ∫ (x : V → Ω), ∏ e ∈ F.edgeFinset, TauCeti.DenseGraphLimits.edgeFactor W x e ∂MeasureTheory.Measure.pi fun (x : V) => μ

theorem TauCeti.DenseGraphLimits.homDensity_def {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon Ω μ) : homDensity F W = ∫ (x : V → Ω), ∏ e ∈ F.edgeFinset, edgeFactor W x e ∂MeasureTheory.Measure.pi fun (x : V) => μ

The defining integral of homDensity.

Outside this module, use this to unfold homDensity; its definition is intentionally not exposed across module boundaries, so rfl will not do it.

theorem TauCeti.DenseGraphLimits.homDensity_integrand_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon Ω μ) (x : V → Ω) : 0 ≤ ∏ e ∈ F.edgeFinset, edgeFactor W x e

The integrand of homDensity is nonnegative.

theorem TauCeti.DenseGraphLimits.homDensity_integrand_le_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon Ω μ) (x : V → Ω) : ∏ e ∈ F.edgeFinset, edgeFactor W x e ≤ 1

The integrand of homDensity is at most 1: it is a product of factors in [0, 1].

theorem TauCeti.DenseGraphLimits.integrable_homDensity_integrand {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon Ω μ) : MeasureTheory.Integrable (fun (x : V → Ω) => ∏ e ∈ F.edgeFinset, edgeFactor W x e) (MeasureTheory.Measure.pi fun (x : V) => μ)

The integrand of homDensity is integrable: it is measurable and bounded on a probability space.

theorem TauCeti.DenseGraphLimits.homDensity_nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon Ω μ) : 0 ≤ homDensity F W

A homomorphism density is nonnegative.

theorem TauCeti.DenseGraphLimits.homDensity_le_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon Ω μ) : homDensity F W ≤ 1

A homomorphism density is at most 1.

@[simp]

theorem TauCeti.DenseGraphLimits.homDensity_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (p : ↑unitInterval) : homDensity F (Graphon.const μ p) = ↑p ^ F.edgeFinset.card

The Erdős–Rényi value. The constant graphon with parameter p has t(F, W_p) = p ^ e(F).