LocalRepresentativeGradient.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Local gradient bounds from a bounded Lipschitz representative

theorem OAI.RegularPointCoordinates.localGamma_le_of_lipschitz_representative line 18

Source documentation

Compact localization makes a local Lipschitz representative an actual Sobolev comparison function. The extra amplitude term is quantitative.

theorem localGamma_le_of_lipschitz_representative
    (f : SobolevSpace μ hQ) (v : X → ℝ) (L A : ℝ≥0) (hv : LipschitzWith L v)
    (p : X) (r : ℝ) (hr : 0 < r)
    (he : SobolevSpace.toLp μ hQ f =ᵐ[μ.restrict (ball p (2*r))] v)
    (hA : ∀ᵐ x ∂μ.restrict (ball p (2*r)), |SobolevSpace.toLp μ hQ f x| ≤ A) :
    ∀ᵐ x ∂μ.restrict (ball p r), localGamma μ hQ f f x ≤ ((L:ℝ)+(A:ℝ)/r)^2 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma