OAI/Analysis/RCDHeat/VariableHeatODE.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: VariableHeatODE, VariableHeat, VariableHeatCoefficient, VariableAverageDual, QuadraticComparisonAdd, VariablePointwiseDual.

  1. theorem OAI.RegularPointCoordinates.gronwallBound_integral_exp line 19
  2. theorem OAI.RegularPointCoordinates.variable_slope_integrated line 28
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.variable_heat_contraction_positive line 49
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.variable_heat_contraction line 89
  5. def OAI.RegularPointCoordinates.heatSpaceFactor line 168
  6. def OAI.RegularPointCoordinates.heatTimePenalty line 170
  7. theorem OAI.RegularPointCoordinates.heatSpaceFactor_pos line 173
  8. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.variable_heat_average_quadratic_dual line 186
  9. theorem OAI.RegularPointCoordinates.quadratic_comparison_of_average_bound_add line 273

    Also declared: OAI/Geometry/RCD/Harmonic/AverageQuadraticError.lean:14 (same declaration text).

  10. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.variable_heat_pointwise_quadratic_dual line 328