OAI/Geometry/WeakHessian/Transport/KineticAction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessianTransport.lsc_real_lintegral_le_liminf line 39
2. lemma OAI.WeakHessianTransport.lsc_lintegral_le_liminf line 52
3. lemma OAI.WeakHessianTransport.lsc_lintegral_le_liminf_of_tendsto line 87
4. def OAI.WeakHessian.kineticAction line 98
5. lemma OAI.WeakHessian.lowerSemicontinuous_kineticAction line 100
6. lemma OAI.WeakHessian.kineticAction_finite_controlNorm line 104
7. lemma OAI.WeakHessian.speed_energy_le_kineticAction line 110
8. lemma OAI.WeakHessian.kineticAction_finite_isAC2 line 131
9. lemma OAI.WeakHessian.probability_isTight_of_action line 134
10. lemma OAI.WeakHessian.exists_action_limit line 180