OAI/Analysis/BiholderTransport/LinearAlgebra/DividedHessian.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakMTWTransport.doubleNormalCost_self_contDiffAtline 46 - def
OAI.WeakMTWTransport.radialCrossingValueline 63