OAI/Geometry/WeakHessian/Geodesics/Join.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.CellMidpoint.exists_join line 58
2. def OAI.WeakHessian.CellMidpoint.join line 94
3. lemma OAI.WeakHessian.CellMidpoint.join_half line 98
4. lemma OAI.WeakHessian.CellMidpoint.join_right line 103
5. lemma OAI.WeakHessian.CellMidpoint.left_energy line 107
6. lemma OAI.WeakHessian.CellMidpoint.right_energy line 115
7. def OAI.WeakHessian.CDEnvironment.build line 128
8. lemma OAI.WeakHessian.CDEnvironment.build_half line 134
9. lemma OAI.WeakHessian.CDEnvironment.build_right line 139
10. lemma OAI.WeakHessian.CDEnvironment.build_stable line 144
11. lemma OAI.WeakHessian.CDEnvironment.build_dominated line 164
12. lemma OAI.WeakHessian.CDEnvironment.build_finite_entropy line 181
13. lemma OAI.WeakHessian.CDEnvironment.entropy_chord_half line 194
14. lemma OAI.WeakHessian.CDEnvironment.entropy_chord_right line 203
15. lemma OAI.WeakHessian.CDEnvironment.build_entropy_bound line 212