OAI/Geometry/RCD/Sobolev/CutoffPointwiseGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pointwise weak-gradient bound for a Sobolev cutoff product

  1. theorem OAI.RegularPointCoordinates.minimalSlope_cutoffCLM_sq_le line 17

    Source documentation

    The two-term cutoff energy inequality before integration.

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

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