OAI/Analysis/RCDHeat/SlopeMeasurability.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: SlopeMeasurability, SlopeCalculus, MinimalRelaxedSlope, RelaxedSlopeRecovery.

  1. def OAI.RegularPointCoordinates.slopeAtScale line 18
  2. theorem OAI.RegularPointCoordinates.slopeAtScale_mono line 22
  3. theorem OAI.RegularPointCoordinates.slopeAtScale_lowerSemicontinuous line 27
  4. theorem OAI.RegularPointCoordinates.localSlope_eq_iInf_scale line 47
  5. theorem OAI.RegularPointCoordinates.localSlope_measurable line 57
  6. theorem OAI.RegularPointCoordinates.slopeAtScale_term_le line 66
  7. theorem OAI.RegularPointCoordinates.slopeAtScale_add_le line 71
  8. theorem OAI.RegularPointCoordinates.localSlope_add_le line 86
  9. theorem OAI.RegularPointCoordinates.localSlope_congr_nhds line 98
  10. theorem OAI.RegularPointCoordinates.localSlope_mul_le_eps line 116
  11. theorem OAI.RegularPointCoordinates.localSlope_mul_le line 165
  12. theorem OAI.RegularPointCoordinates.energyLp_lowerSemicontinuous line 191
  13. theorem OAI.RegularPointCoordinates.lintegral_enorm_sq_Lp line 201
  14. theorem OAI.RegularPointCoordinates.localSlope_toReal_memLp line 212
  15. def OAI.RegularPointCoordinates.lipschitzSlopeLp line 223
  16. theorem OAI.RegularPointCoordinates.lipschitzSlopeLp_nonneg line 227
  17. theorem OAI.RegularPointCoordinates.lipschitzSlopeLp_enorm line 234
  18. theorem OAI.RegularPointCoordinates.lipschitzSlopeLp_energy line 242
  19. theorem OAI.RegularPointCoordinates.cheegerEnergy_le_of_slope_majorant line 253
  20. theorem OAI.RegularPointCoordinates.lipschitzWith_const_mul_real line 271
  21. def OAI.RegularPointCoordinates.IsSlopeMajorant line 284
  22. theorem OAI.RegularPointCoordinates.IsSlopeMajorant.add line 287
  23. theorem OAI.RegularPointCoordinates.IsSlopeMajorant.const_mul line 297
  24. theorem OAI.RegularPointCoordinates.energyLp_le_of_lipschitz_majorant line 307
  25. theorem OAI.RegularPointCoordinates.energyLp_local_lower_bound line 318
  26. theorem OAI.RegularPointCoordinates.slopeMajorants_cauchy_of_recovery line 333