OAI/Geometry/WeakHessian/LocalBounds/ClosedQuadraticEnergy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.WeakHessianFunctional.ClosedQuadraticEnergy line 27
2. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.add_lt_top line 37
3. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.sub_lt_top line 43
4. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.midpoint_lt_top line 49
5. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.midpoint_le line 54
6. def OAI.WeakHessianFunctional.proximalFunctional line 65
7. lemma OAI.WeakHessianFunctional.proximalFunctional_lt_top line 69
8. lemma OAI.WeakHessianFunctional.proximalFunctional_toReal line 75
9. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.proximal_midpoint line 80
10. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.lowerSemicontinuous_proximal line 96
11. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.exists_minimizer line 101
12. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.minimizer_unique line 155
13. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.existsUnique_minimizer line 175