OAI/Analysis/BiholderTransport/Coordinates/RadialFactor.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakMTWTransport.normal_log_fderiv_exp_normline 27 - lemma
OAI.WeakMTWTransport.normalHessian_radial_derivative_factorline 48