AutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalRealMinimality

- A quadratic-optimal coupling minimizes the ordinary real squared-displacement integral among all couplings with the same marginals, whenever the compared real costs are integrable.

theorem integral_norm_sq_le_of_quadraticOptimal
    {gamma xi : Measure (E × E)} {mu0 mu1 : Measure E}
    (hgamma : IsQuadraticOptimalCoupling gamma mu0 mu1)
    (hxi : Transport.IsCoupling xi mu0 mu1)
    (hgammaInt : Integrable (fun z : E × E => ‖z.1 - z.2‖ ^ 2) gamma)
    (hxiInt : Integrable (fun z : E × E => ‖z.1 - z.2‖ ^ 2) xi) :
    (∫ z, ‖z.1 - z.2‖ ^ 2 ∂gamma) ≤
      ∫ z, ‖z.1 - z.2‖ ^ 2 ∂xi := by
  have hENN :
      (∫⁻ z, WassersteinSpace.quadraticCost (E := E) z ∂gamma) ≤
        ∫⁻ z, WassersteinSpace.quadraticCost (E := E) z ∂xi := by
    rw [hgamma.2]
    exact Transport.transportCost_le_lintegral_of_isCoupling
      (WassersteinSpace.quadraticCost (E := E)) mu0 mu1 xi hxi
  have hOfReal :
      ENNReal.ofReal (∫ z, ‖z.1 - z.2‖ ^ 2 ∂gamma) ≤
        ENNReal.ofReal (∫ z, ‖z.1 - z.2‖ ^ 2 ∂xi) := by
    rw [ofReal_integral_norm_sq_eq_lintegral_quadraticCost gamma hgammaInt,
      ofReal_integral_norm_sq_eq_lintegral_quadraticCost xi hxiInt]
    exact hENN
  have hxiNonneg : 0 ≤ ∫ z, ‖z.1 - z.2‖ ^ 2 ∂xi :=
    integral_nonneg fun z => sq_nonneg ‖z.1 - z.2‖
  exact (ENNReal.ofReal_le_ofReal_iff hxiNonneg).mp hOfReal

end

end QuadraticOptimalRealMinimality
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalRealMinimality.lean:30published source at 0e31a3cda412