Gluing the right joint law before applying Minkowski

1. Strict near-optimal selection gives actual couplings \(\gamma_{12},\gamma_{23}\) with \[\begin{gathered}C(\gamma_{12})<r_{12},\\ C(\gamma_{23})<r_{23}.\end{gathered}\] These are consequences of the transport infimum and positive square-root order, not an assumption that the infimum is attained. A coupling of a probability marginal has total mass one, so both plans are probability measures.

2. Disintegrate the second plan with respect to its first coordinate. The finite standard-Borel conditional-kernel theorem supplies a Markov version \(\kappa(y,dz)\) with \[\gamma_{23}(dy,dz)=\mu_2(dy)\kappa(y,dz).\] Define \[\Gamma(d(x,y),dz)=\gamma_{12}(dx,dy)\kappa(y,dz).\] Markov normalization preserves its first pair marginal. Equality \(\gamma_{12}.\mathrm{snd}=\mu_2=\gamma_{23}.\mathrm{fst}\), kernel measurability and the disintegration identity preserve the second pair marginal. Conditional representatives need only have the correct \(\mu_2\)-almost-everywhere meaning; an unsupported pointwise conditional formula is not used.

3. Write \(\pi_{ij}\) for the measurable pair projections from the same triple space. The identities are \[\begin{gathered}(\pi_{12})_\#\Gamma=\gamma_{12},\\(\pi_{23})_\#\Gamma=\gamma_{23}.\end{gathered}\] Put \(\gamma_{13}=(\pi_{13})_\#\Gamma\). Composing measurable coordinate projections proves that its marginals are \(\mu_1,\mu_3\). The Borel norm and the product/projection measurability justify nonnegative pushforward integration; no subtraction of infinite integrals occurs.

4. For \(e_{ij}(x,y,z)=\|x_i-x_j\|\), all edge functions are measurable. Nonnegative pushforward integration gives \[\begin{gathered}\|e_{12}\|_{L^2(\Gamma)}=C(\gamma_{12}),\\\|e_{23}\|_{L^2(\Gamma)}=C(\gamma_{23}).\end{gathered}\] The endpoint identity is \[\|e_{13}\|_{L^2(\Gamma)}=C(\gamma_{13}).\] Pointwise \(e_{13}\le e_{12}+e_{23}\) and extended-nonnegative \(L^{2}\) Minkowski apply on this single law \(Γ\), not on two unrelated pair spaces.

5. Using the endpoint coupling to bound the infimum, then the preceding identities, yields \[\begin{aligned}W_2(\mu_1,\mu_3)&\le C(\gamma_{13})\\&\le C(\gamma_{12})+C(\gamma_{23})\\&<r_{12}+r_{23}.\end{aligned}\] The coefficient is exactly one on each cost. Strict extended-order addition handles the thresholds without an infinity-minus-infinity operation. No optimal plan, density or individual second-moment assumption is added.

6. For the shortcut audit, take \(E=\mathbb R\) and all three marginals equal to \(\frac12\delta_0+\frac12\delta_1\), with both adjacent plans diagonal. Their costs are zero. Under \(\Gamma'=\gamma_{12}\otimes\mu_3\), Y and Z are independent, so \[\begin{gathered}\mathbb P_{\Gamma'}(Y\ne Z)=\tfrac12,\\\|e_{23}\|_{L^2(\Gamma')}=1/\sqrt2.\end{gathered}\] Its second pair marginal is the independent product, not the diagonal \(\gamma_{23}\), and cannot have cost zero. This refutes the shortcut's cost identification, not the true Wasserstein inequality. Correct conditional gluing makes X=Y=Z in this example.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Measure.TransportGluing
import AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals
import Mathlib.Tactic

noncomputable section
open MeasureTheory
open scoped ENNReal
open AutoSamplingTheory.TechnicalLemmas.Measure
open AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore
open AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals
variable {E : Type*} [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
  [StandardBorelSpace E] [Nonempty E]

example
    (μ₁ μ₂ μ₃ : Measure E)
    [IsProbabilityMeasure μ₁] [IsProbabilityMeasure μ₂] [IsProbabilityMeasure μ₃]
    {r₁₂ r₂₃ : ℝ≥0∞}
    (hr₁₂ : WassersteinSpace.wassersteinDistance μ₁ μ₂ < r₁₂)
    (hr₂₃ : WassersteinSpace.wassersteinDistance μ₂ μ₃ < r₂₃) :
    WassersteinSpace.wassersteinDistance μ₁ μ₃ < r₁₂ + r₂₃ := by
  rcases
      WassersteinSpace.exists_isCoupling_sqrt_lintegral_lt_of_wassersteinDistance_lt
        μ₁ μ₂ hr₁₂ with
    ⟨γ₁₂, hγ₁₂, hcost₁₂⟩
  rcases
      WassersteinSpace.exists_isCoupling_sqrt_lintegral_lt_of_wassersteinDistance_lt
        μ₂ μ₃ hr₂₃ with
    ⟨γ₂₃, hγ₂₃, hcost₂₃⟩
  rcases TransportGluing.exists_gluing_of_isCoupling γ₁₂ γ₂₃ hγ₁₂ hγ₂₃ with
    ⟨γ₁₂₃, hfst, hmap₂₃⟩

  have hmap₁₂ : Measure.map (pair12 (E := E)) γ₁₂₃ = γ₁₂ := by
    change Measure.map Prod.fst γ₁₂₃ = γ₁₂
    exact hfst
  have hmap₂₃' : Measure.map (pair23 (E := E)) γ₁₂₃ = γ₂₃ := by
    change Measure.map (fun p : ((E × E) × E) => (p.1.2, p.2)) γ₁₂₃ = γ₂₃
    exact hmap₂₃

  have hpair₁₂ :
      Transport.IsCoupling (Measure.map (pair12 (E := E)) γ₁₂₃) μ₁ μ₂ := by
    rw [hmap₁₂]
    exact hγ₁₂
  have hpair₂₃ :
      Transport.IsCoupling (Measure.map (pair23 (E := E)) γ₁₂₃) μ₂ μ₃ := by
    rw [hmap₂₃']
    exact hγ₂₃
  have hpair₁₃ :
      Transport.IsCoupling (Measure.map (pair13 (E := E)) γ₁₂₃) μ₁ μ₃ :=
    isCoupling_map_pair13_of_pair12_pair23 γ₁₂₃ hpair₁₂ hpair₂₃

  have hedge₁₂ :
      l2Seminorm γ₁₂₃ (edgeLength12 (E := E)) =
        (∫⁻ z, WassersteinSpace.quadraticCost (E := E) z ∂γ₁₂) ^
          (1 / (2 : ℝ)) := by
    rw [l2Seminorm_edge12_eq_pairCost, hmap₁₂]
  have hedge₂₃ :
      l2Seminorm γ₁₂₃ (edgeLength23 (E := E)) =
        (∫⁻ z, WassersteinSpace.quadraticCost (E := E) z ∂γ₂₃) ^
          (1 / (2 : ℝ)) := by
    rw [l2Seminorm_edge23_eq_pairCost, hmap₂₃']
  have hendpoint :
      WassersteinSpace.wassersteinDistance μ₁ μ₃ ≤
        l2Seminorm γ₁₂₃ (edgeLength13 (E := E)) := by
    calc
      WassersteinSpace.wassersteinDistance μ₁ μ₃ ≤
          (∫⁻ z, WassersteinSpace.quadraticCost (E := E) z
            ∂Measure.map (pair13 (E := E)) γ₁₂₃) ^ (1 / (2 : ℝ)) :=
        WassersteinSpace.wassersteinDistance_le_sqrt_lintegral_of_isCoupling
          μ₁ μ₃ (Measure.map (pair13 (E := E)) γ₁₂₃) hpair₁₃
      _ = l2Seminorm γ₁₂₃ (edgeLength13 (E := E)) :=
        (l2Seminorm_edge13_eq_pairCost γ₁₂₃).symm

  calc
    WassersteinSpace.wassersteinDistance μ₁ μ₃ ≤
        l2Seminorm γ₁₂₃ (edgeLength13 (E := E)) := hendpoint
    _ ≤ l2Seminorm γ₁₂₃ (edgeLength12 (E := E)) +
          l2Seminorm γ₁₂₃ (edgeLength23 (E := E)) :=
      l2_edge_triangle γ₁₂₃
    _ = (∫⁻ z, WassersteinSpace.quadraticCost (E := E) z ∂γ₁₂) ^
          (1 / (2 : ℝ)) +
        (∫⁻ z, WassersteinSpace.quadraticCost (E := E) z ∂γ₂₃) ^
          (1 / (2 : ℝ)) := by rw [hedge₁₂, hedge₂₃]
    _ < r₁₂ + r₂₃ := ENNReal.add_lt_add hcost₁₂ hcost₂₃

1. Selects actual strictly near-optimal adjacent couplings and derives their probability interfaces without assuming attainment or individual finite second moments. (1 point)
2. Constructs the common-middle conditional gluing with measurable kernels and both pair marginals, respecting the almost-everywhere meaning of conditional versions. (1 point)
3. Uses measurable pushforward cost identities and extended \(L^{2}\) Minkowski on one triple law to obtain the endpoint coupling bound and exact strict sum. (1 point)
4. Gives the diagonal Bernoulli/independent-third-coordinate counterexample with discrepancy probability 1/2 and edge norm 1/√2, identifying a failed marginal/cost identity rather than claiming the true triangle inequality fails. (1 point)

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Measure.TransportGluing
import AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals
import Mathlib.Tactic

noncomputable section
open MeasureTheory
open scoped ENNReal
open AutoSamplingTheory.TechnicalLemmas.Measure
open AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore
open AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals
variable {E : Type*} [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
  [StandardBorelSpace E] [Nonempty E]

example
    (μ₁ μ₂ μ₃ : Measure E)
    [IsProbabilityMeasure μ₁] [IsProbabilityMeasure μ₂] [IsProbabilityMeasure μ₃]
    {r₁₂ r₂₃ : ℝ≥0∞}
    (hr₁₂ : WassersteinSpace.wassersteinDistance μ₁ μ₂ < r₁₂)
    (hr₂₃ : WassersteinSpace.wassersteinDistance μ₂ μ₃ < r₂₃) :
    WassersteinSpace.wassersteinDistance μ₁ μ₃ < r₁₂ + r₂₃ := by
  -- Replace this comment with your proof.

Download task template

The target is the actual strict-threshold composition theorem, not a new wrapper. Its module is not imported: only the original ancestor modules are allowed. Two near-optimal-selection calls produce concrete plans. exists_gluing_of_isCoupling produces one triple law and the two exact marginal identities. The reference explicitly adapts projection encodings, reconstructs the endpoint coupling and rewrites three \(L^{2}\) seminorm/cost bridges before calling l2_edge_triangle and ENNReal.add_lt_add. Its conclusion certifies the strict endpoint bound; the explanatory Bernoulli counterexample is not a separate Lean conclusion. The exact-threshold closure is a later consumer, not silently supplied here.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Measure.TransportGluing
import AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals
import Mathlib.Tactic

noncomputable section
open MeasureTheory
open scoped ENNReal
open AutoSamplingTheory.TechnicalLemmas.Measure
open AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCore
open AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginals
variable {E : Type*} [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
  [StandardBorelSpace E] [Nonempty E]

example
    (μ₁ μ₂ μ₃ : Measure E)
    [IsProbabilityMeasure μ₁] [IsProbabilityMeasure μ₂] [IsProbabilityMeasure μ₃]
    {r₁₂ r₂₃ : ℝ≥0∞}
    (hr₁₂ : WassersteinSpace.wassersteinDistance μ₁ μ₂ < r₁₂)
    (hr₂₃ : WassersteinSpace.wassersteinDistance μ₂ μ₃ < r₂₃) :
    WassersteinSpace.wassersteinDistance μ₁ μ₃ < r₁₂ + r₂₃ := by
  rcases
      WassersteinSpace.exists_isCoupling_sqrt_lintegral_lt_of_wassersteinDistance_lt
        μ₁ μ₂ hr₁₂ with
    ⟨γ₁₂, hγ₁₂, hcost₁₂⟩
  rcases
      WassersteinSpace.exists_isCoupling_sqrt_lintegral_lt_of_wassersteinDistance_lt
        μ₂ μ₃ hr₂₃ with
    ⟨γ₂₃, hγ₂₃, hcost₂₃⟩
  rcases TransportGluing.exists_gluing_of_isCoupling γ₁₂ γ₂₃ hγ₁₂ hγ₂₃ with
    ⟨γ₁₂₃, hfst, hmap₂₃⟩

  have hmap₁₂ : Measure.map (pair12 (E := E)) γ₁₂₃ = γ₁₂ := by
    change Measure.map Prod.fst γ₁₂₃ = γ₁₂
    exact hfst
  have hmap₂₃' : Measure.map (pair23 (E := E)) γ₁₂₃ = γ₂₃ := by
    change Measure.map (fun p : ((E × E) × E) => (p.1.2, p.2)) γ₁₂₃ = γ₂₃
    exact hmap₂₃

  have hpair₁₂ :
      Transport.IsCoupling (Measure.map (pair12 (E := E)) γ₁₂₃) μ₁ μ₂ := by
    rw [hmap₁₂]
    exact hγ₁₂
  have hpair₂₃ :
      Transport.IsCoupling (Measure.map (pair23 (E := E)) γ₁₂₃) μ₂ μ₃ := by
    rw [hmap₂₃']
    exact hγ₂₃
  have hpair₁₃ :
      Transport.IsCoupling (Measure.map (pair13 (E := E)) γ₁₂₃) μ₁ μ₃ :=
    isCoupling_map_pair13_of_pair12_pair23 γ₁₂₃ hpair₁₂ hpair₂₃

  have hedge₁₂ :
      l2Seminorm γ₁₂₃ (edgeLength12 (E := E)) =
        (∫⁻ z, WassersteinSpace.quadraticCost (E := E) z ∂γ₁₂) ^
          (1 / (2 : ℝ)) := by
    rw [l2Seminorm_edge12_eq_pairCost, hmap₁₂]
  have hedge₂₃ :
      l2Seminorm γ₁₂₃ (edgeLength23 (E := E)) =
        (∫⁻ z, WassersteinSpace.quadraticCost (E := E) z ∂γ₂₃) ^
          (1 / (2 : ℝ)) := by
    rw [l2Seminorm_edge23_eq_pairCost, hmap₂₃']
  have hendpoint :
      WassersteinSpace.wassersteinDistance μ₁ μ₃ ≤
        l2Seminorm γ₁₂₃ (edgeLength13 (E := E)) := by
    calc
      WassersteinSpace.wassersteinDistance μ₁ μ₃ ≤
          (∫⁻ z, WassersteinSpace.quadraticCost (E := E) z
            ∂Measure.map (pair13 (E := E)) γ₁₂₃) ^ (1 / (2 : ℝ)) :=
        WassersteinSpace.wassersteinDistance_le_sqrt_lintegral_of_isCoupling
          μ₁ μ₃ (Measure.map (pair13 (E := E)) γ₁₂₃) hpair₁₃
      _ = l2Seminorm γ₁₂₃ (edgeLength13 (E := E)) :=
        (l2Seminorm_edge13_eq_pairCost γ₁₂₃).symm

  calc
    WassersteinSpace.wassersteinDistance μ₁ μ₃ ≤
        l2Seminorm γ₁₂₃ (edgeLength13 (E := E)) := hendpoint
    _ ≤ l2Seminorm γ₁₂₃ (edgeLength12 (E := E)) +
          l2Seminorm γ₁₂₃ (edgeLength23 (E := E)) :=
      l2_edge_triangle γ₁₂₃
    _ = (∫⁻ z, WassersteinSpace.quadraticCost (E := E) z ∂γ₁₂) ^
          (1 / (2 : ℝ)) +
        (∫⁻ z, WassersteinSpace.quadraticCost (E := E) z ∂γ₂₃) ^
          (1 / (2 : ℝ)) := by rw [hedge₁₂, hedge₂₃]
    _ < r₁₂ + r₂₃ := ENNReal.add_lt_add hcost₁₂ hcost₂₃

Download runnable reference