ResidualBochnerMass.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Small full mass for a residual with small gradient

theorem OAI.RegularPointCoordinates.GoodLaplacianCutoff.mass_le_of_gradient line 21

Source documentation

Testing the full Bochner equation with the actual good cutoff converts an upper bound for the residual gradient into small mass on the inner ball.

theorem GoodLaplacianCutoff.mass_le_of_gradient
    {U : E →L[ℝ] SobolevSpace μ hQ} {M : PositiveBilinearMeasure X E}
    {κ : ℝ} {p : X} {r ρ C β : ℝ} {L : ℝ≥0} {v : E}
    (χ : GoodLaplacianCutoff μ hQ p ρ C) (_hρ : 0 < ρ) (hρr : ρ < r)
    (hC : 0 ≤ C) (hκ : 0 ≤ κ)
    (G : LocalHarmonicEnergy μ hQ U M κ p r L v)
    (hgradient : ∀ᵐ x ∂μ.restrict (closedBall p (2 * ρ)),
      localGamma μ hQ (U v) (U v) x ≤ β) :
    ⟪v, M.massOperator (ball p ρ) v⟫_ℝ ≤
      ((C / ρ ^ 2) / 2 + κ) * β * μ.real (closedBall p (2 * ρ)) := by
…

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