OAI/Geometry/WeakHessian/Sobolev/AeEndpointGlobal.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakHessian.IsLocalWeakUpperGradient.ae_endpoint_le_globalline 49 - lemma
OAI.WeakHessian.IsLocalWeakUpperGradient.integrated_globalline 89