BoundedHeatIntegral.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Heat measure representation for all bounded L² data

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonMeasure_integral_bounded line 22
Source documentation
Uniform compact approximation and absolute continuity extend the constructed measure representation to every bounded L² datum.
```
theorem heatRadonMeasure_integral_bounded (t : ℝ) (ht : 0 < t) (x : X)
    (f : Lp ℝ 2 (hausdorff n X)) (C : ℝ≥0)
    (hf : ∀ᵐ y ∂hausdorff n X, |f y| ≤ C) :
    (∫ y, f y ∂hX.heatRadonMeasure hn p t ht x) = hX.boundedHeat hn p f ⟨C, hf⟩ t ht x := by
…
```
Mentions: OAI.RegularPointCoordinates.hausdorff

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatRadonDensity_integral_bounded line 61

Source documentation

The actual probability density represents all bounded L² heat data.

theorem heatRadonDensity_integral_bounded (t : ℝ) (ht : 0 < t) (x : X)
    (f : Lp ℝ 2 (hausdorff n X)) (C : ℝ≥0)
    (hf : ∀ᵐ y ∂hausdorff n X, |f y| ≤ C) :
    (∫ y, hX.heatRadonDensity hn p t ht x y * f y ∂hausdorff n X) =
      hX.boundedHeat hn p f ⟨C, hf⟩ t ht x := by
…

Mentions: OAI.RegularPointCoordinates.hausdorff