OAI/Geometry/WeakHessian/LocalBounds/Domain.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessianFunctional.ClosedQuadraticEnergy.domain line 32
  2. def OAI.WeakHessianFunctional.ClosedQuadraticEnergy.realEnergy line 42
  3. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.realEnergy_quadratic line 44
  4. def OAI.WeakHessianFunctional.ClosedQuadraticEnergy.form line 60
  5. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.form_apply line 63
  6. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.form_comm line 66
  7. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.form_self line 69
  8. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.realEnergy_add line 72
  9. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.proximal_expansion line 76
  10. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.minimizer_iff_euler line 96
  11. def OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent line 131
  12. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_minimizes line 134
  13. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_finite line 138
  14. def OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolventDomain line 143
  15. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_euler line 146
  16. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_add line 150
  17. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_smul line 165
  18. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_zero line 179
  19. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_firm line 182
  20. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_nonexpansive line 202
  21. def OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolventLinear line 208
  22. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.resolvent_symmetric line 217