HeatMeasureMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_compact_le_one line 18
Source documentation
The Markov bound gives mass at most one on every compact set.
```
theorem heatRadonMeasure_compact_le_one (t : ℝ) (ht : 0 < t) (x : X)
    {S : Set X} (hS : IsCompact S) : hX.heatRadonMeasure hn p t ht x S ≤ 1 := by
…
```
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_mass_le_one line 33
Source documentation
The constructed Radon measure is a subprobability measure.
```
theorem heatRadonMeasure_mass_le_one (t : ℝ) (ht : 0 < t) (x : X) :
    hX.heatRadonMeasure hn p t ht x univ ≤ 1 := by
…
```
instance OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_finite line 39