OAI/Analysis/RCDHeat/SlopeLevels.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: SlopeLevels, StrongLocality, ScalarInverse, ChainEquality, ExactChain.

  1. theorem OAI.RegularPointCoordinates.slopeFlatten_tendsto line 20
  2. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.cut_level line 28
  3. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_zero_on_level line 97
  4. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_smul_nonneg line 113
  5. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_smul line 123
  6. theorem OAI.RegularPointCoordinates.energyForm_le_slope_inner line 132
  7. theorem OAI.RegularPointCoordinates.energyForm_abs_le_slope_inner line 155
  8. theorem OAI.RegularPointCoordinates.energyForm_strongly_local line 166
  9. theorem OAI.RegularPointCoordinates.scalar_small_perturbation_inverse line 188
  10. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_comp_C1_le line 245
  11. theorem OAI.RegularPointCoordinates.SobolevSpace.comp_comp_eq line 267
  12. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_comp_C1_inverse line 280
  13. theorem OAI.RegularPointCoordinates.SobolevSpace.chain_signed_lower line 311
  14. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_comp_C1 line 377