OAI/Geometry/WeakHessian/HeatFlow/PlanHeatEntropy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.compactHopfDualBound line 21
2. lemma OAI.WeakHessian.compact_dual_of_entropy_actions line 26
3. def OAI.WeakHessian.backwardsHeatTime line 64
4. lemma OAI.WeakHessian.backwardsHeatTime_pos line 66
5. lemma OAI.WeakHessian.backwardsHeatTime_hasDerivAt line 71
6. lemma OAI.WeakHessian.cheegerHeat_plan_entropy_dual line 79