OAI/Analysis/RCDHeat/SignedEntropySupport.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: SignedEntropySupport.

  1. theorem OAI.RegularPointCoordinates.sinh_le_mul_cosh_real line 14
  2. theorem OAI.RegularPointCoordinates.sinh_gaussian_derivative_sign line 35
  3. def OAI.RegularPointCoordinates.sharpSinhRatio line 55
  4. theorem OAI.RegularPointCoordinates.sharpSinhRatio_hasDerivAt line 57
  5. theorem OAI.RegularPointCoordinates.sharpSinhRatio_antitone line 67
  6. theorem OAI.RegularPointCoordinates.sinh_mul_sharp_gaussian_lower line 78
  7. theorem OAI.RegularPointCoordinates.sigma_gaussian_lower line 102
  8. theorem OAI.RegularPointCoordinates.tau_gaussian_lower line 146
  9. theorem OAI.RegularPointCoordinates.mul_cos_le_sin_real line 173
  10. theorem OAI.RegularPointCoordinates.sin_gaussian_derivative_sign line 192
  11. def OAI.RegularPointCoordinates.sharpSinRatio line 213
  12. theorem OAI.RegularPointCoordinates.sharpSinRatio_hasDerivAt line 215
  13. theorem OAI.RegularPointCoordinates.sharpSinRatio_antitone line 225
  14. theorem OAI.RegularPointCoordinates.sin_mul_sharp_gaussian_lower line 236
  15. theorem OAI.RegularPointCoordinates.sigma_signed_gaussian_lower line 261
  16. theorem OAI.RegularPointCoordinates.tau_signed_gaussian_lower line 290
  17. theorem OAI.RegularPointCoordinates.ennreal_rpow_le_one_add line 315
  18. theorem OAI.RegularPointCoordinates.ennreal_rpow_tendsto_one line 324
  19. theorem OAI.RegularPointCoordinates.lintegral_rpow_tendsto_mass line 335
  20. theorem OAI.RegularPointCoordinates.renyi_rnDeriv_tendsto_mass line 357
  21. theorem OAI.RegularPointCoordinates.ennreal_rpow_tendsto_zero line 370
  22. theorem OAI.RegularPointCoordinates.absolutelyContinuous_of_rnDeriv_mass_one line 381
  23. theorem OAI.RegularPointCoordinates.dimension_reciprocal_tendsto line 392
  24. theorem OAI.RegularPointCoordinates.gaussian_density_tendsto line 402
  25. theorem OAI.RegularPointCoordinates.ofReal_integral_le_lintegral_ofReal line 426
  26. theorem OAI.RegularPointCoordinates.tau_density_entropy_lower line 439