The metric space of measured kernels #
GromovWassersteinPresentation p Z bundles a standard Borel probability carrier and an
almost-everywhere strongly measurable Z-valued kernel with finite p-size. This is the
finite-distance category, not a replacement for the unrestricted raw-measure definitions in
GromovWasserstein.Basic. The exponent is a parameter, and the moment condition existentially
quantifies its basepoint, so no chosen basepoint is part of a presentation.
For 1 ≤ p, presentations carry the Gromov–Wasserstein pseudometric.
GromovWassersteinSpace p Z uses Mathlib's SeparationQuotient of this pseudometric.
Two presentations have the same class exactly when their kernels are weakly isomorphic,
not when their carriers or kernels are equal.
The quotient has a genuine metric, with the original coupling formula as its extended distance.
This includes p = ∞, where finite size means essential boundedness.
One-point kernels give an isometric embedding of Z into this space. Comparing with these
kernels proves finiteness of all distances without requiring a globally separable or complete
target. Common-parametrization bounds and filter convergence criteria transfer L^p convergence of
pulled-back kernels on an auxiliary space directly to convergence of presentations and weak
isomorphism classes. Carrier universes are fixed independently of the target universe.
References #
- M. Bauer, F. Mémoli, T. Needham and M. Nishino, The Z-Gromov–Wasserstein distance, J. Mach. Learn. Res. 26 (2025), Definition 28 and the metric on weak-isomorphism classes. The distance here uses the full distortion, without their factor of one half.
A finite-p measured-kernel presentation on a standard Borel probability carrier.
The target needs no separability or completeness. Presentations themselves are not identified
under null changes or measure-preserving parametrizations; GromovWassersteinSpace makes
exactly those identifications.
- Carrier : Type u
The measurable carrier of the kernel.
- measurableSpace : MeasurableSpace self.Carrier
The sigma-algebra on the carrier.
- standardBorelSpace : StandardBorelSpace self.Carrier
Standard Borel structure supplies coupling gluing and attainment.
- measure : MeasureTheory.Measure self.Carrier
The probability law on the carrier.
- isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure self.measure
The carrier law has total mass one.
The target-valued kernel, with no symmetry assumption.
- aestronglyMeasurable_kernel : MeasureTheory.AEStronglyMeasurable self.kernel (self.measure.prod self.measure)
Strong measurability is needed only almost everywhere on the square.
- finite_moment : ∃ (z : Z), MeasureTheory.MemLp (fun (q : self.Carrier × self.Carrier) => edist (self.kernel q) z) p (self.measure.prod self.measure)
Finite size about some target point, including essential boundedness at infinity.
Instances For
The one-point presentation with constant kernel value z.
Instances For
Distance to the constant one-point kernel is exactly the size about that point.
Between constant one-point kernels, GW recovers the target metric at nonzero exponents.
Finite size at possibly different basepoints suffices for finite GW distance.
The GW pseudometric on finite-size standard Borel presentations. Distinct presentations may have distance zero; only the subsequent quotient is a metric space.
The pseudometric on presentations is the original infimum over couplings.
The common-parametrization bound for presentations along a.e.-measurable maps: if f and
g push an s-finite measure γ forward to K.measure and L.measure, the GW distance of K and
L is at most the L^p (γ ⊗ γ) discrepancy of their pulled-back kernels.
The common-parametrization bound for presentations along measure-preserving maps.
Convergence of presentations from a common parametrization. Along any filter l, if
a.e.-measurable maps f i (eventually along l) and g push an s-finite measure γ forward to
(Ks i).measure and L.measure, and the L^p (γ ⊗ γ) discrepancy between the pulled-back kernels
tends to zero, then Ks tends to L in the GW pseudometric.
Convergence of presentations from measure-preserving common parametrizations.
Finite-size standard Borel measured kernels modulo weak isomorphism, with the full Gromov–Wasserstein metric. The carrier universe is fixed, but is independent of the target.
Instances For
The separation quotient of the presentation pseudometric is a genuine metric space.
Pass from a presentation to its weak-isomorphism class.
Instances For
Every GW class has a presentation in the fixed carrier universe.
The quotient extended distance is exactly the raw GW coupling infimum.
Passing from presentations to weak-isomorphism classes is an isometry.
The real metric is the finite raw GW value read in ℝ.
Equality of classes is precisely weak isomorphism, witnessed by an exact coupling. It does not assert equality of presentations, even after null modifications.
Convergence in GW space from a common parametrization. Along any filter l, if
a.e.-measurable maps f i (eventually along l) and g push an s-finite measure γ forward to
(Ks i).measure and L.measure, and the L^p (γ ⊗ γ) discrepancy between the pulled-back kernels
tends to zero, then mk (Ks i) tends to mk L.
Convergence in GW space from measure-preserving common parametrizations.
Descend any weak-isomorphism-invariant function on presentations to GW classes.
Instances For
A descended function takes its prescribed value on every presentation.
The class of the one-point kernel with value z.
Instances For
Distance from a presented kernel to a one-point class is its size about that point.
A measured-kernel presentation is the one-point class at z exactly when its kernel
is almost everywhere equal to z.
The target embeds isometrically as constant one-point kernels in GW space.