OAI/Geometry/WeakHessian/HeatFlow/HeatSymbol.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessianFunctional.heatSymbol line 40
  2. lemma OAI.WeakHessianFunctional.heatSymbol_zero line 43
  3. lemma OAI.WeakHessianFunctional.heatSymbol_continuous line 45
  4. lemma OAI.WeakHessianFunctional.heatSymbol_nonneg line 51
  5. lemma OAI.WeakHessianFunctional.heatSymbol_of_pos line 57
  6. lemma OAI.WeakHessianFunctional.heatSymbol_nonpos line 64
  7. lemma OAI.WeakHessianFunctional.heatSymbol_le_one line 68
  8. lemma OAI.WeakHessianFunctional.heatSymbol_add line 78
  9. lemma OAI.WeakHessianFunctional.heatSymbol_resolvent_error line 92
  10. def OAI.WeakHessianFunctional.resolventHeat line 109
  11. lemma OAI.WeakHessianFunctional.resolventHeat_zero line 111
  12. lemma OAI.WeakHessianFunctional.resolventHeat_add line 117
  13. lemma OAI.WeakHessianFunctional.resolvent_spectrum_bounds line 124
  14. lemma OAI.WeakHessianFunctional.resolventHeat_norm_le_one line 131
  15. lemma OAI.WeakHessianFunctional.resolventHeat_positive line 138
  16. lemma OAI.WeakHessianFunctional.resolventHeat_range_error line 143
  17. lemma OAI.WeakHessianFunctional.resolventHeat_range_error_apply line 158
  18. lemma OAI.WeakHessianFunctional.resolventHeat_contractive line 166
  19. lemma OAI.WeakHessianFunctional.resolventHeat_strong_zero line 175