HeatMeasureAbsoluteContinuity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Absolute continuity of the constructed heat measure

Small continuous cutoffs of a null compact set converge to zero in L². The uniform bounded-data smoothing estimate makes their heat values converge at every center. Radon regularity then excludes every null set. No kernel density is assumed.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_compact_null line 26
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_absolutelyContinuous line 47
Source documentation
Every positive-time heat evaluation has a density with respect to the actual reference measure, including at every prescribed center.
```
theorem heatRadonMeasure_absolutelyContinuous (t : ℝ) (ht : 0 < t) (x : X) :
    hX.heatRadonMeasure hn p t ht x ≪ hausdorff n X := by
…
```
Mentions: OAI.RegularPointCoordinates.hausdorff