Homomorphism Densities

This file defines homomorphism densities for graphons, which measure how frequently a fixed graph pattern appears in a graphon.

Main definitions

• Graphon.homDensity - The homomorphism density t(F, W) of a graph F in a graphon W

Main results

• Graphon.homDensity_nonneg - Homomorphism density is nonnegative
• Graphon.homDensity_le_one - Homomorphism density is at most 1

Implementation notes

The homomorphism density t(F, W) for a graph F on vertex set V and graphon W is defined as the integral over all maps x : V → [0,1] of the product of W(x(u), x(v)) over all edges {u, v} of F.

Technical note on a.e. bounds

The integrand bounds (nonneg, ≤ 1, integrability) require lifting the graphon's a.e. bound from μ × μ to Measure.pi (fun _ => μ). The key fact is that for probability measures with independent coordinates, the pair projection x ↦ (x v₁, x v₂) maps Measure.pi to μ × μ when v₁ ≠ v₂. This is implicit in measurePreserving_piFinTwo and related results.

References

• [L. Lovász, Large Networks and Graph Limits][lovasz2012], Section 7.1

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

The homomorphism density t(F, W) of a simple graph F in a graphon W.

This measures the probability that a random map from the vertices of F to the probability space preserves adjacency (in expectation). Formally:

t(F, W) = ∫_{x : V → α} ∏_{e ∈ E(F)} W(x(u_e), x(v_e)) dμ^V

The product uses Quot.out to extract a canonical representative pair from each edge in edgeFinset. Since W is symmetric a.e. and the integral marginalizes over all vertex mappings, the choice of representative does not affect the result.

For a finite graph G on n vertices, t(F, W_G) = hom(F, G) / n^|V(F)| where hom(F, G) is the number of graph homomorphisms from F to G.

Equations

• Graphon.homDensity F W = ∫ (x : V → α), ∏ e ∈ F.edgeFinset, ↑W.toAEEqFun (x (Quot.out e).1, x (Quot.out e).2) ∂MeasureTheory.Measure.pi fun (x : V) => μ

noncomputable def Graphon.homDensityIntegrand {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon α μ) (x : V → α) : ℝ

The integrand in the homomorphism density formula.

Equations

• Graphon.homDensityIntegrand F W x = ∏ e ∈ F.edgeFinset, ↑W.toAEEqFun (x (Quot.out e).1, x (Quot.out e).2)

theorem Graphon.homDensity_eq_integral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] [DecidableEq V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon α μ) : homDensity F W = ∫ (x : V → α), homDensityIntegrand F W x ∂MeasureTheory.Measure.pi fun (x : V) => μ

theorem Graphon.homDensity_congr_decRel {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] [DecidableEq V] (F : SimpleGraph V) (inst₁ inst₂ : DecidableRel F.Adj) (W : Graphon α μ) : homDensity F W = homDensity F W

homDensity is independent of the DecidableRel instance used.

Since edgeFinset is determined by edgeSet (a propositional Set), different DecidableRel instances for the same adjacency relation yield the same homDensity.

theorem Graphon.homDensity_bot {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] [DecidableEq V] (W : Graphon α μ) : homDensity ⊥ W = 1

The homomorphism density of the empty graph is 1.

An empty graph has no edges, so the integrand is a product over an empty set, which equals 1. The integral of 1 over a probability space is 1.

theorem Graphon.edge_out_ne {V : Type u_2} [Fintype V] [DecidableEq V] {F : SimpleGraph V} [DecidableRel F.Adj] {e : Sym2 V} (he : e ∈ F.edgeSet) : (Quot.out e).1 ≠ (Quot.out e).2

Helper: for edges in simple graphs, the two vertices are distinct.

theorem Graphon.graphonEval_mem_Icc_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] [DecidableEq V] (W : Graphon α μ) {v₁ v₂ : V} (hne : v₁ ≠ v₂) : ∀ᵐ (x : V → α) ∂MeasureTheory.Measure.pi fun (x : V) => μ, ↑W.toAEEqFun (x v₁, x v₂) ∈ Set.Icc 0 1

For probability measures, the graphon value at a pair projection is in [0,1] a.e.

This key technical lemma shows that for distinct indices v₁ ≠ v₂ : V, the composition x ↦ W(x v₁, x v₂) takes values in [0,1] for a.e. x : V → α under Measure.pi.

The proof uses that for distinct coordinates, eval v₁ and eval v₂ are independent under Measure.pi. By measurePreserving_eval, the marginal distributions equal μ, and by independence, the pair (x v₁, x v₂) has distribution μ × μ. Since the graphon's a.e. bound holds on μ × μ, it lifts to Measure.pi.

theorem Graphon.homDensityIntegrand_nonneg_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] [DecidableEq V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon α μ) : 0 ≤ᵐ[MeasureTheory.Measure.pi fun (x : V) => μ] fun (x : V → α) => homDensityIntegrand F W x

The integrand in the homomorphism density is nonnegative a.e.

This follows because each factor W(x(u), x(v)) is nonnegative a.e. (W takes values in [0,1] a.e.) and a product of nonnegative terms is nonnegative.

theorem Graphon.homDensityIntegrand_le_one_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] [DecidableEq V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon α μ) : (fun (x : V → α) => homDensityIntegrand F W x) ≤ᵐ[MeasureTheory.Measure.pi fun (x : V) => μ] fun (x : V → α) => 1

The integrand in the homomorphism density is at most 1 a.e.

This follows because each factor W(x(u), x(v)) is at most 1 a.e. (W takes values in [0,1] a.e.) and a product of terms in [0,1] is in [0,1].

theorem Graphon.homDensityIntegrand_mem_Icc_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] [DecidableEq V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon α μ) : ∀ᵐ (x : V → α) ∂MeasureTheory.Measure.pi fun (x : V) => μ, homDensityIntegrand F W x ∈ Set.Icc 0 1

The homomorphism density integrand takes values in [0, 1] a.e.

This combines the nonnegativity and upper bound.

theorem Graphon.homDensityIntegrand_aemeasurable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] [DecidableEq V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon α μ) : AEMeasurable (homDensityIntegrand F W) (MeasureTheory.Measure.pi fun (x : V) => μ)

The homomorphism density integrand is ae-measurable.

Technical note: The proof requires showing that the composition x ↦ W(x v₁, x v₂) is ae-measurable on Measure.pi. The graphon is ae-strongly-measurable on μ × μ, and we need to lift this to the pushforward measure Measure.map (x ↦ (x v₁, x v₂)) (Measure.pi _). For probability measures with independent coordinates, this pushforward equals μ × μ when v₁ ≠ v₂ (which holds for simple graph edges).

theorem Graphon.homDensityIntegrand_integrable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] [DecidableEq V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon α μ) : MeasureTheory.Integrable (homDensityIntegrand F W) (MeasureTheory.Measure.pi fun (x : V) => μ)

The homomorphism density integrand is integrable over the product measure.

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

Homomorphism density is nonnegative.

This is the integral of an a.e. nonnegative function over a measure space.

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

Homomorphism density is at most 1.

This follows because the integrand is bounded by 1 a.e. and we integrate over a probability space (so the integral of the constant 1 is 1).

theorem Graphon.homDensity_mem_Icc {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] [DecidableEq V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon α μ) : homDensity F W ∈ Set.Icc 0 1

Homomorphism density is in [0, 1].

theorem Graphon.homDensity_map_embedding {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] [DecidableEq V] {W' : Type u_3} [Fintype W'] [DecidableEq W'] (F : SimpleGraph V) [DecidableRel F.Adj] (f : V ↪ W') (G : Graphon α μ) : homDensity (SimpleGraph.map f F) G = homDensity F G

Mapping a graph along an embedding preserves homomorphism density.

If σ : V ↪ W' is an embedding and F : SimpleGraph V, then homDensity (F.map σ) G = homDensity F G for any graphon G.

Proof sketch: The integrand of homDensity (F.map σ) G is ∏_{e' ∈ (F.map σ).edgeFinset} G(y(e'.1), y(e'.2)). Since (F.map σ).edgeFinset = F.edgeFinset.map σ.sym2Map, this equals ∏_{e ∈ F.edgeFinset} G(y(σ(e.1)), y(σ(e.2))). The integrand depends on y : W' → α only through y ∘ σ : V → α. By splitting the product measure μ^W' via piEquivPiSubtypeProd into μ^(range σ) × μ^(range σ)ᶜ and using that the integrand is independent of the complement coordinates, the integral over the complement gives μ(univ)^|W' \ range σ| = 1 (since μ is a probability measure), leaving ∫_{x : V → α} ∏_{e ∈ F.edgeFinset} G(x(e.1), x(e.2)) dμ^V = homDensity F G.

The proof uses map_precomp_pi_eq: the pushforward of μ^W' under (· ∘ f) equals μ^V.