OAI/Analysis/BiholderTransport/Regularity/PullbackDet.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakMTWTransport.abs_det_hessian_pullbackline 18 - lemma
OAI.WeakMTWTransport.symmetric_det_posline 39 - lemma
OAI.WeakMTWTransport.det_positive_hessian_pullbackline 47