HeatBoundedSmoothing.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded-data Lipschitz smoothing for the actual RCD heat flow

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_bounded_gradient line 18
Source documentation
Reverse Poincaré bounds the weak gradient of a positive-time heat flow using only the amplitude of its initial L² data.
```
theorem NoncollapsedRCD.heat_bounded_gradient
    (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X) (p : X) :
    letI : ProperSpace X := hX.proper K n hn
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_bounded_lipschitz line 50

Source documentation

Positive heat time turns arbitrary bounded L² data into a function with a Lipschitz representative.

theorem NoncollapsedRCD.heat_bounded_lipschitz
    (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X) (p : X)
    (f : Lp ℝ 2 (hausdorff n X)) (C : ℝ≥0)
    (hf : ∀ᵐ x ∂hausdorff n X, |f x| ≤ C) (T : ℝ) (hT : 0 < T) :
    letI : ProperSpace X := hX.proper K n hn
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff