BoundedHeatRepresentative.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Canonical bounded-data heat representatives

The actual Cheeger semigroup and the proved reverse Poincare estimate give continuous representatives on every RCD space in this application. Full support makes the representative unique; positivity, linearity and the Markov amplitude bound therefore hold at every point. No heat kernel is assumed in this construction.

def OAI.RegularPointCoordinates.HasBoundedAmplitude line 24
Source documentation
Essential boundedness of the L² datum; only a finite amplitude is used.
```
def HasBoundedAmplitude (f : Lp ℝ 2 (hausdorff n X)) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.hausdorff
def OAI.RegularPointCoordinates.NoncollapsedRCD.boundedHeat line 33
Source documentation
The continuous representative constructed from bounded-data smoothing.
```
def boundedHeat (f : Lp ℝ 2 (hausdorff n X)) (hf : HasBoundedAmplitude f)
    (t : ℝ) (ht : 0 < t) : X → ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.HasBoundedAmplitude
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.boundedHeat_represents line 38
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.boundedHeat_continuous line 46
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.boundedHeat_unique line 53
Source documentation
Independence of the base point and the bound chosen in the construction.
```
theorem boundedHeat_unique (f : Lp ℝ 2 (hausdorff n X))
    (hf : HasBoundedAmplitude f) (t : ℝ) (ht : 0 < t)
    {v : X → ℝ} (hv : Continuous v)
    (hrep : heatAt (hausdorff n X) hX.quadratic t f =ᵐ[hausdorff n X] v) :
    hX.boundedHeat hn p f hf t ht = v := by
…
```
Mentions: OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.HasBoundedAmplitude, OAI.RegularPointCoordinates.heatAt
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.boundedHeat_lipschitz line 63