OAI/Geometry/WeakHessian/HeatFlow/HeatInverseSymbol.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessianFunctional.resolventHeat_second_error line 46
  2. lemma OAI.WeakHessianFunctional.resolventHeat_second_error_apply line 67
  3. lemma OAI.WeakHessianFunctional.resolventHeat_slope_range2_error line 75
  4. lemma OAI.WeakHessianFunctional.resolventHeat_deriv_range2_zero line 87
  5. lemma OAI.WeakHessianFunctional.positive_contraction_norm line 103
  6. lemma OAI.WeakHessianFunctional.resolventHeat_slope_range_contractive line 109
  7. lemma OAI.WeakHessianFunctional.resolvent_minus_id_bound line 125
  8. lemma OAI.WeakHessianFunctional.resolventHeat_slope_range_zero line 137
  9. lemma OAI.WeakHessianFunctional.resolventHeat_deriv_range_zero line 164
  10. def OAI.WeakHessianFunctional.heatInverseSymbol line 176
  11. lemma OAI.WeakHessianFunctional.heatInverseSymbol_continuous line 179
  12. lemma OAI.WeakHessianFunctional.heatInverseSymbol_mul line 184
  13. lemma OAI.WeakHessianFunctional.heatSymbol_maps_range line 191
  14. lemma OAI.WeakHessianFunctional.resolventHeat_eq_resolvent_mul line 194
  15. lemma OAI.WeakHessianFunctional.resolventHeat_mem_range line 205
  16. lemma OAI.WeakHessianFunctional.resolventHeat_commute_resolvent line 212
  17. lemma OAI.WeakHessianFunctional.resolventHeat_resolvent line 218