OAI/Geometry/WeakHessian/HeatFlow/RealHeat.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessianFunctional.ofRealLp_norm line 51
2. lemma OAI.WeakHessianFunctional.ofRealLp_injective line 58
3. lemma OAI.WeakHessianFunctional.complexify_le_one line 62
4. def OAI.WeakHessianFunctional.realHeat line 66
5. lemma OAI.WeakHessianFunctional.ofReal_realHeat line 69
6. lemma OAI.WeakHessianFunctional.realHeat_zero line 73
7. lemma OAI.WeakHessianFunctional.realHeat_add line 80
8. lemma OAI.WeakHessianFunctional.realHeat_contractive line 88
9. lemma OAI.WeakHessianFunctional.realHeat_strong_zero line 95
10. lemma OAI.WeakHessianFunctional.realHeat_symmetric line 103