OAI/Analysis/RCDHeat/HeatEnergy.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: HeatEnergy, HeatSmoothing, HeatContraction, HeatFullGenerator.

  1. theorem OAI.RegularPointCoordinates.SobolevSpace.energy_eq_norms line 19
  2. theorem OAI.RegularPointCoordinates.SobolevSpace.energy_continuous line 25
  3. theorem OAI.RegularPointCoordinates.SobolevSpace.energy_hasDerivAt line 31
  4. theorem OAI.RegularPointCoordinates.heatCore_continuous line 47
  5. theorem OAI.RegularPointCoordinates.heatCore_double_hasDerivAt line 50
  6. theorem OAI.RegularPointCoordinates.heatCore_double_energy_hasDerivAt line 57
  7. theorem OAI.RegularPointCoordinates.heatCore_norm_sq_hasDerivAt line 68
  8. theorem OAI.RegularPointCoordinates.heatCore_double_energy_antitone line 77
  9. theorem OAI.RegularPointCoordinates.heatCore_double_energy_bound line 86
  10. theorem OAI.RegularPointCoordinates.SobolevSpace.energyLp_eq line 119
  11. theorem OAI.RegularPointCoordinates.heatAt_energy_bound line 125
  12. def OAI.RegularPointCoordinates.heatSobolev line 139
  13. theorem OAI.RegularPointCoordinates.heatSobolev_toLp line 142
  14. theorem OAI.RegularPointCoordinates.heatSobolev_energy_bound line 145
  15. theorem OAI.RegularPointCoordinates.heatSobolev_norm_bound line 151
  16. def OAI.RegularPointCoordinates.heatSobolevMap line 168
  17. theorem OAI.RegularPointCoordinates.heatSobolevMap_apply line 175
  18. theorem OAI.RegularPointCoordinates.SobolevSpace.resolventAt_one line 184
  19. theorem OAI.RegularPointCoordinates.SobolevSpace.resolvent_denseRange line 192
  20. theorem OAI.RegularPointCoordinates.SobolevSpace.resolventAt_one_denseRange line 207
  21. theorem OAI.RegularPointCoordinates.SobolevSpace.double_core_denseRange line 214
  22. theorem OAI.RegularPointCoordinates.heatSobolev_core line 221
  23. theorem OAI.RegularPointCoordinates.heatSobolev_energy_le line 226
  24. def OAI.RegularPointCoordinates.energyOperator line 246
  25. theorem OAI.RegularPointCoordinates.energyOperator_inner line 249
  26. theorem OAI.RegularPointCoordinates.energyOperator_norm_le line 255
  27. theorem OAI.RegularPointCoordinates.heatAt_inner line 277
  28. theorem OAI.RegularPointCoordinates.heatAt_add line 281
  29. def OAI.RegularPointCoordinates.heatGenerator line 289
  30. theorem OAI.RegularPointCoordinates.heatGenerator_inner line 293
  31. theorem OAI.RegularPointCoordinates.heatGenerator_core line 300
  32. theorem OAI.RegularPointCoordinates.heatGenerator_form line 316
  33. theorem OAI.RegularPointCoordinates.heatSobolev_weak_laplacian line 330
  34. theorem OAI.RegularPointCoordinates.heatSobolevMap_norm_le line 335
  35. theorem OAI.RegularPointCoordinates.heatGenerator_norm_le line 340