OAI/Analysis/BiholderTransport/Volume/SpectralDeterminants.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakMTWTransport.expJacobian_eq_prod_singularValuesline 27 - lemma
OAI.WeakMTWTransport.expJacobian_comparison_of_singularValuesline 38 - lemma
OAI.WeakMTWTransport.uniform_radial_expJacobian_comparisonline 50 - lemma
OAI.WeakMTWTransport.WeakMTW.uniform_extended_expJacobian_comparisonline 64