UniformRadialResolvent.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A radial resolvent with only a lower rescaled curvature bound

The resolvent and heat-gradient estimates hold at the chosen time. The volume bound is supplied by CD, including the improved nonnegative-curvature case. No two-sided bound on curvature is needed.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.radial_resolvent_of_volume line 19
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.uniform_radial_resolvent_bounded line 112
Source documentation
A fixed lower rescaled curvature bound gives a uniform resolvent time and therefore a uniform bounded-Laplacian approximation of the radial cutoff.
```
theorem NoncollapsedRCD.uniform_radial_resolvent_bounded {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (a : ℝ) (ha : 0 ≤ a) :
    ∃ D : ℝ, 1 ≤ D ∧ ∀ (p : X) (R : ℝ) (_hR : 0 < R), -a ≤ K*R^2 →
      letI : ProperSpace X := hX.proper K n hn
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.uniform_radial_resolvent line 175
Source documentation
A fixed lower rescaled curvature bound gives a uniform resolvent time and therefore a uniform bounded-Laplacian approximation of the radial cutoff.
```
theorem NoncollapsedRCD.uniform_radial_resolvent {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) :
    ∃ D : ℝ, 1 ≤ D ∧ ∀ (p : X) (R : ℝ) (_hR : 0 < R), -1 ≤ K*R^2 →
      letI : ProperSpace X := hX.proper K n hn
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD