Cross-carrier cut-norm contraction, isometry, and stability under measure-preserving pullback

cutNormDiff_pullback_le_measurePreserving: pulling two graphons back along a measure-preserving map between different carriers does not increase their cut-norm difference. Step 1 of the step-approximation programme.

Step 4 adds the two generic halves that live at this level of generality: cutNormDiff_pullback_eq_measurePreserving — for kernels factoring through the same measure-preserving map the pullback is an exact cut-norm isometry, since every rectangle test transports with equal value (rectIntegralDiff_pullback_preimage) — and abs_cutNormDiff_pullback_sub_le, Lipschitz stability of coupling cost: changing both marginal kernels moves the pulled-back cut-norm difference by at most the sum of the marginal cut-norm differences.

No standard Borel hypothesis. The same-carrier cutNormDiff_pullback_le carries [StandardBorelSpace α], but its proof is a pure Radon–Nikodym argument: the weight of a rectangle side S is the density of (μ.restrict S).map φ against the target measure — a sub-probability density, [0,1]-valued almost everywhere — and the weighted rectangle integral is dominated by the cut norm (abs_weighted_integral_diff_le, itself proved by layer cake with no regularity of the carrier). This file states the theorem in the generality the proof supports: arbitrary probability carriers on both sides. Zero-mass rectangle sides need no special treatment — the density of a zero measure is zero.

Deliberately not here: pushing couplings to quotients is the companion result in Graphon.ForMathlib.CouplingGluing; lifting factor laws back is Graphon.ForMathlib.CountableFactorLift; step-kernel cost transport consumes this file in Graphon.StepCostTransport; any triangle-inequality claim is a later unit of the programme.

theorem Graphon.cutNormDiff_pullback_le_measurePreserving {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (U W : Graphon β ν) (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν) : (U.pullback φ hφ).cutNormDiff (W.pullback φ hφ) ≤ U.cutNormDiff W

Cross-carrier cut-norm contraction: pulling back along a measure-preserving map between arbitrary probability carriers does not increase the cut-norm difference. No standard Borel hypothesis — the weights are Radon–Nikodym densities of the mapped restricted measures.

theorem Graphon.rectIntegralDiff_pullback_preimage {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (U W : Graphon β ν) (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν) {S T : Set β} (hS : MeasurableSet S) (hT : MeasurableSet T) : (U.pullback φ hφ).rectIntegralDiff (W.pullback φ hφ) (φ ⁻¹' S) (φ ⁻¹' T) = U.rectIntegralDiff W S T

Rectangle transport: the rectangle integral of a pulled-back difference over a pulled-back rectangle equals the original rectangle integral — change of variables along the measure-preserving map, restricted to the rectangle sides.

theorem Graphon.le_cutNormDiff_pullback_measurePreserving {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (U W : Graphon β ν) (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν) : U.cutNormDiff W ≤ (U.pullback φ hφ).cutNormDiff (W.pullback φ hφ)

Cross-carrier cut-norm expansion bound: the original cut-norm difference is attained among the pulled-back kernels — every rectangle test on the target lifts to the pulled-back rectangle test on the source with the same value.

theorem Graphon.cutNormDiff_pullback_eq_measurePreserving {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (U W : Graphon β ν) (φ : α → β) (hφ : MeasureTheory.MeasurePreserving φ μ ν) : (U.pullback φ hφ).cutNormDiff (W.pullback φ hφ) = U.cutNormDiff W

Cross-carrier cut-norm isometry: for kernels that factor through the map — both compared kernels are pullbacks along the same measure-preserving map — the pullback is an exact cut-norm isometry, not merely a contraction. Combines the contraction (cutNormDiff_pullback_le_measurePreserving) with rectangle transport.

theorem Graphon.abs_cutNormDiff_pullback_sub_le {α : 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 U' : Graphon β ν) (W W' : Graphon γ ρ) (φ : α → β) (ψ : α → γ) (hφ : MeasureTheory.MeasurePreserving φ μ ν) (hψ : MeasureTheory.MeasurePreserving ψ μ ρ) : |(U.pullback φ hφ).cutNormDiff (W.pullback ψ hψ) - (U'.pullback φ hφ).cutNormDiff (W'.pullback ψ hψ)| ≤ U.cutNormDiff U' + W.cutNormDiff W'

Generic Lipschitz stability of coupling cost under changing both marginal kernels: for two measure-preserving maps out of a common carrier — coupling projections are the intended instance — the pulled-back cut-norm difference moves by at most the sum of the two marginal cut-norm differences. Two triangle inequalities plus the cross-carrier contraction, once along each map.