OAI/Analysis/RCDHeat/GeometricSlopeOptimization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: GeometricSlopeOptimization, GeometricSignedOptimization, DimensionalScaledParameter, DimensionalScaledGradient, DimensionalLocalGradient.

  1. theorem OAI.RegularPointCoordinates.localSlope_sq_le_geometric_quadratic line 20
  2. theorem OAI.RegularPointCoordinates.localSlope_sq_le_geometric_limit line 78
  3. theorem OAI.RegularPointCoordinates.geometric_signed_slope_bound line 116
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dimensional_scaled_parameter_ratio line 152
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dimensional_scaled_parameter line 201
  6. def OAI.RegularPointCoordinates.heatDimensionCoefficient line 258
  7. theorem OAI.RegularPointCoordinates.heatKernelIntegral_pos line 261
  8. theorem OAI.RegularPointCoordinates.heatDimensionCoefficient_nonneg line 267
  9. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dimensional_scaled_gradient line 274
  10. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dimensional_local_gradient line 335