HeatMeasureConservation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Conservation of the constructed heat measures

Semigroup self-adjointness passes compact cutoff exhaustion through the heat flow. Its already proved L¹ mass conservation then forces the mass of the pointwise Radon measures to be one at every center.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compactHeatEval_continuous line 24
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compactHeatEval_pair line 30
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_mass_average line 54
Source documentation
Averaging total pointwise mass against any nonnegative compact test recovers exactly that test's reference integral.
```
theorem heatRadonMeasure_mass_average (t : ℝ) (ht : 0 < t)
    (F : C_c(X, ℝ)) (hF : ∀ x, 0 ≤ F x) :
    (∫ x, F x * (hX.heatRadonMeasure hn p t ht x).real univ ∂hausdorff n X) =
      ∫ x, F x ∂hausdorff n X := by
…
```
Mentions: OAI.RegularPointCoordinates.hausdorff