OAI/Analysis/RCDHeat/GeodesicCauchy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: GeodesicCauchy, FullCDHWI, FullCDDescent, LogDensitySlope, SqrtDensityDescent, SquareDensityLaws, NormalizedTail.

  1. theorem OAI.RegularPointCoordinates.geodesic_slope_integral_cauchy line 18
  2. theorem OAI.RegularPointCoordinates.geodesic_dist_integrable_of_sq line 41
  3. theorem OAI.RegularPointCoordinates.FullCD.exists_HWI_exp_plan line 57
  4. theorem OAI.RegularPointCoordinates.FullCD.entropy_descent_le_coupling line 99
  5. theorem OAI.RegularPointCoordinates.localSlope_log_sq_weighted_le line 155
  6. theorem OAI.RegularPointCoordinates.log_sq_slope_integral_le line 179
  7. theorem OAI.RegularPointCoordinates.log_sq_majorant_sqrt_le line 203
  8. theorem OAI.RegularPointCoordinates.FullCD.sqrt_density_descent line 227
  9. theorem OAI.RegularPointCoordinates.squareDensity_probability line 275
  10. theorem OAI.RegularPointCoordinates.squareDensity_integrable_iff line 281
  11. theorem OAI.RegularPointCoordinates.squareDensity_entropy line 288
  12. theorem OAI.RegularPointCoordinates.exists_normalized_exponential_sqrt line 305