OAI/Geometry/WeakHessian/Calculus/IntegralHopfInitial.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakHessianTransport.integrable_density_slopeApprox_sqline 19 - lemma
OAI.WeakHessianTransport.tendsto_integral_slopeApproxline 30 - lemma
OAI.WeakHessianTransport.integral_hopf_initial_eventually_ltline 47