OAI/Geometry/WeakHessian/LocalBounds/ReLp.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.scale_lt_top_iff line 50
  2. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.scale line 62
  3. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.scale_form line 75
  4. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.scale_isFormGenerator_iff line 86
  5. lemma OAI.WeakHessianFunctional.ClosedQuadraticEnergy.scaled_resolvent_iff line 105
  6. def OAI.WeakHessianFunctional.reLp line 118
  7. def OAI.WeakHessianFunctional.imLp line 119
  8. def OAI.WeakHessianFunctional.ofRealLp line 120
  9. lemma OAI.WeakHessianFunctional.reLp_ae line 122
  10. lemma OAI.WeakHessianFunctional.imLp_ae line 124
  11. lemma OAI.WeakHessianFunctional.ofRealLp_ae line 126
  12. lemma OAI.WeakHessianFunctional.re_ofRealLp line 129
  13. lemma OAI.WeakHessianFunctional.im_ofRealLp line 133
  14. lemma OAI.WeakHessianFunctional.reLp_smul_complex line 139
  15. lemma OAI.WeakHessianFunctional.imLp_smul_complex line 147
  16. lemma OAI.WeakHessianFunctional.ofRealLp_re_add_im line 155
  17. lemma OAI.WeakHessianFunctional.ofRealLp_inner line 164
  18. lemma OAI.WeakHessianFunctional.complexLp_inner line 171
  19. def OAI.WeakHessianFunctional.complexifyReal line 180
  20. lemma OAI.WeakHessianFunctional.complexifyReal_apply line 184
  21. lemma OAI.WeakHessianFunctional.complexLp_ext line 188
  22. lemma OAI.WeakHessianFunctional.re_complexifyReal line 192
  23. lemma OAI.WeakHessianFunctional.im_complexifyReal line 196
  24. lemma OAI.WeakHessianFunctional.complexifyReal_smul line 200
  25. def OAI.WeakHessianFunctional.complexify line 206
  26. lemma OAI.WeakHessianFunctional.re_complexify line 212
  27. lemma OAI.WeakHessianFunctional.im_complexify line 214
  28. lemma OAI.WeakHessianFunctional.complexify_symmetric line 217
  29. lemma OAI.WeakHessianFunctional.complexify_injective line 225
  30. lemma OAI.WeakHessianFunctional.complexify_positive line 234
  31. lemma OAI.WeakHessianFunctional.complexify_sub line 245
  32. lemma OAI.WeakHessianFunctional.complexify_one line 250
  33. lemma OAI.WeakHessianFunctional.complexify_range_dense line 254
  34. lemma OAI.WeakHessianFunctional.ofRealLp_of_im_zero line 269
  35. def OAI.WeakHessianFunctional.realOperators line 278
  36. lemma OAI.WeakHessianFunctional.realOperators_closed line 311
  37. lemma OAI.WeakHessianFunctional.complexify_mem_realOperators line 320
  38. lemma OAI.WeakHessianFunctional.cfc_preserves_real line 325
  39. def OAI.WeakHessianFunctional.realCfc line 331
  40. lemma OAI.WeakHessianFunctional.ofReal_realCfc line 334