OAI/Analysis/RCDHeat/RelaxedChain.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: RelaxedChain, Flatten, SlopeLocality, CompConvergence, SlopeEquality.

  1. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.comp_C1 line 22
  2. def OAI.RegularPointCoordinates.slopeFlatten line 76
  3. def OAI.RegularPointCoordinates.slopeFlattenDeriv line 77
  4. def OAI.RegularPointCoordinates.slopeFlattenFactor line 79
  5. theorem OAI.RegularPointCoordinates.slopeFlatten_den_pos line 81
  6. theorem OAI.RegularPointCoordinates.slopeFlatten_deriv line 84
  7. theorem OAI.RegularPointCoordinates.slopeFlattenDeriv_continuous line 90
  8. theorem OAI.RegularPointCoordinates.slopeFlattenDeriv_nonneg line 95
  9. theorem OAI.RegularPointCoordinates.slopeFlattenDeriv_le line 100
  10. theorem OAI.RegularPointCoordinates.slopeFlatten_lipschitz line 106
  11. theorem OAI.RegularPointCoordinates.slopeFlatten_zero line 114
  12. theorem OAI.RegularPointCoordinates.slopeFlattenDeriv_zero line 115
  13. theorem OAI.RegularPointCoordinates.slopeFlattenFactor_zero line 116
  14. theorem OAI.RegularPointCoordinates.slopeFlattenFactor_bounds line 118
  15. theorem OAI.RegularPointCoordinates.slopeFlattenFactor_continuous line 124
  16. theorem OAI.RegularPointCoordinates.slopeFlatten_eq_factor line 130
  17. theorem OAI.RegularPointCoordinates.slopeFlattenFactor_tendsto line 135
  18. theorem OAI.RegularPointCoordinates.slopeFlattenDeriv_tendsto line 147
  19. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.cut_zero line 169
  20. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_zero_on_zero line 239
  21. theorem OAI.RegularPointCoordinates.lipschitz_comp_quotient_bound line 254
  22. theorem OAI.RegularPointCoordinates.compLp_tendsto_of_pointwise line 263
  23. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.neg line 307
  24. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_neg line 328
  25. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_sub_le line 340
  26. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_eq_on_eq line 347
  27. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_sub_norm_le line 371