OAI/Analysis/RCDHeat/VariableRadialSecant.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: VariableRadialSecant, DimensionalPairCutoff, VariableHeatCutoffCost, VariableHeatSlope.

  1. theorem OAI.RegularPointCoordinates.variable_secant_algebra line 21
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.variable_cutoff_heat_secant line 42
  3. theorem OAI.RegularPointCoordinates.square_difference_exponential line 125
  4. theorem OAI.RegularPointCoordinates.pair_dist_square_exponential line 144
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.radial_heat_pair_cost_exponential line 174
  6. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.radial_heat_two_cost_exponential line 256
  7. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.variable_heat_frequent_slope line 339