OAI/Geometry/RCD/Heat/HeatConcentration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Short-time concentration of the actual heat measures

The constructed bounded-Laplacian cutoffs yield a dimensional escape estimate. No continuous-kernel or pointwise Gaussian estimate is used.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_concentration_of_cutoff line 23
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_concentration line 55
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_half_mass line 65