OAI/Geometry/RCD/Sobolev/CutoffPoissonLaplacian.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.IsConstantLaplacianOn.cutoff_weakLaplacian line 20

   Source documentation

   A compact Lipschitz cutoff converts the local constant-source equation into a global L² Laplacian. The gradient cross term is retained explicitly.

   theorem IsConstantLaplacianOn.cutoff_weakLaplacian
       {Ω : Set X} (f η : SobolevSpace μ hQ) (c : ℝ)
       (hf : IsConstantLaplacianOn μ hQ Ω f c)
       (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)
       (hsupp : tsupport χ ⊆ Ω) (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 => c*χ x+SobolevSpace.toLp μ hQ f x*d x+
           2*localGamma μ hQ f η x := by
   …

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