Reading a graphon on another carrier #

A graphon on (Ω, μ) may be read on any other probability space through a measurable map f : Ω' → Ω, by evaluating it at the images of both arguments: W.comap f hf μ' x y = W (f x) (f y). Symmetry, measurability and the [0, 1] range all survive, so the result is again a graphon.

This is SymmKernel.comap with the range constraint carried along, and it is the object that makes the cross-carrier theory run: the two graphons compared by the cut distance live on different spaces, and a coupling π of their carriers turns both into graphons on (Ω₁ × Ω₂, π) — the pullbacks along the two coordinate projections, whose difference is TauCeti.DenseGraphLimits.overlayDiff. Nothing here needs f to be measure preserving; that hypothesis enters only where an integral is transported, as in TauCeti.DenseGraphLimits.homDensity_comap.

Main definitions #

TauCeti.DenseGraphLimits.Graphon.comap — the pullback of a graphon along a measurable map.

Main results #

Graphon.comap_apply — the eliminator W.comap f hf μ' x y = W (f x) (f y);
Graphon.toSymmKernel_comap — the pullback of a graphon is the pullback of its kernel, which is how the cut norm and the kernel algebra see it;
Graphon.comap_id, Graphon.comap_comap, Graphon.comap_const — functoriality and the constant graphon.

References #

Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 1 — the basic API of the Graphon object, and the cross-carrier reading of two graphons through a coupling that the coupling-primary cutDist rests on.
S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), §6.

source

def TauCeti.DenseGraphLimits.Graphon.comap {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (f : Ω' → Ω) (hf : Measurable f) (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsProbabilityMeasure μ'] :

Graphon Ω' μ'

The pullback of a graphon along a measurable map f : Ω' → Ω, acting on both arguments: W.comap f hf μ' x y = W (f x) (f y).

The underlying kernel is SymmKernel.comap, so symmetry, measurability and boundedness are inherited from there; the [0, 1] range is inherited pointwise. As for kernels, no hypothesis on either measure is needed — μ' only has to be a probability measure for the result to be a graphon at all.

The argument order follows SymmKernel.comap: the map first, then its measurability, then the carrier measure of the result, which the data does not determine.

Equations

W.comap f hf μ' = { toSymmKernel := W.comap f hf μ', mem01' := ⋯ }

Instances For

source

@[simp]

theorem TauCeti.DenseGraphLimits.Graphon.comap_apply {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (f : Ω' → Ω) (hf : Measurable f) (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsProbabilityMeasure μ'] (x y : Ω') :

(W.comap f hf μ') x y = W (f x) (f y)

Pulling back a graphon evaluates it after applying the map to both arguments.

source

@[simp]

theorem TauCeti.DenseGraphLimits.Graphon.toSymmKernel_comap {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (f : Ω' → Ω) (hf : Measurable f) (μ' : MeasureTheory.Measure Ω') [MeasureTheory.IsProbabilityMeasure μ'] :

(W.comap f hf μ').toSymmKernel = W.comap f hf μ'

The underlying kernel of a pulled-back graphon is the pullback of its kernel. This is the form the cut norm and the kernel algebra consume, so it is the bridge between this file and TauCeti.Combinatorics.DenseGraphLimits.Kernel.Pullback.

source

@[simp]