OAI/Analysis/RCDHeat/VolumeComparison2.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: VolumeComparison, RCDVolumeGrowth, RCDConservative, LipschitzProduct, RelaxedProduct, DaviesForm, DaviesWeight.

  1. theorem OAI.RegularPointCoordinates.hausdorff_normalization_pos_ne_top line 21
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.ball_upper_enlargement line 32
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.ball_upper line 82
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exponential_volume line 107
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.conservative line 147
  6. theorem OAI.RegularPointCoordinates.lipschitz_mul_constant_outside_compact line 169
  7. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.mul_lipschitz line 198
  8. theorem OAI.RegularPointCoordinates.mul_lipschitz_finiteEnergy line 253
  9. def OAI.RegularPointCoordinates.SobolevSpace.mulLipschitz line 266
  10. theorem OAI.RegularPointCoordinates.form_sub_smul line 275
  11. theorem OAI.RegularPointCoordinates.energyForm_lower_of_slope_variations line 287
  12. theorem OAI.RegularPointCoordinates.energyForm_weight_lower_inner line 317