import AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementRealQuadraticCost

#check AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementRealQuadraticCost.ofReal_integral_norm_sq_eq_lintegral_quadraticCost
#check AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementRealQuadraticCost.ofReal_integral_norm_sq_eq_wassersteinDistance_sq_of_optimal
#check AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementRealQuadraticCost.integral_norm_sq_eq_wassersteinDistance_sq_toReal_of_optimal