GoodCutoffFromResolvent.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Good Laplacian cutoffs from the actual RCD resolvent

A scalar plateau applied to a radial resolvent yields the exact inner and outer radii used by the chart argument. Its differentiated formula gives locality of the Laplacian on both constant regions.

theorem OAI.RegularPointCoordinates.boundedLaplacian_comp_C2_formula line 22
theorem OAI.RegularPointCoordinates.plateau_derivatives_zero line 80
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.goodCutoffInput_bounded line 95
Source documentation
The curvature-dimension condition and heat resolvents produce a cutoff with uniformly controlled gradient and Laplacian.
```
theorem NoncollapsedRCD.goodCutoffInput_bounded {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (a : ℝ) (ha : 0 ≤ a) :
    2 ≤ n → ∃ C : ℝ, 1 ≤ C ∧ ∀ (p : X) (r : ℝ), 0 < r →
      -a ≤ K * r ^ 2 → Nonempty (GoodLaplacianCutoff (hausdorff n X) hX.quadratic p r C) := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.hausdorff
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.goodCutoffInput line 261
Source documentation
The dimensional cutoff bound at unit rescaled curvature.
```
theorem NoncollapsedRCD.goodCutoffInput {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) : LocalGoodCutoffInput hX := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalGoodCutoffInput
theorem OAI.RegularPointCoordinates.NoncollapsedRCD.goodCutoff_exists line 267
Source documentation
At any fixed radius the actual RCD resolvent supplies a good cutoff. The constant may depend on the rescaled lower curvature.
```
theorem NoncollapsedRCD.goodCutoff_exists {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (p : X) {r : ℝ} (hr : 0 < r) :
    ∃ C : ℝ, 1 ≤ C ∧ Nonempty (GoodLaplacianCutoff (hausdorff n X) hX.quadratic p r C) := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.hausdorff