The almost-everywhere view of a graphon

A graphon is carried as a strict function W : Ω → Ω → ℝ, symmetric and [0, 1]-valued at every point. This file is the single place where the almost-everywhere picture enters: it sends a graphon to its class Graphon.toAEEqFun W : (Ω × Ω) →ₘ[μ ⊗ μ] ℝ in Mathlib's AEEqFun, proves that the three observables — homomorphism densities, the cut norm, and the cut distance — do not see the difference between two representatives of one class, and exhibits the reverse passage: an a.e. [0, 1]-valued, a.e. symmetric class is the class of a strict graphon.

The strict and almost-everywhere views. Carrying the strict function is what makes U - W a literal kernel and ∀ x y, W x y ∈ Set.Icc 0 1 a stateable hypothesis, so the cut norm and the counting lemma never carry a null-set side condition. The price is that representatives are not unique, and analytic arguments that produce a function only up to a null set — conditional expectations and martingale limits — are naturally AEEqFun-native. The theorems below pay that price once: homDensity_congr_ae, cutNorm_congr_ae and cutDist_eq_zero_of_aeEq say the strict representative may be chosen freely, and exists_graphon_repr says such a choice always exists.

The round trip is lossy in exactly one direction. Graphon.toAEEqFun forgets the values of W on a null set, so it is not injective; exists_graphon_repr inverts it only up to that forgetting. What is not lost is the pair of pointwise constraints: the class of a graphon is a.e. [0, 1] -valued and a.e. symmetric (Graphon.toAEEqFun_mem_Icc_ae, Graphon.toAEEqFun_symm_ae), and those two conditions are exactly what a class needs in order to come from a graphon (exists_graphon_repr_iff). Symmetrising and clamping a measurable representative is what converts "a.e." back into "everywhere".

Main definitions

• TauCeti.DenseGraphLimits.Graphon.toAEEqFun — the a.e. class of a graphon on μ ⊗ μ.

Main results

• Graphon.toAEEqFun_eq_iff — two graphons have the same class exactly when they agree a.e.;
• Graphon.ae_eq_const_of_dirac — a graphon on a point mass agrees a.e. with its value there;
• Graphon.toAEEqFun_mem_Icc_ae, Graphon.toAEEqFun_symm_ae — the class of a graphon is a.e. [0, 1]-valued and a.e. symmetric;
• Graphon.toAEEqFun_comap — the class of a measure-preserving pullback is the composition of the class with the pullback, Mathlib's AEEqFun.compMeasurePreserving;
• cutNorm_congr_ae and SymmKernel.rectIntegral_congr_ae — the cut norm, and already each rectangle integral, factor through the a.e. class of a kernel;
• homDensity_congr_ae — homomorphism densities factor through the a.e. class of a graphon;
• cutNorm_overlayDiff_congr_ae_left, cutDist_congr_ae_left and cutDist_congr_ae_right — the cut distance itself, not merely its vanishing, factors through the a.e. classes of its two arguments, on arbitrary carriers;
• cutDist_eq_zero_of_aeEq — a.e. equal graphons are at cut distance zero;
• exists_graphon_repr and exists_graphon_repr_iff — an a.e. [0, 1]-valued, a.e. symmetric class is the class of a strict graphon, and only such a class is.

Implementation

The rectangle integrals of two a.e. equal kernels agree because a.e. equality passes to the restriction of μ ⊗ μ to a rectangle, and the cut norm is a supremum of their absolute values. For the cut distance the a.e. hypothesis lives on μ₁ ⊗ μ₁ while the overlaid difference lives on π ⊗ π for a coupling π; the first-coordinate projection relates them, and is measure preserving exactly because π has left marginal μ₁. Every coupling therefore contributes the same value to the two infima, which gives the invariance of δ□ with no triangle inequality; vanishing on a.e. equal graphons is then the case U' = W of that invariance together with cutDist_self.

For homomorphism densities the a.e. hypothesis lives on μ ⊗ μ while the integral is over Measure.pi, so it has to be transported along the evaluation map x ↦ (x a, x b) at the two endpoints of an edge. That map is measure preserving precisely because the endpoints of an edge of a SimpleGraph are distinct (TauCeti.measurePreserving_eval_pair); the finitely many edges are then intersected with Filter.eventually_all_finset.

The strict representative built by exists_graphon_repr is fun x y => max 0 (min 1 ((f (x, y) + f (y, x)) / 2)): the average symmetrises everywhere, not just a.e., and the clamping puts the values in [0, 1] everywhere. Both operations are the identity a.e., which is what makes the result represent the class it started from — and both are needed, since a class has no reason to have a representative with either property on the nose.

References

• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), §6 — graphons up to a.e. equality.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §7.

theorem TauCeti.DenseGraphLimits.Graphon.ae_eq_const_of_dirac {Ω : Type u_1} [MeasurableSpace Ω] {b : Ω} (W : Graphon Ω (MeasureTheory.Measure.dirac b)) : ∀ᵐ (x : Ω × Ω) ∂(MeasureTheory.Measure.dirac b).prod (MeasureTheory.Measure.dirac b), W x.1 x.2 = (const (MeasureTheory.Measure.dirac b) ⟨W b b, ⋯⟩) x.1 x.2

A graphon on a point mass is almost everywhere constant: on (Ω, δ_b) it agrees δ_b ⊗ δ_b-almost everywhere with the constant graphon at its value W b b.

No measurable-singleton hypothesis is needed: the set where W takes the value W b b is measurable because W is.

theorem TauCeti.DenseGraphLimits.SymmKernel.rectIntegral_congr_ae {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {K L : SymmKernel Ω μ} (h : ∀ᵐ (p : Ω × Ω) ∂μ.prod μ, K p.1 p.2 = L p.1 p.2) (S T : Set Ω) : rectIntegral μ K S T = rectIntegral μ L S T

A rectangle integral only sees the a.e. class of the kernel. Almost everywhere equality on μ ⊗ μ restricts to any rectangle, so the two integrands agree there.

theorem TauCeti.DenseGraphLimits.cutNorm_congr_ae {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {K L : SymmKernel Ω μ} (h : ∀ᵐ (p : Ω × Ω) ∂μ.prod μ, K p.1 p.2 = L p.1 p.2) : cutNorm μ K = cutNorm μ L

The cut norm factors through the a.e. class of a kernel. Two kernels agreeing off a μ ⊗ μ-null set have the same cut norm: they have the same rectangle integrals, and the cut norm is the supremum of their absolute values.

noncomputable def TauCeti.DenseGraphLimits.Graphon.toAEEqFun {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : Ω × Ω →ₘ[μ.prod μ] ℝ

The a.e. class of a graphon, an element of Mathlib's AEEqFun on the product carrier μ ⊗ μ.

This is the one place the strict carrier is traded for an a.e. class. Outside this module use Graphon.coeFn_toAEEqFun and Graphon.toAEEqFun_eq_iff rather than unfolding the definition.

Equations

• W.toAEEqFun = MeasureTheory.AEEqFun.mk (fun (p : Ω × Ω) => W p.1 p.2) ⋯

theorem TauCeti.DenseGraphLimits.Graphon.coeFn_toAEEqFun {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : ↑W.toAEEqFun =ᵐ[μ.prod μ] fun (p : Ω × Ω) => W p.1 p.2

The class of a graphon is represented by the graphon itself.

theorem TauCeti.DenseGraphLimits.Graphon.toAEEqFun_eq_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {U W : Graphon Ω μ} : U.toAEEqFun = W.toAEEqFun ↔ ∀ᵐ (p : Ω × Ω) ∂μ.prod μ, U p.1 p.2 = W p.1 p.2

Two graphons have the same class exactly when they agree almost everywhere.

theorem TauCeti.DenseGraphLimits.Graphon.toAEEqFun_eq_of_ae {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {W : Graphon Ω μ} {f : Ω × Ω →ₘ[μ.prod μ] ℝ} (h : ∀ᵐ (p : Ω × Ω) ∂μ.prod μ, W p.1 p.2 = ↑f p) : W.toAEEqFun = f

A graphon whose values agree a.e. with a given class has that class.

theorem TauCeti.DenseGraphLimits.Graphon.toAEEqFun_mem_Icc_ae {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : ∀ᵐ (p : Ω × Ω) ∂μ.prod μ, ↑W.toAEEqFun p ∈ Set.Icc 0 1

The class of a graphon is a.e. [0, 1]-valued — one of the two constraints that characterise the classes coming from graphons.

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

The class of a graphon is a.e. symmetric — the other constraint characterising the classes coming from graphons. Symmetry of the representative is pointwise; transporting it to the class uses that Prod.swap preserves μ ⊗ μ.

theorem TauCeti.DenseGraphLimits.Graphon.toAEEqFun_comap {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Ω' : Type u_2} [MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ'] (W : Graphon Ω μ) {φ : Ω' → Ω} (hφ : MeasureTheory.MeasurePreserving φ μ' μ) : (W.comap φ ⋯ μ').toAEEqFun = W.toAEEqFun.compMeasurePreserving (Prod.map φ φ) ⋯

The a.e. view is compatible with measure-preserving pullbacks. Pulling a graphon back along a measure-preserving map is, on classes, Mathlib's AEEqFun.compMeasurePreserving along the pullback of the product carrier.

theorem TauCeti.DenseGraphLimits.homDensity_congr_ae {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] {U W : Graphon Ω μ} (h : ∀ᵐ (p : Ω × Ω) ∂μ.prod μ, U p.1 p.2 = W p.1 p.2) : homDensity F U = homDensity F W

Homomorphism densities factor through the a.e. class of a graphon. Changing a graphon on a μ ⊗ μ-null set changes no t(F, ·).

The hypothesis is the a.e. equality itself; for the equality of classes use Graphon.toAEEqFun_eq_iff.

theorem TauCeti.DenseGraphLimits.cutNorm_overlayDiff_congr_ae_left {Ω₁ : Type u_2} {Ω₂ : Type u_3} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {U U' : Graphon Ω₁ μ₁} {W : Graphon Ω₂ μ₂} {π : MeasureTheory.Measure (Ω₁ × Ω₂)} (hπ : MeasureTheory.IsCoupling μ₁ μ₂ π) (h : ∀ᵐ (p : Ω₁ × Ω₁) ∂μ₁.prod μ₁, U p.1 p.2 = U' p.1 p.2) : cutNorm π (overlayDiff U W π) = cutNorm π (overlayDiff U' W π)

Along any coupling, the overlaid cut norm only sees the a.e. class of the left graphon.

Almost everywhere equality holds on μ₁ ⊗ μ₁ while the overlaid difference lives on π ⊗ π; the two are related by the first-coordinate projection, which is measure preserving precisely because π is a coupling with left marginal μ₁.

theorem TauCeti.DenseGraphLimits.cutDist_congr_ae_left {Ω₁ : Type u_2} {Ω₂ : Type u_3} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {U U' : Graphon Ω₁ μ₁} {W : Graphon Ω₂ μ₂} (h : ∀ᵐ (p : Ω₁ × Ω₁) ∂μ₁.prod μ₁, U p.1 p.2 = U' p.1 p.2) : cutDist U W = cutDist U' W

The cut distance factors through the a.e. class of its left argument.

This is the full a.e.-invariance of δ□, not just of its vanishing, and it holds on arbitrary probability carriers: every coupling contributes the same value to the two infima, so the infima agree. No triangle inequality is involved.

theorem TauCeti.DenseGraphLimits.cutDist_congr_ae_right {Ω₁ : Type u_2} {Ω₂ : Type u_3} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {U : Graphon Ω₁ μ₁} {W W' : Graphon Ω₂ μ₂} (h : ∀ᵐ (p : Ω₂ × Ω₂) ∂μ₂.prod μ₂, W p.1 p.2 = W' p.1 p.2) : cutDist U W = cutDist U W'

The cut distance factors through the a.e. class of its right argument, by symmetry (cutDist_comm).

theorem TauCeti.DenseGraphLimits.cutDist_eq_zero_of_aeEq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {U W : Graphon Ω μ} (h : ∀ᵐ (p : Ω × Ω) ∂μ.prod μ, U p.1 p.2 = W p.1 p.2) : cutDist U W = 0

Almost everywhere equal graphons are at cut distance zero. Replacing U by the a.e. equal W leaves δ□(U, W) unchanged, and δ□(W, W) = 0.

No triangle inequality is used, so this holds on an arbitrary probability carrier.

theorem TauCeti.DenseGraphLimits.exists_graphon_repr {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (f : Ω × Ω →ₘ[μ.prod μ] ℝ) (hbdd : ∀ᵐ (p : Ω × Ω) ∂μ.prod μ, ↑f p ∈ Set.Icc 0 1) (hsymm : ∀ᵐ (p : Ω × Ω) ∂μ.prod μ, ↑f p = ↑f p.swap) : ∃ (W : Graphon Ω μ), W.toAEEqFun = f

The reverse bridge: an a.e. [0, 1]-valued, a.e. symmetric class comes from a graphon. This is the measurable-selection step that lets AEEqFun-native constructions — conditional expectations, martingale limits — be read back as strict graphons.

The witness is built from a measurable representative by averaging it with its transpose and clamping to [0, 1]; both operations are the identity almost everywhere, and both are needed, since a representative has no reason to be symmetric or [0, 1]-valued at every point.

theorem TauCeti.DenseGraphLimits.exists_graphon_repr_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (f : Ω × Ω →ₘ[μ.prod μ] ℝ) : (∃ (W : Graphon Ω μ), W.toAEEqFun = f) ↔ (∀ᵐ (p : Ω × Ω) ∂μ.prod μ, ↑f p ∈ Set.Icc 0 1) ∧ ∀ᵐ (p : Ω × Ω) ∂μ.prod μ, ↑f p = ↑f p.swap

The classes that come from graphons are exactly the a.e. [0, 1]-valued, a.e. symmetric ones. The forward direction is the pointwise range and symmetry of a strict graphon read on its class; the converse is exists_graphon_repr.