WeakLaplacianCutoff.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Product rule for a compact cutoff and an L² weak Laplacian

theorem OAI.RegularPointCoordinates.IsWeakLaplacian.cutoff line 18

Source documentation

Localizing a bounded Sobolev function with an L² Laplacian preserves the L² Laplacian, with the full gradient cross term.

theorem IsWeakLaplacian.cutoff
    (f η : SobolevSpace μ hQ) (df : Lp ℝ 2 μ)
    (hf : IsWeakLaplacian μ hQ f df)
    (d : Lp ℝ 2 μ) (hd : IsWeakLaplacian μ hQ η d)
    {χ : X → ℝ} {L B A : ℝ≥0} (hχ : LipschitzWith L χ)
    (hs : HasCompactSupport χ) (hb : ∀ x, |χ x| ≤ B) (hn : ∀ x, 0 ≤ χ x)
    (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ] χ)
    (hA : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ f x| ≤ A) :
    ∃ q : Lp ℝ 2 μ,
      IsWeakLaplacian μ hQ (SobolevSpace.cutoffCLM μ hQ hχ hs hb hn f) q ∧
      q =ᵐ[μ] fun x => χ x*df x+SobolevSpace.toLp μ hQ f x*d x+
        2*localGamma μ hQ f η x := by
…

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