import AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementConvexPotentialSupport

#check AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementConvexPotentialSupport.isSupportingField_of_convexOn_univ_hasFDerivAt_inner
#check AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementConvexPotentialSupport.isMonotoneMap_of_convexOn_univ_hasFDerivAt_inner
#check AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementConvexPotentialSupport.injective_affineDisplacementMap_of_convexOn_univ_hasFDerivAt_inner