OAI/Analysis/RCDHeat/WeightedGradientConvex.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: WeightedGradientConvex, WeightedGradientDerivative, KantorovichVariationBound, KantorovichVariation.

  1. theorem OAI.RegularPointCoordinates.convex_summand_differentiable line 21
  2. def OAI.RegularPointCoordinates.weightedGradientSquare line 48
  3. theorem OAI.RegularPointCoordinates.weightedGradientSquare_integrable line 51
  4. theorem OAI.RegularPointCoordinates.weightedGradientSquare_self line 57
  5. theorem OAI.RegularPointCoordinates.weightedGradientSquare_convex line 63
  6. theorem OAI.RegularPointCoordinates.weightedGradientSquare_line_convex line 95
  7. theorem OAI.RegularPointCoordinates.weightedGradientSquare_line_differentiable line 116
  8. def OAI.RegularPointCoordinates.weightedGradientPair line 150
  9. theorem OAI.RegularPointCoordinates.weightedGradientSquare_hasDerivAt_zero line 153
  10. theorem OAI.RegularPointCoordinates.weightedGradientPair_neg_right line 164
  11. def OAI.RegularPointCoordinates.planInitialSecant line 190
  12. theorem OAI.RegularPointCoordinates.kantorovich_perturbation_increment line 193
  13. theorem OAI.RegularPointCoordinates.kantorovich_directional_lower_bound line 233
  14. theorem OAI.RegularPointCoordinates.weightedGradientPair_secant_limit line 317
  15. theorem OAI.RegularPointCoordinates.kantorovich_directional_eventually_gt line 333
  16. theorem OAI.RegularPointCoordinates.planInitialSecant_neg_sobolev line 362
  17. theorem OAI.RegularPointCoordinates.kantorovich_signed_first_variation line 387