OAI/Geometry/RCD/Heat/HeatDensityL2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

L² heat densities without a Gaussian input

The pointwise heat evaluation estimate is tested against capped versions of its actual Radon--Nikodym density. Monotone convergence gives the square-integrable row and its volume-normalized bound.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity_square_bound line 24
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity_memLp_two line 69