OAI/Analysis/RCDHeat/CompactSquareIntegrability.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: CompactSquareIntegrability, CompactDensityDescent, CompactRecovery, CompactConvergence, ProbabilityRecovery.

  1. theorem OAI.RegularPointCoordinates.compactSquare_integrable line 18
  2. theorem OAI.RegularPointCoordinates.compactSquare_entropy_integrable line 21
  3. theorem OAI.RegularPointCoordinates.compactSquare_weight_integrable line 26
  4. theorem OAI.RegularPointCoordinates.compactSupport_of_dist_bound line 33
  5. theorem OAI.RegularPointCoordinates.FullCD.compact_sqrt_density_descent line 48
  6. theorem OAI.RegularPointCoordinates.FullCD.compact_density_HWI line 143
  7. def OAI.RegularPointCoordinates.clipPositive line 175
  8. theorem OAI.RegularPointCoordinates.clipPositive_lipschitz line 176
  9. theorem OAI.RegularPointCoordinates.clipPositive_zero line 178
  10. theorem OAI.RegularPointCoordinates.clipPositive_bounds line 179
  11. theorem OAI.RegularPointCoordinates.clipPositive_eq_self line 181
  12. theorem OAI.RegularPointCoordinates.IsSlopeMajorant.comp_contraction line 184
  13. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.bounded_recovery line 189
  14. theorem OAI.RegularPointCoordinates.radialCutoff_slope_zero line 215
  15. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.compact_bounded_recovery line 225
  16. theorem OAI.RegularPointCoordinates.compact_bounded_integral_tendsto line 315
  17. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.compact_probability_recovery line 349