The overlaid difference of two graphons

Given a coupling of two probability spaces, two graphons living on different carriers can be compared: read U through the first coordinate, read W through the second, and subtract. The result is the overlaid difference kernel overlayDiff U W π, a symmetric kernel on the coupled space (Ω₁ × Ω₂, π). The carrier-independent coupling API lives in TauCeti.MeasureTheory.Measure.Coupling.Basic.

These two objects are what makes the cut distance of the dense graph limit theory cross-carrier. cutDist U W is the infimum, over all couplings π, of the cut norm of overlayDiff U W π; the cut norm acts on kernels, and overlayDiff U W π is exactly the kernel it is applied to. Neither object needs a standard Borel or atomless hypothesis, which is why the resulting distance is defined on arbitrary probability carriers. That its triangle inequality also holds there is a separate result, proved by step-graphon approximation (Janson, Lemma 6.5) rather than by gluing couplings, and is not built here.

overlayDiff does not need the coupling hypothesis. The measure argument of SymmKernel is a phantom parameter, so the kernel fun p q => U p.1 q.1 - W p.2 q.2 is well-formed over any measure π on Ω₁ × Ω₂. The marginal conditions enter one level up, where the cut norm integrates against π; keeping them off the constructor means the pointwise algebra below — and in particular overlayDiff_swap, the swap symmetry the cut distance's cutDist_comm runs on — carries no hypotheses at all.

Main definitions

• TauCeti.DenseGraphLimits.overlayDiff — the overlaid difference kernel of two graphons on a coupling of their carriers.

Main results

• overlayDiff_apply, abs_overlayDiff_apply_le_one — the eliminator and the [-1, 1] bound;
• overlayDiff_swap — swapping the two graphons negates the overlaid difference, up to the pullback along Prod.swap, for any two measures on the two products;
• comap_overlayDiff_prodMk — pulling back along a pair of maps gives the difference of the two kernel pullbacks;
• comap_overlayDiff_diagonalCoupling — on a common carrier the overlaid difference along the diagonal coupling pulls back along the diagonal to the plain difference U - W.

References

• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 1 — IsCoupling, isCoupling_prod, overlayDiff and overlayDiff_apply, the ingredients of the coupling-primary cross-carrier cutDist. The cut norm, cutDist itself, its triangle inequality, and the GraphonSpace quotient are separate targets and are not built here. The signatures follow TauCetiRoadmap/DenseGraphLimits/Suggested.lean, which pins IsCoupling as a Prop (not a structure or class) for the reason recorded above.
• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), §6 — cut distance via couplings.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §8.2.

def TauCeti.DenseGraphLimits.overlayDiff {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) (π : MeasureTheory.Measure (Ω₁ × Ω₂)) : SymmKernel (Ω₁ × Ω₂) π

The overlaid difference kernel of two graphons along a measure π on the product of their carriers: U read through the first coordinate minus W read through the second.

This is the kernel whose cut norm the cut distance minimizes over couplings — not a neutral overlay of the two graphons, but the difference that the counting lemma bounds a density gap by. It is a literal difference of two SymmKernel.comaps, so the kernel algebra applies to it directly.

The measure π is unconstrained here: SymmKernel carries its measure as a phantom parameter, and the marginal conditions are only needed once the cut norm integrates against π.

Equations

• TauCeti.DenseGraphLimits.overlayDiff U W π = U.comap Prod.fst ⋯ π - W.comap Prod.snd ⋯ π

@[simp]

theorem TauCeti.DenseGraphLimits.overlayDiff_apply {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) (π : MeasureTheory.Measure (Ω₁ × Ω₂)) (p q : Ω₁ × Ω₂) : (overlayDiff U W π) p q = U p.1 q.1 - W p.2 q.2

The overlaid difference evaluates as the difference of the two graphons read through the two coordinates.

theorem TauCeti.DenseGraphLimits.abs_overlayDiff_apply_le_one {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) (π : MeasureTheory.Measure (Ω₁ × Ω₂)) (p q : Ω₁ × Ω₂) : |(overlayDiff U W π) p q| ≤ 1

The overlaid difference of two graphons takes values in [-1, 1]: it is a difference of two [0, 1]-valued functions.

theorem TauCeti.DenseGraphLimits.overlayDiff_swap {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) (π : MeasureTheory.Measure (Ω₁ × Ω₂)) (ρ : MeasureTheory.Measure (Ω₂ × Ω₁)) : overlayDiff W U ρ = -(overlayDiff U W π).comap Prod.swap ⋯ ρ

Swapping the roles of the two graphons — and correspondingly the two coordinates of the coupling — negates the overlaid difference.

This is the identity behind the symmetry of the cut distance: the cut norm is even and invariant under the pullback along the measure-preserving Prod.swap, so the two infima agree. Both measures are unconstrained — they are phantom parameters of the two kernel types — so a caller holding a coupling ρ of μ₂, μ₁ may use it directly, without rewriting ρ into the form π.map Prod.swap inside its type.

theorem TauCeti.DenseGraphLimits.comap_overlayDiff_prodMk {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {Ω : Type u_3} [MeasurableSpace Ω] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) (π : MeasureTheory.Measure (Ω₁ × Ω₂)) {f : Ω → Ω₁} {g : Ω → Ω₂} (hf : Measurable f) (hg : Measurable g) (ν : MeasureTheory.Measure Ω) : (overlayDiff U W π).comap (fun (x : Ω) => (f x, g x)) ⋯ ν = U.comap f hf ν - W.comap g hg ν

Pulling an overlaid difference back along x ↦ (f x, g x) gives the difference of the two pulled-back kernels.

theorem TauCeti.DenseGraphLimits.comap_overlayDiff_diagonalCoupling {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (U W : Graphon Ω μ) : (overlayDiff U W (MeasureTheory.diagonalCoupling μ)).comap (fun (x : Ω) => (x, x)) ⋯ μ = U.toSymmKernel - W.toSymmKernel

On a common carrier, the overlaid difference of U and W along the diagonal coupling pulls back along the diagonal x ↦ (x, x) to their plain difference as kernels.

TauCeti.MeasureTheory.diagonalCoupling μ is the pushforward of μ along that same diagonal, and by TauCeti.MeasureTheory.isCoupling_diagonalCoupling it is one of the couplings the cross-carrier cut distance takes an infimum over. This identity computes the kernel it contributes; recognizing the resulting value as the same-carrier cut norm ‖U - W‖□ additionally needs the invariance of the cut norm under measure-preserving pullback, and is cutNorm_overlayDiff_diagonalCoupling in TauCeti.Combinatorics.DenseGraphLimits.CutMetric.Distance.