OAI/Geometry/RCD/Heat/HeatParabolicStep.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A superlinear parabolic level estimate

The actual heat cylinder energy and the proved RCD Sobolev inequality control the next upper level. The constants are uniform at bounded rescaled curvature, and no heat-kernel estimate is assumed.

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