Graphons

A graphon is (informally) a symmetric measurable function W : [0,1]² → [0,1] that represents the limit of a convergent sequence of dense graphs. More precisely, graphons are equivalence classes of such functions under almost-everywhere equality.

This file introduces graphons parameterized by a probability space (α, μ), using AEEqFun (almost-everywhere equivalence classes of functions) to represent kernels. Two kernels that agree almost everywhere are considered equal.

Main definitions

• SymmKernel - A symmetric kernel: element of L⁰(α × α, ℝ) symmetric a.e. (general measure, used as base type)
• Graphon - A graphon over a probability space: symmetric kernel with values in [0,1] a.e.
• SignedGraphon - Signed graphon: |W| ≤ 1 a.e. For cut distance calculations.
• GraphonI - Canonical graphon type on the unit interval with Lebesgue measure

Design notes

We parameterize Graphon and SignedGraphon by a probability space (α, μ) with [IsProbabilityMeasure μ], following Lovász's normalization convention. The canonical type GraphonI uses the unit interval with Lebesgue measure. The base type SymmKernel is defined for general measures to allow reuse in other contexts.

We use AEEqFun to represent kernels as elements of L⁰, which gives us automatic quotienting by a.e. equality. We use ℝ as the codomain (rather than Set.Icc 0 1) to enable subtraction for cut distance calculations.

The IsProbabilityMeasure assumption ensures:

• The product measure μ.prod μ is also a probability measure
• Swap is measure-preserving (μ.prod μ is symmetric)
• Integrals are normalized (important for homomorphism densities)

References

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

Helper lemmas for product measure symmetry

theorem ae_prod_swap {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] {P : α × α → Prop} (hP : ∀ᵐ (p : α × α) ∂μ.prod μ, P p) : ∀ᵐ (p : α × α) ∂μ.prod μ, P p.swap

If a property holds a.e. for the product measure μ × μ, then it also holds a.e. when composed with swap.

This requires [SFinite μ] to ensure that swap is measure-preserving on the product measure (i.e., (μ.prod μ).map swap = μ.prod μ).

structure SymmKernel (α : Type u_2) [MeasurableSpace α] (μ : MeasureTheory.Measure α) : Type u_2

A symmetric kernel: an element of L⁰(α × α, ℝ) that is symmetric a.e.

This is the base type for both graphons (values in [0,1]) and signed kernels (values in [-1,1]). The symmetry condition W(x,y) = W(y,x) holds almost everywhere with respect to the product measure.

Note: This type is defined for general measures. For the swap-invariance of a.e. properties to hold, the measure should be SFinite. The subtypes Graphon and SignedGraphon are intended for use with probability measures.

• toAEEqFun : α × α →ₘ[μ.prod μ] ℝ

  The underlying almost-everywhere equal function class

• symm' : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑self.toAEEqFun p.swap = ↑self.toAEEqFun p

  The function is symmetric a.e.: W(x,y) = W(y,x) for a.e. (x,y)

structure Graphon (α : Type u_2) [MeasurableSpace α] (μ : MeasureTheory.Measure α) extends SymmKernel α μ : Type u_2

A graphon: a symmetric kernel with values in [0,1] almost everywhere.

This represents the limit object for sequences of dense graphs. The domain is a probability space (α, μ). Operations on graphons require [IsProbabilityMeasure μ] to ensure proper normalization and measure-theoretic properties.

The IsProbabilityMeasure constraint ensures:

• μ.prod μ is a probability measure on the product space
• Swap is measure-preserving (needed for symmetry properties)
• Integrals give meaningful densities

• toAEEqFun : α × α →ₘ[μ.prod μ] ℝ
• symm' : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑self.toAEEqFun p.swap = ↑self.toAEEqFun p
• ae_mem_Icc : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑self.toAEEqFun p ∈ Set.Icc 0 1

  Values lie in [0,1] a.e.

structure SignedGraphon (α : Type u_2) [MeasurableSpace α] (μ : MeasureTheory.Measure α) extends SymmKernel α μ : Type u_2

A signed graphon: a symmetric kernel with |W| ≤ 1 almost everywhere.

Used for cut distance calculations, where we need to consider differences of graphons. The bound |W| ≤ 1 is preserved under taking differences of graphons.

Like Graphon, operations require [IsProbabilityMeasure μ].

• toAEEqFun : α × α →ₘ[μ.prod μ] ℝ
• symm' : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑self.toAEEqFun p.swap = ↑self.toAEEqFun p
• ae_abs_le_one : ∀ᵐ (p : α × α) ∂μ.prod μ, |↑self.toAEEqFun p| ≤ 1

  Absolute value bounded by 1 a.e.

Canonical graphon type

@[reducible, inline]

abbrev GraphonI : Type

The canonical graphon type on the unit interval with Lebesgue measure.

This is the standard space for graphons in the literature. We use I (= Set.Icc 0 1) as the underlying type, which carries the subtype measure from Lebesgue measure on ℝ.

Equations

• GraphonI = Graphon (↑unitInterval) MeasureTheory.volume

Coercions and instances for SymmKernel

We provide coercions so that a SymmKernel can be used directly as an AEEqFun. The extensionality lemma shows that two symmetric kernels are equal iff their underlying AEEqFun representatives are equal (which is itself equality up to a.e. equivalence).

instance SymmKernel.instCoeFunAEEqFunProdRealProd {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} : CoeFun (SymmKernel α μ) fun (x : SymmKernel α μ) => α × α →ₘ[μ.prod μ] ℝ

A symmetric kernel can be used as its underlying AEEqFun.

Equations

• SymmKernel.instCoeFunAEEqFunProdRealProd = { coe := SymmKernel.toAEEqFun }

theorem SymmKernel.ext {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {W₁ W₂ : SymmKernel α μ} (h : W₁.toAEEqFun = W₂.toAEEqFun) : W₁ = W₂

Symmetric kernels are equal iff their underlying AEEqFun are equal.

Since AEEqFun equality is defined as a.e. equality of representatives, this means two symmetric kernels are equal iff they agree almost everywhere.

theorem SymmKernel.ext_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {W₁ W₂ : SymmKernel α μ} : W₁ = W₂ ↔ W₁.toAEEqFun = W₂.toAEEqFun

theorem SymmKernel.symm_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : SymmKernel α μ) : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑W.toAEEqFun p.swap = ↑W.toAEEqFun p

The symmetry property: W(x,y) = W(y,x) for almost every (x,y).

This is the defining property of symmetric kernels, ensuring the kernel represents an undirected relationship.

Coercions and instances for Graphon

We provide coercions so that a Graphon can be used as a SymmKernel or AEEqFun. The key properties are:

• ae_nonneg: values are non-negative a.e.
• ae_le_one: values are at most 1 a.e.
• symm_ae: the graphon is symmetric a.e.

Together these ensure the graphon represents a valid edge-weight function for the limit of dense graphs.

instance Graphon.instCoeFunAEEqFunProdRealProd {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} : CoeFun (Graphon α μ) fun (x : Graphon α μ) => α × α →ₘ[μ.prod μ] ℝ

A graphon can be used as its underlying AEEqFun.

Equations

• Graphon.instCoeFunAEEqFunProdRealProd = { coe := fun (W : Graphon α μ) => W.toAEEqFun }

instance Graphon.instCoeSymmKernel {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} : Coe (Graphon α μ) (SymmKernel α μ)

A graphon can be viewed as its underlying symmetric kernel.

This forgets the [0,1] bound but retains the symmetry property.

Equations

• Graphon.instCoeSymmKernel = { coe := Graphon.toSymmKernel }

theorem Graphon.ext {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {W₁ W₂ : Graphon α μ} (h : W₁.toSymmKernel = W₂.toSymmKernel) : W₁ = W₂

Graphons are equal iff their underlying symmetric kernels are equal.

Since SymmKernel equality reduces to AEEqFun equality (a.e. equality), two graphons are equal iff they agree almost everywhere.

theorem Graphon.ext_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {W₁ W₂ : Graphon α μ} : W₁ = W₂ ↔ W₁.toSymmKernel = W₂.toSymmKernel

theorem Graphon.ae_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) : ∀ᵐ (p : α × α) ∂μ.prod μ, 0 ≤ ↑W.toAEEqFun p

Graphon values are non-negative almost everywhere.

This is half of the [0,1] bound; combined with ae_le_one, it ensures the graphon represents valid edge probabilities.

theorem Graphon.ae_le_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑W.toAEEqFun p ≤ 1

Graphon values are at most 1 almost everywhere.

This is half of the [0,1] bound; combined with ae_nonneg, it ensures the graphon represents valid edge probabilities.

theorem Graphon.symm_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑W.toAEEqFun p.swap = ↑W.toAEEqFun p

The symmetry property for graphons: W(x,y) = W(y,x) for almost every (x,y).

This ensures the graphon represents an undirected graph limit.

Constant graphons

The constant graphons zero and one represent the limits of sequences of empty graphs and complete graphs, respectively. For a sequence of empty graphs Gₙ on n vertices, the graphon limit is the constant function W ≡ 0. Similarly, complete graphs converge to W ≡ 1.

These require [IsProbabilityMeasure μ] to ensure the product measure is symmetric under swap.

def Graphon.zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] : Graphon α μ

The constant zero graphon, representing the limit of empty graphs.

For a sequence of empty graphs Gₙ (graphs with no edges), the edge density between any two sets converges to 0, giving the graphon W(x,y) = 0 for all x,y.

Equations

• Graphon.zero = { toAEEqFun := MeasureTheory.AEEqFun.const (α × α) 0, symm' := ⋯, ae_mem_Icc := ⋯ }

def Graphon.one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] : Graphon α μ

The constant one graphon, representing the limit of complete graphs.

For a sequence of complete graphs Kₙ, the edge density between any two sets converges to 1, giving the graphon W(x,y) = 1 for all x,y.

Equations

• Graphon.one = { toAEEqFun := MeasureTheory.AEEqFun.const (α × α) 1, symm' := ⋯, ae_mem_Icc := ⋯ }

theorem Graphon.zero_toAEEqFun {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] : zero.toAEEqFun = MeasureTheory.AEEqFun.const (α × α) 0

The underlying AEEqFun of the zero graphon is the constant 0 function.

theorem Graphon.one_toAEEqFun {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] : one.toAEEqFun = MeasureTheory.AEEqFun.const (α × α) 1

The underlying AEEqFun of the one graphon is the constant 1 function.

Complement

The complement operation compl W = 1 - W corresponds to taking graph complements. If W is the graphon limit of a sequence of graphs Gₙ, then compl W is the graphon limit of the complement graphs Ḡₙ.

Key properties:

• compl_compl: complement is an involution
• compl_zero: the complement of the empty graph limit is the complete graph limit
• compl_one: the complement of the complete graph limit is the empty graph limit

def Graphon.compl {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) : Graphon α μ

The complement of a graphon: (1 - W).

If W is the graphon limit of graphs Gₙ, then compl W is the limit of the complement graphs Ḡₙ. The edge probability W(x,y) becomes the non-edge probability 1 - W(x,y).

Equations

• W.compl = { toAEEqFun := MeasureTheory.AEEqFun.const (α × α) 1 - W.toAEEqFun, symm' := ⋯, ae_mem_Icc := ⋯ }

@[simp]

theorem Graphon.compl_compl {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) : W.compl.compl = W

Complement is an involution: (1 - (1 - W)) = W.

This reflects the graph-theoretic fact that the complement of the complement of a graph is the original graph.

@[simp]

theorem Graphon.compl_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] : zero.compl = one

The complement of the zero graphon is the one graphon: 1 - 0 = 1.

Graph-theoretically: the complement of the empty graph is the complete graph.

@[simp]

theorem Graphon.compl_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] : one.compl = zero

The complement of the one graphon is the zero graphon: 1 - 1 = 0.

Graph-theoretically: the complement of the complete graph is the empty graph.

Coercions and instances for SignedGraphon

Signed graphons arise naturally when computing cut distances, which involve differences of graphons. The key property is that if W₁, W₂ : Graphon α μ with values in [0,1], then W₁ - W₂ has values in [-1,1], so |W₁ - W₂| ≤ 1 almost everywhere.

The sub operation constructs the difference of two graphons as a signed graphon, which is essential for defining the cut norm and cut distance.

instance SignedGraphon.instCoeFunAEEqFunProdRealProd {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} : CoeFun (SignedGraphon α μ) fun (x : SignedGraphon α μ) => α × α →ₘ[μ.prod μ] ℝ

A signed graphon can be used as its underlying AEEqFun.

Equations

• SignedGraphon.instCoeFunAEEqFunProdRealProd = { coe := fun (W : SignedGraphon α μ) => W.toAEEqFun }

instance SignedGraphon.instCoeSymmKernel {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} : Coe (SignedGraphon α μ) (SymmKernel α μ)

A signed graphon can be viewed as its underlying symmetric kernel.

This forgets the |W| ≤ 1 bound but retains the symmetry property.

Equations

• SignedGraphon.instCoeSymmKernel = { coe := SignedGraphon.toSymmKernel }

theorem SignedGraphon.ext {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {W₁ W₂ : SignedGraphon α μ} (h : W₁.toSymmKernel = W₂.toSymmKernel) : W₁ = W₂

Signed graphons are equal iff their underlying symmetric kernels are equal.

Since SymmKernel equality reduces to AEEqFun equality (a.e. equality), two signed graphons are equal iff they agree almost everywhere.

theorem SignedGraphon.ext_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {W₁ W₂ : SignedGraphon α μ} : W₁ = W₂ ↔ W₁.toSymmKernel = W₂.toSymmKernel

def SignedGraphon.ofGraphon {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) : SignedGraphon α μ

Embed a graphon as a signed graphon.

Since graphon values lie in [0,1] a.e., we have |W| ≤ 1 a.e., so every graphon is trivially a signed graphon. This embedding is useful when we want to use graphons in contexts that expect signed graphons (e.g., cut norm).

Equations

• SignedGraphon.ofGraphon W = { toSymmKernel := W.toSymmKernel, ae_abs_le_one := ⋯ }

def SignedGraphon.sub {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W₁ W₂ : Graphon α μ) : SignedGraphon α μ

The difference of two graphons as a signed graphon.

If W₁(x,y) ∈ [0,1] and W₂(x,y) ∈ [0,1] a.e., then (W₁ - W₂)(x,y) ∈ [-1,1] a.e., so |W₁ - W₂| ≤ 1.

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

Equations

• SignedGraphon.sub W₁ W₂ = { toAEEqFun := W₁.toAEEqFun - W₂.toAEEqFun, symm' := ⋯, ae_abs_le_one := ⋯ }