CutoffGamma.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Local product rule for arbitrary Sobolev cutoff products

Pointwise locality allows the bounded product rule to be applied on each finite value strip. No integrability of a third-order product is presumed.

theorem OAI.RegularPointCoordinates.localGamma_cutoffCLM line 22

Source documentation

Multiplication by a compactly supported nonnegative Lipschitz function satisfies the local product rule even when the other factor is unbounded.

theorem localGamma_cutoffCLM (f η h : 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) :
    localGamma μ hQ (SobolevSpace.cutoffCLM μ hQ hv hs hb hn f) h =ᵐ[μ]
      fun x => v x*localGamma μ hQ f h x+
        SobolevSpace.toLp μ hQ f x*localGamma μ hQ η h x := by
…

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