GoodLaplacianCutoff.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Quantitative cutoff input and its canonical Bochner application

The existence input is the fixed radius-ratio specialization of Mondino-- Naber (2019), Lemma 3.1 (arXiv:1405.2222v3, pp.13--14), also stated in Connell et al. (2021), Lemma 2.6. Scaling to unit radius and lowering the curvature bound to -1 makes its constant dimensional. Support of the Laplacian off the transition region is the locality of the weak Laplacian.

structure OAI.RegularPointCoordinates.GoodLaplacianCutoff line 26
Source documentation
An actual Sobolev cutoff with bounded weak Laplacian.
```
structure GoodLaplacianCutoff (p : X) (r C : ℝ) where
…
```
def OAI.RegularPointCoordinates.LocalGoodCutoffInput line 41
Source documentation
Exact existence consequence at bounded rescaled curvature.
```
def LocalGoodCutoffInput {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD
theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.tsupport_subset line 49
Source documentation
The topological support remains inside the closed outer ball.
```
theorem tsupport_subset {p : X} {r C : ℝ} (χ : GoodLaplacianCutoff μ hQ p r C) :
    tsupport (χ.weight : X → ℝ) ⊆ closedBall p (2 * r) := by
…
```
Mentions: OAI.RegularPointCoordinates.GoodLaplacianCutoff
theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.hasCompactSupport line 57

theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.harmonic_mass_le line 63

Source documentation

The good cutoff and local harmonic Bochner equation imply small mass on the inner ball, without a separate raw-source assumption.

theorem harmonic_mass_le [IsFiniteMeasureOnCompacts μ]
    {n : ℕ} {p : X} {ρ C r κ : ℝ} {L : ℝ≥0}
    (χ : GoodLaplacianCutoff μ hQ p ρ C) (hρ : 0 < ρ) (hρr : ρ < r)
    (hC : 0 ≤ C) (hκ : 0 ≤ κ) (u : Fin n → SobolevSpace μ hQ)
    (M : PositiveBilinearMeasure X (Euclidean n))
    (G : ∀ v, LocalHarmonicEnergy μ hQ (sobolevColumnMap μ hQ u) M κ p r L v)
    {ε : ℝ} (hε : 0 ≤ ε)
    (herror : ∀ i j : Fin n, ∫ x in closedBall p (2 * ρ),
      |localGamma μ hQ (u i) (u j) x - (if i = j then 1 else 0)| ∂μ ≤ ε)
    (v : Euclidean n) :
    ⟪v, M.massOperator (ball p ρ) v⟫_ℝ ≤
      ((C / ρ ^ 2) * ((n : ℝ) ^ 2 * ε) / 2 +
…

Mentions: OAI.RegularPointCoordinates.GoodLaplacianCutoff, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.LocalHarmonicEnergy, OAI.RegularPointCoordinates.sobolevColumnMap, OAI.RegularPointCoordinates.localGamma