OAI/Analysis/RCDHeat/RelaxedSlope.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: RelaxedSlope, RelaxedSlopeClosure, LpMultiplier, PointwiseGluing, RelaxedGluing.

  1. def OAI.RegularPointCoordinates.IsRelaxedSlope line 21
  2. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.nonneg line 28
  3. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.energy_le line 35
  4. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.add line 49
  5. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.const_mul line 64
  6. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.unique_minimizer line 77
  7. theorem OAI.RegularPointCoordinates.SobolevSpace.exists_minimalRelaxedSlope line 97
  8. def OAI.RegularPointCoordinates.SobolevSpace.minimalSlope line 141
  9. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_isRelaxed line 144
  10. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_norm_sq line 148
  11. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.mono line 157
  12. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.of_tendsto line 171
  13. theorem OAI.RegularPointCoordinates.relaxedSlope_isClosed line 193
  14. def OAI.RegularPointCoordinates.lpMultiplier line 206
  15. theorem OAI.RegularPointCoordinates.lpMultiplier_coe line 213
  16. theorem OAI.RegularPointCoordinates.lpMultiplier_congr line 217
  17. theorem OAI.RegularPointCoordinates.real_lipschitz_abs line 225
  18. def OAI.RegularPointCoordinates.lpAbs line 230
  19. theorem OAI.RegularPointCoordinates.lpAbs_coe line 233
  20. theorem OAI.RegularPointCoordinates.lpAbs_continuous line 237
  21. theorem OAI.RegularPointCoordinates.lpAbs_zero line 240
  22. theorem OAI.RegularPointCoordinates.localSlope_sub_const line 248
  23. theorem OAI.RegularPointCoordinates.localSlope_convex_glue line 254
  24. theorem OAI.RegularPointCoordinates.lipschitzWith_mul_of_support_bound line 280
  25. theorem OAI.RegularPointCoordinates.lipschitz_mul_compact_cutoff line 317
  26. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.cutoff_blend line 332