ScaledHarmonicMass.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual local Bochner mass has a uniform scaled bound

theorem OAI.RegularPointCoordinates.harmonic_scaled_local_mass_bound line 20

Source documentation

A larger good cutoff bounds only the local full measure needed by coarse dyadic balls; its exterior extension plays no role.

theorem harmonic_scaled_local_mass_bound {n : ℕ} {p : X} {R κ C B V : ℝ}
    (hR : 0 < R) (hκ : 0 ≤ κ) (hC : 0 ≤ C) (hB : 0 ≤ B)
    (hcurv : κ * R ^ 2 ≤ 1)
    (U : Euclidean n →L[ℝ] SobolevSpace μ hQ) (M : PositiveBilinearMeasure X (Euclidean n)) (L : ℝ≥0)
    (G : ∀ v, LocalHarmonicEnergy μ hQ U M κ p (4 * R) L v)
    (χ : GoodLaplacianCutoff μ hQ p (2 * R) C)
    (hL : (L : ℝ) ^ 2 ≤ B)
    (hvolume : μ.real (closedBall p (4 * R)) ≤ V * (5 * R) ^ n) (v : Euclidean n) :
    ⟪v, M.massOperator (ball p (2 * R)) v⟫_ℝ ≤
      ((C / 8 + 1) * B * V * 5 ^ n) * (R ^ n / R ^ 2) * ‖v‖ ^ 2 := by
…

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