OAI/Geometry/WeakHessian/HeatFlow/FormGenerator.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_injective line 35
2. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_range_dense line 52
3. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_positive line 67
4. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_le_one line 75
5. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_norm_le_one line 90
6. def OAI.WeakHessianFunctional.ClosedQuadraticEnergy.IsFormGenerator line 96
7. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.isFormGenerator_resolvent line 100
8. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.isFormGenerator_iff line 108
9. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.formGenerator_unique line 124
10. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.formGenerator_add line 130
11. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.formGenerator_smul line 138
12. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.formGenerator_sub line 143
13. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.formGenerator_energy line 150
14. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.formGenerator_energy_bound line 156
15. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.formGenerator_closed line 163