OAI/Analysis/RCDHeat/FisherLimit.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: FisherLimit, EntropyDissipation, RCDHeatDissipation, PositiveTail, ExponentialTail.

  1. def OAI.RegularPointCoordinates.entropyScale line 23
  2. theorem OAI.RegularPointCoordinates.entropyScale_pos line 24
  3. theorem OAI.RegularPointCoordinates.entropyScale_antitone line 25
  4. theorem OAI.RegularPointCoordinates.entropyScale_tendsto line 29
  5. theorem OAI.RegularPointCoordinates.regularizedReciprocal_antitone line 33
  6. theorem OAI.RegularPointCoordinates.regularizedReciprocal_sq_tendsto line 39
  7. theorem OAI.RegularPointCoordinates.regularizedFisher_integrable line 62
  8. def OAI.RegularPointCoordinates.fisherInformation line 78
  9. theorem OAI.RegularPointCoordinates.regularizedFisher_monotone line 81
  10. theorem OAI.RegularPointCoordinates.fisherInformation_eq_integral line 93
  11. theorem OAI.RegularPointCoordinates.heatAt_entropy_mono_of_finite line 121
  12. theorem OAI.RegularPointCoordinates.regularizedFisher_intervalIntegrable line 138
  13. theorem OAI.RegularPointCoordinates.heatAt_entropy_dissipation_of_finite line 147
  14. theorem OAI.RegularPointCoordinates.heatAt_entropy_dissipation line 188
  15. theorem OAI.RegularPointCoordinates.heatAt_fisher_time_finite line 202
  16. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_entropy_dissipation line 211
  17. def OAI.RegularPointCoordinates.positiveTail line 253
  18. theorem OAI.RegularPointCoordinates.positiveTail_pos line 255
  19. theorem OAI.RegularPointCoordinates.exp_neg_dist_lipschitz line 258
  20. theorem OAI.RegularPointCoordinates.positiveTail_lipschitz line 278
  21. theorem OAI.RegularPointCoordinates.lipschitz_log_one_add line 282
  22. theorem OAI.RegularPointCoordinates.positiveTail_log_lipschitz line 302
  23. theorem OAI.RegularPointCoordinates.localSlope_exp_neg_dist line 348
  24. theorem OAI.RegularPointCoordinates.exp_neg_dist_memLp_two line 362
  25. theorem OAI.RegularPointCoordinates.exp_neg_dist_slopeMajorant line 373
  26. theorem OAI.RegularPointCoordinates.integrable_dist_pow_mul_exp_of_le line 384