OAI/Analysis/RCDHeat/ResolventFamily.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: ResolventFamily, Yosida, BoundedSemigroup.

  1. theorem OAI.RegularPointCoordinates.energyForm_sub_left line 19
  2. def OAI.RegularPointCoordinates.resolventLp line 25
  3. theorem OAI.RegularPointCoordinates.resolventLp_apply line 28
  4. theorem OAI.RegularPointCoordinates.resolventLp_norm_le line 32
  5. theorem OAI.RegularPointCoordinates.resolventLp_inner line 37
  6. theorem OAI.RegularPointCoordinates.resolventLp_selfAdjoint line 50
  7. theorem OAI.RegularPointCoordinates.resolventLp_inner_nonneg line 60
  8. theorem OAI.RegularPointCoordinates.resolventLp_sub_identity_inner_nonneg line 69
  9. theorem OAI.RegularPointCoordinates.SobolevSpace.resolventAt_identity line 78
  10. theorem OAI.RegularPointCoordinates.resolventLp_identity line 95
  11. theorem OAI.RegularPointCoordinates.resolventLp_commute line 105
  12. theorem OAI.RegularPointCoordinates.resolventLp_error_energy line 116
  13. def OAI.RegularPointCoordinates.yosida line 134
  14. theorem OAI.RegularPointCoordinates.yosida_smul line 137
  15. theorem OAI.RegularPointCoordinates.yosida_nonneg line 141
  16. theorem OAI.RegularPointCoordinates.yosida_commute line 146
  17. theorem OAI.RegularPointCoordinates.yosida_resolvent_one line 159
  18. theorem OAI.RegularPointCoordinates.yosida_difference_on_core line 175
  19. theorem OAI.RegularPointCoordinates.resolventLp_sub_eq_yosida line 185
  20. theorem OAI.RegularPointCoordinates.yosida_difference_on_core_eq line 197
  21. theorem OAI.RegularPointCoordinates.yosida_difference_on_core_norm_le line 216
  22. theorem OAI.RegularPointCoordinates.resolventLp_eq_zero_iff line 244
  23. theorem OAI.RegularPointCoordinates.resolventLp_injective line 258
  24. theorem OAI.RegularPointCoordinates.resolventLp_denseRange line 265
  25. theorem OAI.RegularPointCoordinates.resolventLp_sq_denseRange line 279
  26. def OAI.RegularPointCoordinates.expNeg line 289
  27. theorem OAI.RegularPointCoordinates.expNeg_zero line 293
  28. theorem OAI.RegularPointCoordinates.expNeg_add line 296
  29. theorem OAI.RegularPointCoordinates.expNeg_hasDerivAt line 302
  30. theorem OAI.RegularPointCoordinates.expNeg_apply_hasDerivAt line 306
  31. theorem OAI.RegularPointCoordinates.expNeg_norm_apply_le line 311
  32. theorem OAI.RegularPointCoordinates.expNeg_norm_le line 325
  33. theorem OAI.RegularPointCoordinates.commute_expNeg line 333
  34. theorem OAI.RegularPointCoordinates.expNeg_difference_bound line 337