SubsolutionCaccioppoli.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Upper-level Caccioppoli estimate with a zeroth-order term

theorem OAI.RegularPointCoordinates.IsWeakSubsolutionOn.upper_level_caccioppoli line 18

Source documentation

The potential term is retained explicitly, allowing the level-set iteration to use the same cutoff energy estimate as in the harmonic case.

theorem IsWeakSubsolutionOn.upper_level_caccioppoli
    {Ω : Set X} (u η : SobolevSpace μ hQ) {a k : ℝ} (hk : 0 ≤ k)
    (hu : IsWeakSubsolutionOn μ hQ Ω u a)
    {χ : X → ℝ} {L B A : ℝ≥0} (hχ : LipschitzWith L χ)
    (hs : HasCompactSupport χ) (hb : ∀ x, |χ x| ≤ B) (hn : ∀ x, 0 ≤ χ x)
    (hΩ : tsupport χ ⊆ Ω) (hrep : SobolevSpace.toLp μ hQ η =ᵐ[μ] χ)
    (hgrad : ∀ᵐ x ∂μ, |SobolevSpace.minimalSlope μ hQ η x| ≤ A) :
    let v := u.upperPositivePart μ hQ hk
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsWeakSubsolutionOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope