OAI/Geometry/RCD/Heat/HeatTailGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One gradient bound for an entire smoothed heat tail

The outer heat time is fixed and positive. Markov contraction bounds its input at every parameter value, including before the tail equals heat.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatTail_gradient_bound line 22