Stability of graphon cut distance under approximation

The coupling cut distance is stable when either graphon is replaced by a nearby graphon on the same carrier. Quantitatively,

|δ□(U, W) - δ□(U', W')| ≤ ‖U - U'‖□ + ‖W - W'‖□.

This estimate does not use the triangle inequality for cutDist. Instead, fix a coupling used to compare U' and W. On that coupling, the overlaid difference of U and W splits into the pullback of U - U' plus the overlaid difference of U' and W. The cut-norm triangle inequality bounds the sum, and invariance under the measure-preserving coordinate projection identifies the first summand with ‖U - U'‖□. Taking the infimum over the same couplings gives the one-coordinate estimate; symmetry and a second replacement give the displayed bound.

The result is the stability input for the finite-step reduction in the arbitrary-carrier triangle inequality. Once graphons have been approximated by finite step graphons, a triangle estimate for the finite approximants transfers to the original graphons with precisely the two cut-norm errors recorded here. Thus no disintegration of an arbitrary intermediate carrier is hidden in this module.

Main results

• TauCeti.DenseGraphLimits.abs_cutDist_sub_left_le_cutNorm bounds the effect of changing the graphon on the left carrier.
• TauCeti.DenseGraphLimits.abs_cutDist_sub_right_le_cutNorm is the corresponding bound on the right carrier.
• TauCeti.DenseGraphLimits.abs_cutDist_sub_le_cutNorm_add_cutNorm changes both graphons at once.
• TauCeti.DenseGraphLimits.cutDist_le_add_two_mul_cutNorm_of_le_add transfers a triangle estimate proved with an approximating intermediate graphon back to the original intermediate.

References

• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013), Lemma 6.5.
• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, the Layer-1 design-validation milestone requiring stability of the finite coupling reduction under step approximation.

theorem TauCeti.DenseGraphLimits.abs_cutDist_sub_left_le_cutNorm {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U U' : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) : |cutDist U W - cutDist U' W| ≤ cutNorm μ₁ (U.toSymmKernel - U'.toSymmKernel)

Stability under replacement on the left carrier. If U and U' are graphons on the same probability space, then their cut distances to any graphon W differ by at most ‖U - U'‖□.

No triangle inequality for cutDist is used: the proof compares the two overlaid differences along each individual coupling.

theorem TauCeti.DenseGraphLimits.abs_cutDist_sub_right_le_cutNorm {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W W' : Graphon Ω₂ μ₂) : |cutDist U W - cutDist U W'| ≤ cutNorm μ₂ (W.toSymmKernel - W'.toSymmKernel)

Stability under replacement on the right carrier. If W and W' are graphons on the same probability space, then their cut distances from any graphon U differ by at most ‖W - W'‖□.

theorem TauCeti.DenseGraphLimits.abs_cutDist_sub_le_cutNorm_add_cutNorm {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U U' : Graphon Ω₁ μ₁) (W W' : Graphon Ω₂ μ₂) : |cutDist U W - cutDist U' W'| ≤ cutNorm μ₁ (U.toSymmKernel - U'.toSymmKernel) + cutNorm μ₂ (W.toSymmKernel - W'.toSymmKernel)

Two-coordinate stability of coupling cut distance. Replacing both graphons by graphons on their respective carriers changes their cut distance by at most the sum of the two same-carrier cut-norm errors.

This is the quantitative form used by step approximation: a finite-step estimate transfers to the original pair once each endpoint is close to its finite-step approximant in cut norm.

theorem TauCeti.DenseGraphLimits.cutDist_le_add_two_mul_cutNorm_of_le_add {Ω₁ : Type u_1} {Ω₂ : Type u_2} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] {Ω₃ : Type u_3} [MeasurableSpace Ω₃] {μ₃ : MeasureTheory.Measure Ω₃} [MeasureTheory.IsProbabilityMeasure μ₃] (U : Graphon Ω₁ μ₁) (W W' : Graphon Ω₂ μ₂) (X : Graphon Ω₃ μ₃) (h : cutDist U X ≤ cutDist U W' + cutDist W' X) : cutDist U X ≤ cutDist U W + cutDist W X + 2 * cutNorm μ₂ (W.toSymmKernel - W'.toSymmKernel)

Transfer of a triangle estimate from an approximating intermediate graphon. Suppose a triangle estimate has been proved with W' as the intermediate graphon. Replacing W' by a graphon W on the same carrier costs at most twice ‖W - W'‖□, once for each leg of the triangle.

The finite-step reduction uses this with W' a step approximation of W: finite-middle coupling gluing supplies the hypothesis, and letting the cut-norm error tend to zero yields the desired triangle estimate through W.