AutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalMapUniqueness

- A uniqueness principle for quadratic-optimal couplings with fixed marginals. This interface is intentionally proposition-level: any later Brenier uniqueness theorem can discharge it without the map layer depending on how that theorem was proved.

def HasUniqueQuadraticOptimalCoupling (mu nu : Measure E) : Prop :=
  ∀ ⦃gamma₀ gamma₁ : Measure (E × E)⦄,
    IsQuadraticOptimalCoupling gamma₀ mu nu →
    IsQuadraticOptimalCoupling gamma₁ mu nu →
    gamma₀ = gamma₁

/-- If the quadratic-optimal coupling between `mu` and `nu` is unique, then any
two quadratic-optimal transport maps are equal `mu`-almost everywhere. -/

AutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalMapUniqueness.lean:50published source at 0e31a3cda412

- If the quadratic-optimal coupling between `mu` and `nu` is unique, then any two quadratic-optimal transport maps are equal `mu`-almost everywhere.

theorem ae_eq_of_quadraticOptimalMap_of_uniqueCoupling
    {T S : E → E} {mu nu : Measure E}
    (hT : IsQuadraticOptimalMap T mu nu)
    (hS : IsQuadraticOptimalMap S mu nu)
    (hUnique : HasUniqueQuadraticOptimalCoupling mu nu) :
    T =ᵐ[mu] S := by
  apply ae_eq_of_graphCoupling_eq hT.1 hS.1
  exact hUnique hT.2.2 hS.2.2

/-- The same bridge with the coupling-uniqueness hypothesis written directly,
useful when a consumer already has a theorem rather than the named predicate. -/

AutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalMapUniqueness.lean:58published source at 0e31a3cda412

- The same bridge with the coupling-uniqueness hypothesis written directly, useful when a consumer already has a theorem rather than the named predicate.

theorem ae_eq_of_quadraticOptimalMap_of_forall_optimal_eq
    {T S : E → E} {mu nu : Measure E}
    (hT : IsQuadraticOptimalMap T mu nu)
    (hS : IsQuadraticOptimalMap S mu nu)
    (hUnique : ∀ ⦃gamma₀ gamma₁ : Measure (E × E)⦄,
      IsQuadraticOptimalCoupling gamma₀ mu nu →
      IsQuadraticOptimalCoupling gamma₁ mu nu →
      gamma₀ = gamma₁) :
    T =ᵐ[mu] S :=
  ae_eq_of_quadraticOptimalMap_of_uniqueCoupling hT hS hUnique

end

end QuadraticOptimalMapUniqueness
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalMapUniqueness.lean:69published source at 0e31a3cda412