OAI/Geometry/RCD/Sobolev/PoissonCutoffSource.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Separating the bounded and annular parts of a localized Poisson source

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

    Source documentation

    The localized source is the sum of bounded data and an integrable L² error supported in the cutoff annulus. Both parts are constructed from the actual weak equation.

    theorem IsConstantLaplacianOn.cutoff_source_decomposition
    {Ω : Set X} (f : SobolevSpace μ hQ) (c : ℝ)
    (hf : IsConstantLaplacianOn μ hQ Ω f c) (A : ℝ≥0)
    (hA : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ f x| ≤ A)
    {p : X} {R C : ℝ} (hR : 0 < R) (hC : 0 ≤ C)
    (χ : GoodLaplacianCutoff μ hQ p R C) (hΩ : closedBall p (2*R) ⊆ Ω) :
    ∃ b e : Lp ℝ 2 μ,
      IsWeakLaplacian μ hQ
        (SobolevSpace.cutoffCLM μ hQ (B := 1) χ.lipschitz (χ.hasCompactSupport μ hQ)
…

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