CompactHeatMeasure.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

A Radon measure representing each bounded heat evaluation

The positive functional is the actual heat semigroup on compact continuous data. Riesz--Markov constructs its representing measure, without assuming a kernel or a density. Subsequent density arguments can therefore work with the canonical measure rather than adding an existence premise.

def OAI.RegularPointCoordinates.compactTestToL2 line 24
Source documentation
Compact continuous tests as actual L² classes.
```
def compactTestToL2 : C_c(X, ℝ) →ₗ[ℝ] Lp ℝ 2 μ where
…
```
theorem OAI.RegularPointCoordinates.compactTestToL2_coe line 29
theorem OAI.RegularPointCoordinates.compactTestToL2_mono line 32
theorem OAI.RegularPointCoordinates.compactTestToL2_bounded line 41
def OAI.RegularPointCoordinates.NoncollapsedRCD.compactHeatEval line 54
Source documentation
Positive heat evaluation on compactly supported continuous functions.
```
def compactHeatEval (t : ℝ) (ht : 0 < t) (x : X) : C_c(X, ℝ) →ₚ[ℝ] ℝ where
…
```
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compactHeatEval_abs_le line 67
def OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure line 76
Source documentation
The canonical Radon heat measure at a fixed positive time and center.
```
def heatRadonMeasure (t : ℝ) (ht : 0 < t) (x : X) : Measure X :=
…
```
instance OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_regular line 79
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_integral line 83