The map form of the cut distance, and its agreement with the coupling form #
The map form of the cut distance is the classical one: read both graphons on the canonical
carrier (I, volume) through measure-preserving maps, and take the infimum of the cut norm of the
difference of the two pullbacks,
δ□ᵐᵃᵖ(U, W) = inf { ‖U ∘ (f × f) − W ∘ (g × g)‖□ | f : I → Ω₁, g : I → Ω₂ measure preserving }.
The main result is that it agrees with the coupling-primary cutDist over standard Borel carriers,
cutDist_eq_cutDistPullback. This is the design equivalence that justifies taking the coupling
form as primary: nothing is lost by doing so, since on the carriers where the classical definition
is usually stated the two numbers are equal.
Atoms are allowed. No atomless hypothesis appears on either carrier, and none is needed. The
inequality cutDistPullback ≤ cutDist turns a coupling into a pair of maps by pushing (I, volume)
forward onto the coupling itself — a probability measure on the standard Borel space Ω₁ × Ω₂ —
and exists_measurePreserving_from_unitInterval (Janson, Thm A.9) does that with no atomless
hypothesis. That is the whole content of the harder direction: an arbitrary coupling, however
atomic, is realized by a pair of measure-preserving maps out of (I, volume), because the pair of
projections of such a realization has the coupling as its joint law. The companion
CutMetric.Pullback.Validation module evaluates the map form through the equivalence at a
point-mass coupling, at finitely atomic ones, and at ones mixing an atomic with a continuous
direction; these regressions are what the absence of an atomless hypothesis buys, and each fails to
typecheck for any formulation that assumes one.
Why the easy direction is easy. A pair of measure-preserving maps f, g out of a common
carrier pushes that carrier forward to a coupling along x ↦ (f x, g x), and the overlaid
difference along that coupling pulls back to the plain difference of pullbacks — this is
cutDist_le_cutNorm_sub_of_measurePreserving, already available on an arbitrary common carrier.
Specializing it to (I, volume) gives cutDist ≤ cutDistPullback outright.
The junk value. cutDistPullback is an infimum over a set of reals that is empty when a
carrier receives no measure-preserving map from (I, volume) at all, and then it is 0 by the
sInf convention. The elimination rules — and cutDist_le_cutDistPullback through them — carry
standard Borel hypotheses on the two carriers that rule this out (pullbackCutNorms_nonempty);
cutDistPullback_le_cutDist runs the other way and only needs the product carrier standard Borel,
which is where it applies Thm A.9. The range and common-carrier bounds hold with no such hypothesis
at all: in the empty case they reduce to the corresponding fact about 0, and in the nonempty case
any witness supplies the required upper bound.
Main definitions #
TauCeti.DenseGraphLimits.cutDistPullback— the infimum, over pairs of measure-preserving maps from(I, volume)to the two carriers, of the cut norm of the difference of the two pullbacks.
Main results #
cutDist_eq_cutDistPullback— the coupling and map forms of the cut distance agree over standard Borel carriers, atoms allowed; it iscutDist_le_cutDistPullbackandcutDistPullback_le_cutDisttogether;cutDistPullback_leandle_cutDistPullbackare the introduction and elimination rules for the infimum, andexists_measurePreserving_cutNorm_sub_ltproduces a pair of maps beating any strict upper bound;cutDistPullback_defspells the defining infimum out in public terms;cutDistPullback_commis symmetry, and holds with no hypothesis on either carrier;cutDistPullback_nonneg,cutDistPullback_le_one,cutDistPullback_selfandcutDistPullback_le_cutNorm_subare the range and the same-carrier bounds.
References #
- S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4
(2013), Thm 6.9 (the two forms agree) with Thm A.9 (the transport from
(I, volume)). - L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §8.2.
- Roadmap:
TauCetiRoadmap/DenseGraphLimits/README.md, Layer 5 —cutDistPullbackandcutDist_eq_cutDistPullback, whose signatures followTauCetiRoadmap/DenseGraphLimits/Suggested.lean(with the two carrier measures implicit, as they are forcutDisthere). The atomless mod-null equivalenceexists_mpModNull_equiv_unitIntervalis the layer's other target and is not built here.
The map form of the cut distance: the infimum, over measure-preserving maps from the
canonical carrier (I, volume) to each of (Ω₁, μ₁) and (Ω₂, μ₂), of the cut norm of the
difference of the two pullbacks.
This is the classical definition. Over standard Borel carriers it agrees with the
coupling-primary cutDist (cutDist_eq_cutDistPullback); off them it can be a junk 0, since the
infimum is then taken over an empty set.
Equations
Instances For
The defining infimum of the map form of the cut distance, with its index set spelled out in
public terms: the cut norms of the differences of the two pullbacks, one for each pair of
measure-preserving maps out of (I, volume).
Ordinary use should go through cutDistPullback_le and le_cutDistPullback instead; this is the
escape hatch for a goal that has to be stated or rewritten at the infimum itself.
The map form of the cut distance is at most the pulled-back cut norm along any pair of measure-preserving maps: the introduction rule for the infimum.
To bound the map form of the cut distance from below it suffices to bound every pulled-back cut norm from below: the elimination rule for the infimum. The standard Borel hypotheses are what make the infimum a genuine one rather than the empty-set junk value.
Any strict upper bound on the map form of the cut distance is beaten by some pair of
measure-preserving maps. This is the form in which a cutDistPullback hypothesis is used: it turns
an infimum into an explicit pair of maps.
The map form of the cut distance is symmetric.
No hypothesis is needed: the two infima are taken over the same set of reals, since a pair
(f, g) for (U, W) is a pair (g, f) for (W, U) with the same value.
The map form of the cut distance is nonnegative.
The two forms agree #
A pair of measure-preserving maps bounds the cut distance from above. This is the easy half
of cutDist_eq_cutDistPullback: the graph of (f, g) pushes volume forward to a coupling, along
which the overlaid difference is exactly the difference of the two pullbacks.
Every coupling is realized by a pair of measure-preserving maps. This is the substance of
cutDist_eq_cutDistPullback.
A coupling π of μ₁ and μ₂ is a probability measure on Ω₁ × Ω₂, so Janson's Thm A.9 gives a
measure-preserving h : I → Ω₁ × Ω₂. Its two coordinates are measure preserving onto the two
carriers, and h is their pairing, so the overlaid difference along π pulls back along h to the
difference of the two pullbacks. No atomless hypothesis enters: π may be a point mass.
Only the product carrier is assumed standard Borel, which is all Thm A.9 is applied to here; when
both factors are standard Borel — the hypotheses of cutDist_eq_cutDistPullback — the instance is
synthesized from them.
The coupling and map forms of the cut distance agree, over standard Borel carriers, with atoms allowed.
This is the design equivalence behind the coupling-primary definition: the classical
measure-preserving-map infimum is not more general, so nothing is lost by taking the cross-carrier
coupling form — which needs no hypothesis even to be stated — as the primary object. In particular
the whole cutDist API transfers to cutDistPullback over standard Borel carriers.
The map form of the cut distance is at most 1.
The map form of the cut distance of a graphon to itself is zero.
On a common carrier the map form of the cut distance is at most the cut norm of the difference.
As for cutDist_le_cutNorm_sub, the reverse inequality is false: a measure-preserving rearrangement
of the carrier leaves the left-hand side at 0 while the right-hand side can be bounded away from
it.