CutoffProductEnergy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Energy of a Lipschitz cutoff times an arbitrary Sobolev function

theorem OAI.RegularPointCoordinates.energy_cutoffCLM_le line 18

Source documentation

The usual two-term product energy bound, with no boundedness hypothesis on the Sobolev factor.

theorem energy_cutoffCLM_le (u η : SobolevSpace μ hQ)
    {v : X → ℝ} {L B A : ℝ≥0} (hv : LipschitzWith L v)
    (hs : HasCompactSupport v) (hb : ∀ x, |v x| ≤ B) (hn : ∀ x, 0 ≤ v x)
    (hrep : SobolevSpace.toLp μ hQ η =ᵐ[μ] v)
    (hgrad : ∀ᵐ x ∂μ, |SobolevSpace.minimalSlope μ hQ η x| ≤ A) :
    let z := SobolevSpace.cutoffCLM μ hQ hv hs hb hn u
…

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