HeatPointEvaluation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Full support promotes the local almost-everywhere smoothing estimate to all points of the continuous bounded-data representative.

theorem OAI.RegularPointCoordinates.exists_heat_local_radius line 21
Source documentation
A radius below both the time and curvature scales.
```
theorem exists_heat_local_radius (K t : ℝ) (ht : 0 < t) :
    ∃ R : ℝ, 0 < R ∧ R^2 < t ∧ -1 ≤ K*R^2 := by
…
```
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.boundedHeat_local_L2_bound line 44
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.boundedHeat_L2_evaluation line 71
Source documentation
At every positive time, a common radius gives locally uniform bounded linear evaluations on bounded L² data.
```
theorem boundedHeat_L2_evaluation (t : ℝ) (ht : 0 < t) :
    ∃ R C : ℝ, 0 < R ∧ 1 ≤ C ∧ ∀ (x : X)
      (f : Lp ℝ 2 (hausdorff n X)) (hf : HasBoundedAmplitude f),
      |hX.boundedHeat hn p f hf t ht x| ≤
        C/Real.sqrt ((hausdorff n X).real (ball x R))*‖f‖ := by
…
```
Mentions: OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.HasBoundedAmplitude