import AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitorQuadraticCost

#check AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitorQuadraticCost.integrable_ambient_of_remainder_removed
#check AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitorQuadraticCost.integrable_replacementCompetitor
#check AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitorQuadraticCost.integral_replacementCompetitor_lt_ambient