OAI/Analysis/RCDHeat/WeightedMoment.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.RegularPointCoordinates.rpow_half_weight_bound line 17
  2. theorem OAI.RegularPointCoordinates.heatAt_exp_dist_integrable line 33
  3. theorem OAI.RegularPointCoordinates.heatMeasure_exp_dist_integrable line 51
  4. theorem OAI.RegularPointCoordinates.integrable_rnDeriv_half_of_exp_moment line 64
  5. theorem OAI.RegularPointCoordinates.geodesic_exp_dist_bound line 80
  6. theorem OAI.RegularPointCoordinates.optimalPlan_exp_dist_integrable line 100
  7. theorem OAI.RegularPointCoordinates.lintegral_rpow_tendsto_mass_half line 122
  8. theorem OAI.RegularPointCoordinates.rnDeriv_power_lintegral_eq_of_integrable line 142
  9. theorem OAI.RegularPointCoordinates.cd_plan_absolutelyContinuous_half line 154
  10. theorem OAI.RegularPointCoordinates.cd_plan_renyi_variation_bound_half line 252
  11. theorem OAI.RegularPointCoordinates.cd_plan_entropy_bound_half line 366