OAI/Analysis/RCDHeat/WeightedRenyi.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.RegularPointCoordinates.density_power_hasDerivAt line 17
  2. theorem OAI.RegularPointCoordinates.density_power_secant_lower line 28
  3. theorem OAI.RegularPointCoordinates.entropy_density_lower line 46
  4. theorem OAI.RegularPointCoordinates.density_power_secant_tendsto line 56
  5. theorem OAI.RegularPointCoordinates.integrable_of_nonneg_fatou_bound line 72
  6. theorem OAI.RegularPointCoordinates.integrable_density_power line 104
  7. theorem OAI.RegularPointCoordinates.entropy_le_of_renyi_variation_bound line 120
  8. theorem OAI.RegularPointCoordinates.entropy_le_of_renyi_variation_bound_on_support line 170
  9. theorem OAI.RegularPointCoordinates.density_power_secant_sqrt_lower line 196
  10. theorem OAI.RegularPointCoordinates.density_power_le_sqrt_add line 217
  11. theorem OAI.RegularPointCoordinates.integrable_density_power_of_sqrt line 225
  12. theorem OAI.RegularPointCoordinates.entropy_le_of_renyi_variation_bound_sqrt line 236