OAI/Analysis/RCDHeat/HeatMoments.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: HeatMoments, HeatEntropy, HeatLaw, EntropyNormalization, EntropyLimit.

  1. theorem OAI.RegularPointCoordinates.heatAt_exponential_square_integrable line 25
  2. theorem OAI.RegularPointCoordinates.exponential_moment_young line 37
  3. theorem OAI.RegularPointCoordinates.heatAt_dist_pow_integrable line 58
  4. theorem OAI.RegularPointCoordinates.heatAt_finiteSecondMoment line 71
  5. theorem OAI.RegularPointCoordinates.entropy_radial_lower line 96
  6. theorem OAI.RegularPointCoordinates.entropy_radial_abs_bound line 116
  7. theorem OAI.RegularPointCoordinates.heatAt_entropy_integrable line 128
  8. def OAI.RegularPointCoordinates.heatMeasure line 146
  9. theorem OAI.RegularPointCoordinates.heatMeasure_absolutelyContinuous line 149
  10. theorem OAI.RegularPointCoordinates.heatMeasure_probability line 153
  11. theorem OAI.RegularPointCoordinates.heatMeasure_rnDeriv line 164
  12. theorem OAI.RegularPointCoordinates.lp_integrable_of_bounded_support line 177
  13. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_law line 187
  14. theorem OAI.RegularPointCoordinates.regularizedReciprocal_sqrt line 220
  15. theorem OAI.RegularPointCoordinates.regularizedEntropy_formula line 227
  16. def OAI.RegularPointCoordinates.normalizedEntropy line 247
  17. theorem OAI.RegularPointCoordinates.normalizedEntropy_zero line 250
  18. theorem OAI.RegularPointCoordinates.normalizedEntropy_formula line 253
  19. theorem OAI.RegularPointCoordinates.entropy_le_normalizedEntropy line 266
  20. theorem OAI.RegularPointCoordinates.normalizedEntropy_le_sq_add line 278
  21. theorem OAI.RegularPointCoordinates.normalizedEntropy_abs_bound line 292
  22. theorem OAI.RegularPointCoordinates.normalizedEntropy_tendsto line 301
  23. theorem OAI.RegularPointCoordinates.normalizedEntropy_continuous line 324
  24. theorem OAI.RegularPointCoordinates.normalizedEntropy_integrable line 332
  25. theorem OAI.RegularPointCoordinates.integral_normalizedEntropy line 338
  26. theorem OAI.RegularPointCoordinates.integral_normalizedEntropy_tendsto line 352
  27. theorem OAI.RegularPointCoordinates.integral_normalizedEntropy_sub_tendsto line 370