PoissonAnnularEnergy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Energy control of the annular Poisson error without a gradient bound

theorem OAI.RegularPointCoordinates.IsConstantLaplacianOn.annular_error_L1_le line 19

Source documentation

A second cutoff covering the transition annulus controls its cross source by the equation and the amplitude of the original solution.

theorem IsConstantLaplacianOn.annular_error_L1_le
    {Ω : Set X} (hfin : μ Ω ≠ ∞)
    (f η : SobolevSpace μ hQ) (c : ℝ) (hf : IsConstantLaplacianOn μ hQ Ω f c)
    (A : ℝ≥0) (hApos : 0 < (A:ℝ))
    (hA : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ f x| ≤ A)
    {χ : X → ℝ} {L : ℝ≥0} (hχ : LipschitzWith L χ)
    (hs : HasCompactSupport χ) (hb : ∀ x, 0 ≤ χ x ∧ χ x ≤ 1)
    (hsupp : tsupport χ ⊆ Ω) (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ] χ)
    {p : X} {R C : ℝ} (hR : 0 < R) (hC : 0 ≤ C)
    (ξ : GoodLaplacianCutoff μ hQ p R C)
    (hinside : closedBall p (2*R) ⊆ Ω)
    (hone : ∀ x, R ≤ dist x p → dist x p ≤ 2*R → χ x = 1)
…

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

theorem OAI.RegularPointCoordinates.IsConstantLaplacianOn.cutoff_cross_L1_le line 94

Source documentation

The same estimate written directly for the cutoff cross density.

theorem IsConstantLaplacianOn.cutoff_cross_L1_le
    {Ω : Set X} (hfin : μ Ω ≠ ∞)
    (f η : SobolevSpace μ hQ) (c : ℝ) (hf : IsConstantLaplacianOn μ hQ Ω f c)
    (A : ℝ≥0) (hApos : 0 < (A:ℝ))
    (hA : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ f x| ≤ A)
    {χ : X → ℝ} {L : ℝ≥0} (hχ : LipschitzWith L χ)
    (hs : HasCompactSupport χ) (hb : ∀ x, 0 ≤ χ x ∧ χ x ≤ 1)
    (hsupp : tsupport χ ⊆ Ω) (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ] χ)
    {p : X} {R C : ℝ} (hR : 0 < R) (hC : 0 ≤ C)
    (ξ : GoodLaplacianCutoff μ hQ p R C)
    (hinside : closedBall p (2*R) ⊆ Ω)
    (hone : ∀ x, R ≤ dist x p → dist x p ≤ 2*R → χ x = 1) :
…

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