OAI/Geometry/WeakHessian/HeatFlow/ScaledResolventCfc.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakHessianFunctional.ClosedQuadraticEnergy.scaled_resolvent_cfcline 46 - lemma
OAI.WeakHessianFunctional.ClosedQuadraticEnergy.euler_tendsto_heatline 53 - lemma
OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_normal_fixedline 64 - lemma
OAI.WeakHessianFunctional.ClosedQuadraticEnergy.heat_normal_fixedline 79