OAI/Analysis/RCDHeat/DimensionalEntropy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: DimensionalEntropy, DimensionalEntropySubsegment, EntropyEndpoints, DiscreteDimensionalEntropy, MidpointGrid, LogCoshLimit.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_plan_dimensional_entropy_midpoint line 21
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_plan_dimensional_entropy_submidpoint line 96
  3. lemma OAI.RegularPointCoordinates.NoncollapsedRCD.entropy_compressed_plan_continuousAt_one line 147
  4. lemma OAI.RegularPointCoordinates.sum_second_difference line 193
  5. lemma OAI.RegularPointCoordinates.sum_centered_difference line 202
  6. lemma OAI.RegularPointCoordinates.sum_log_cosh_ge line 211
  7. lemma OAI.RegularPointCoordinates.dimensional_midpoint_discrete_sum line 224
  8. lemma OAI.RegularPointCoordinates.dimensional_midpoint_grid line 258
  9. lemma OAI.RegularPointCoordinates.tendsto_log_cosh_div_sq line 309
  10. def OAI.RegularPointCoordinates.logCoshRatio line 326
  11. lemma OAI.RegularPointCoordinates.continuousAt_logCoshRatio_zero line 328
  12. lemma OAI.RegularPointCoordinates.log_cosh_eq_sq_mul_ratio line 338
  13. lemma OAI.RegularPointCoordinates.dimensional_log_cosh_scaled_limit line 344