import AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementJacobianMatrixLogDet

#check AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementJacobianMatrixLogDet.det_affineIdentityMatrix_eq_prod_eigenvalues
#check AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementJacobianMatrixLogDet.spectrumLogDet_affineIdentity_eigenvalues_eq_log_det
#check AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementJacobianMatrixLogDet.neg_log_det_affineIdentity_le