OAI/Geometry/WeakHessian/HeatFlow/RealHeatRangeError.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakHessianFunctional.realHeat_range_error_applyline 46 - lemma
OAI.WeakHessianFunctional.realHeat_range_lipschitzline 53 - lemma
OAI.WeakHessianFunctional.ClosedQuadraticEnergy.heat_lipschitz_on_generatorline 76 - lemma
OAI.WeakHessianFunctional.ClosedQuadraticEnergy.heat_deriv_form_rightline 83