Pullbacks of Graphons

This file defines pullbacks of graphons along measure-preserving maps and proves that homomorphism densities are invariant under pullbacks.

Main definitions

• Graphon.pullback - The pullback of a graphon along a measure-preserving map
• Graphon.WeakIso - Weak isomorphism: graphons related by a measure-preserving pullback

Main results

• Graphon.pullback_ae - The pullback equals W composed with the product map, a.e.
• Graphon.homDensity_pullback - t(F, W^φ) = t(F, W) for measure-preserving φ

Implementation notes

Given a measure-preserving map φ : α → β from (α, μ) to (β, ν), the pullback W^φ : α × α → ℝ of a graphon W : β × β → ℝ is defined by W^φ(x, y) = W(φ(x), φ(y)).

The key insight is that Prod.map φ φ : α × α → β × β is measure-preserving when φ is measure-preserving (by MeasurePreserving.prod), so we can use AEEqFun.compMeasurePreserving to define the pullback.

References

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

Pullback of a symmetric kernel

theorem SymmKernel.measurePreserving_prodMap_self {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {φ : α → β} (hφ : MeasureTheory.MeasurePreserving φ μ ν) : MeasureTheory.MeasurePreserving (Prod.map φ φ) (μ.prod μ) (ν.prod ν)

The product map Prod.map φ φ is measure-preserving when φ is.

This is a specialized version of MeasurePreserving.prod for the case where both factors use the same map.

def SymmKernel.pullback {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (W : SymmKernel β ν) (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν) : SymmKernel α μ

The pullback of a symmetric kernel along a measure-preserving map.

Given a symmetric kernel W : β × β → ℝ and a measure-preserving map φ : α → β, the pullback W^φ(x, y) = W(φ(x), φ(y)) is again a symmetric kernel on α.

Equations

• W.pullback φ hφ = { toAEEqFun := W.toAEEqFun.compMeasurePreserving (Prod.map φ φ) ⋯, symm' := ⋯ }

theorem SymmKernel.pullback_toAEEqFun {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (W : SymmKernel β ν) (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν) : (W.pullback φ hφ).toAEEqFun = W.toAEEqFun.compMeasurePreserving (Prod.map φ φ) ⋯

The underlying AEEqFun of a symmetric kernel pullback.

theorem SymmKernel.pullback_ae {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (W : SymmKernel β ν) (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν) : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑(W.pullback φ hφ).toAEEqFun p = ↑W.toAEEqFun (φ p.1, φ p.2)

The pullback equals W composed with the product map, a.e.

Pullback of a graphon

def Graphon.pullback {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (W : Graphon β ν) (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν) : Graphon α μ

The pullback of a graphon along a measure-preserving map.

Given a graphon W : β × β → [0,1] and a measure-preserving map φ : α → β, the pullback W^φ(x, y) = W(φ(x), φ(y)) is again a graphon on α.

This operation is fundamental for defining the cut distance: δ□(U, W) = inf_φ ‖U - W^φ‖_□

Key property: t(F, W^φ) = t(F, W) for all graphs F (proved in homDensity_pullback).

Equations

• W.pullback φ hφ = { toSymmKernel := W.pullback φ hφ, ae_mem_Icc := ⋯ }

theorem Graphon.pullback_toAEEqFun {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (W : Graphon β ν) (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν) : (W.pullback φ hφ).toAEEqFun = W.toAEEqFun.compMeasurePreserving (Prod.map φ φ) ⋯

The underlying AEEqFun of a pullback equals the composition with the product map.

theorem Graphon.pullback_ae {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (W : Graphon β ν) (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν) : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑(W.pullback φ hφ).toAEEqFun p = ↑W.toAEEqFun (φ p.1, φ p.2)

The pullback equals W composed with the product map, a.e.

@[simp]

theorem Graphon.pullback_id {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) : W.pullback id ⋯ = W

Pullback by the identity is the original graphon.

theorem Graphon.pullback_pullback {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {γ : Type u_3} [MeasurableSpace γ] {τ : MeasureTheory.Measure γ} [MeasureTheory.IsProbabilityMeasure τ] (W : Graphon β ν) (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν) (ψ : γ → α) (hψ : MeasureTheory.MeasurePreserving ψ τ μ) : (W.pullback φ hφ).pullback ψ hψ = W.pullback (φ ∘ ψ) ⋯

Pullback is functorial: (W^φ)^ψ = W^(φ ∘ ψ).

theorem Graphon.pullback_congr_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) {f g : α → α} (hf : MeasureTheory.MeasurePreserving f μ μ) (hg : MeasureTheory.MeasurePreserving g μ μ) (h : f =ᵐ[μ] g) : W.pullback f hf = W.pullback g hg

If two measure-preserving maps agree a.e., their pullbacks are equal.

This is used to transfer cutNormDiff bounds from a general MP map to a MeasurableEquiv witness obtained via Rokhlin alignment.

Weak isomorphism

def Graphon.WeakIso {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (U : Graphon α μ) (W : Graphon β ν) : Prop

Two graphons are weakly isomorphic if one is a pullback of the other.

This is a one-sided (asymmetric) relation: WeakIso U W means U = W^φ for some measure-preserving φ. This is NOT an equivalence relation.

Important distinction:

• This definition uses any measure-preserving map φ : α → β
• The homDensity_pullback theorem requires φ to be a measurable equivalence (φ : α ≃ᵐ β) for the change of variables formula

The cut distance δ□(U, W) = 0 corresponds to the symmetric closure: there exist measure-preserving maps in BOTH directions making U and W equal via pullback.

For full weak isomorphism equivalence, one would quotient by this symmetric closure.

Equations

• U.WeakIso W = ∃ (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν), U = W.pullback φ hφ

theorem Graphon.WeakIso.refl {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) : W.WeakIso W

Reflexivity: a graphon is weakly isomorphic to itself via the identity.

theorem Graphon.WeakIso.pullback {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {U : Graphon α μ} {W : Graphon β ν} {γ : Type u_3} [MeasurableSpace γ] {τ : MeasureTheory.Measure γ} [MeasureTheory.IsProbabilityMeasure τ] (h : U.WeakIso W) (ψ : γ → α) (hψ : MeasureTheory.MeasurePreserving ψ τ μ) : (U.pullback ψ hψ).WeakIso W

Weak isomorphism is preserved under pullback.

Homomorphism density is invariant under pullback

def Graphon.piMap {α : Type u_1} {β : Type u_2} {V : Type u_3} (φ : α → β) : (V → α) → V → β

The map (V → α) → (V → β) induced by φ : α → β via post-composition.

Equations

• Graphon.piMap φ x v = φ (x v)

theorem Graphon.measurable_piMap {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {V : Type u_3} [Fintype V] [DecidableEq V] {φ : α → β} (hφ : Measurable φ) : Measurable (piMap φ)

piMap φ is measurable when φ is measurable.

theorem Graphon.measurePreserving_piMap {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {V : Type u_3} [Fintype V] [DecidableEq V] {φ : α → β} (hφ : MeasureTheory.MeasurePreserving φ μ ν) : MeasureTheory.MeasurePreserving (piMap φ) (MeasureTheory.Measure.pi fun (x : V) => μ) (MeasureTheory.Measure.pi fun (x : V) => ν)

piMap φ is measure-preserving when φ is.

def Graphon.piMapEquiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {V : Type u_3} (φ : α ≃ᵐ β) : (V → α) ≃ᵐ (V → β)

piMap φ is a measurable equivalence when φ is.

Equations

• Graphon.piMapEquiv φ = MeasurableEquiv.piCongrRight fun (x : V) => φ

theorem Graphon.homDensityIntegrand_pullback_ae {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {V : Type u_3} [Fintype V] [DecidableEq V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon β ν) (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν) : ∀ᵐ (x : V → α) ∂MeasureTheory.Measure.pi fun (x : V) => μ, homDensityIntegrand F (W.pullback φ hφ) x = homDensityIntegrand F W (piMap φ x)

The homomorphism density integrand commutes with pullback.

For any graph F, graphon W, and measure-preserving φ: homDensityIntegrand F (W^φ) x = homDensityIntegrand F W (piMap φ x) a.e.

theorem Graphon.homDensity_pullback {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {V : Type u_3} [Fintype V] [DecidableEq V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon β ν) (φ : α ≃ᵐ β) (hφ : MeasureTheory.MeasurePreserving (⇑φ) μ ν) : homDensity F (W.pullback (⇑φ) hφ) = homDensity F W

Main theorem: Homomorphism density is invariant under pullback.

For any graph F, graphon W, and measure-preserving map φ : α → β: t(F, W^φ) = t(F, W)

This is a fundamental property that makes the cut distance well-defined: weakly isomorphic graphons have the same homomorphism densities for all graphs.

theorem Graphon.homDensity_pullback_mp {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {V : Type u_3} [Fintype V] [DecidableEq V] (F : SimpleGraph V) [DecidableRel F.Adj] (W : Graphon β ν) (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν) : homDensity F (W.pullback φ hφ) = homDensity F W

General version: Homomorphism density is invariant under pullback for any measure-preserving map (not just equivalences).

For any graph F, graphon W, and measure-preserving map φ : α → β: t(F, W^φ) = t(F, W)

This uses integral_map instead of integral_comp', so it doesn't require φ to be a bijection.

theorem Graphon.homDensity_weakIso {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {V : Type u_3} [Fintype V] [DecidableEq V] (F : SimpleGraph V) [DecidableRel F.Adj] {U : Graphon α μ} {W : Graphon β ν} (φ : α ≃ᵐ β) (hφ : MeasureTheory.MeasurePreserving (⇑φ) μ ν) (h : U = W.pullback (⇑φ) hφ) : homDensity F U = homDensity F W

Weakly isomorphic graphons have the same homomorphism densities.