Documentation

TauCeti.MeasureTheory.OptimalTransport.GromovWasserstein.Zero

Zero Gromov–Wasserstein distance and presentation invariance #

For probability measures on standard Borel carriers and a.e. strongly measurable kernels into an extended metric space, zero Gromov–Wasserstein distance is equivalent to weak isomorphism. This holds at every nonzero exponent, including infinity, without moment bounds or separability of the target. More generally, tight Borel probability measures on second-countable metrizable carriers suffice. A compatible Polish topology on each standard Borel carrier recovers the standard Borel result from this tight-measure criterion. At the measurable root, the criterion needs only an optimal coupling and a weak extended metric target, with no topology on the carriers, finiteness, or measurability assumptions on the kernels.

At every exponent, weak isomorphisms preserve distance to a third measured kernel. These invariance statements need only an extended pseudometric target and finite measures on the two isomorphic carriers, assuming couplings glue in both orders. A standard Borel comparison carrier supplies these gluings. Together with the zero-distance characterization, they supply the separation and representative-independence needed to put Gromov–Wasserstein distance on weak-isomorphism classes. No equality of the raw presentations is asserted.

References #

theorem TauCeti.gromovWassersteinEDist_eq_zero_iff_of_exists_optimal_coupling {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {ωX : X × X → Z} {ωY : Y × Y → Z} {p : ENNReal} [TopologicalSpace Z] [WeakEMetricSpace Z] (hopt : ∃ (π : MeasureTheory.Measure (X × Y)), IsCoupling π μ ν ∧ gromovWassersteinDistortion p ωX ωY π = gromovWassersteinEDist p μ ωX ν ωY) (hp : p ≠ 0) :
gromovWassersteinEDist p μ ωX ν ωY = 0 ↔ AreWeaklyIsomorphicKernels μ ωX ν ωY

When an optimal coupling exists, zero Gromov–Wasserstein distance is exactly weak isomorphism at every nonzero exponent. The carriers need only measurable structures; the measures need not be finite and the kernels need not be measurable. The target's topology need not be induced by its extended distance.

For a.e. strongly measurable kernels with tight Borel probability measures on second-countable metrizable spaces, zero Gromov–Wasserstein distance is exactly weak isomorphism at every nonzero exponent. The target needs neither a measurable structure nor separability, completeness, or finite moments.

For a.e. strongly measurable kernels on standard Borel probability spaces, zero Gromov–Wasserstein distance is exactly weak isomorphism, at every nonzero exponent. The target needs neither a measurable structure nor separability, completeness, or finite moments.

theorem TauCeti.AreWeaklyIsomorphicKernels.gromovWassersteinEDist_congr_left_of_exists_glue {X : Type u_1} {Y : Type u_2} {W : Type u_3} {Z : Type u_4} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace W] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {ρ : MeasureTheory.Measure W} {ωX : X × X → Z} {ωY : Y × Y → Z} {ωW : W × W → Z} {p : ENNReal} [PseudoEMetricSpace Z] [MeasureTheory.IsFiniteMeasure μ] (h : AreWeaklyIsomorphicKernels μ ωX ν ωY) (hωX : MeasureTheory.AEStronglyMeasurable ωX (μ.prod μ)) (hωY : MeasureTheory.AEStronglyMeasurable ωY (ν.prod ν)) (hωW : MeasureTheory.AEStronglyMeasurable ωW (ρ.prod ρ)) (hglueXYW : ∀ (π : MeasureTheory.Measure (X × Y)) (σ : MeasureTheory.Measure (Y × W)), IsCoupling π μ ν → IsCoupling σ ν ρ → ∃ (γ : MeasureTheory.Measure (X × Y × W)), MeasureTheory.Measure.map (Prod.map id Prod.fst) γ = π ∧ γ.snd = σ) (hglueYXW : ∀ (π : MeasureTheory.Measure (Y × X)) (σ : MeasureTheory.Measure (X × W)), IsCoupling π ν μ → IsCoupling σ μ ρ → ∃ (γ : MeasureTheory.Measure (Y × X × W)), MeasureTheory.Measure.map (Prod.map id Prod.fst) γ = π ∧ γ.snd = σ) :
gromovWassersteinEDist p μ ωX ρ ωW = gromovWassersteinEDist p ν ωY ρ ωW

Replacing the first measured kernel by a weakly isomorphic one preserves its distance to a third measured kernel whenever couplings glue in both orders of the isomorphic carriers. This holds at every exponent. No standard Borel structure is required, and the comparison measure need not be finite.

theorem TauCeti.AreWeaklyIsomorphicKernels.gromovWassersteinEDist_congr_right_of_exists_glue {X : Type u_1} {Y : Type u_2} {W : Type u_3} {Z : Type u_4} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace W] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {ρ : MeasureTheory.Measure W} {ωX : X × X → Z} {ωY : Y × Y → Z} {ωW : W × W → Z} {p : ENNReal} [PseudoEMetricSpace Z] [MeasureTheory.IsFiniteMeasure μ] (h : AreWeaklyIsomorphicKernels μ ωX ν ωY) (hωX : MeasureTheory.AEStronglyMeasurable ωX (μ.prod μ)) (hωY : MeasureTheory.AEStronglyMeasurable ωY (ν.prod ν)) (hωW : MeasureTheory.AEStronglyMeasurable ωW (ρ.prod ρ)) (hglueXYW : ∀ (π : MeasureTheory.Measure (X × Y)) (σ : MeasureTheory.Measure (Y × W)), IsCoupling π μ ν → IsCoupling σ ν ρ → ∃ (γ : MeasureTheory.Measure (X × Y × W)), MeasureTheory.Measure.map (Prod.map id Prod.fst) γ = π ∧ γ.snd = σ) (hglueYXW : ∀ (π : MeasureTheory.Measure (Y × X)) (σ : MeasureTheory.Measure (X × W)), IsCoupling π ν μ → IsCoupling σ μ ρ → ∃ (γ : MeasureTheory.Measure (Y × X × W)), MeasureTheory.Measure.map (Prod.map id Prod.fst) γ = π ∧ γ.snd = σ) :
gromovWassersteinEDist p ρ ωW μ ωX = gromovWassersteinEDist p ρ ωW ν ωY

Replacing the second measured kernel by a weakly isomorphic one preserves its distance from a third measured kernel whenever couplings glue in both orders of the isomorphic carriers, with the comparison carrier last. This holds at every exponent, and the comparison measure need not be finite.

Replacing the first measured kernel by a weakly isomorphic one preserves its distance to a standard Borel measured kernel at every exponent. The comparison measure need not be finite.

Replacing the second measured kernel by a weakly isomorphic one preserves its distance from a standard Borel measured kernel at every exponent. The comparison measure need not be finite.