PoissonCaccioppoli.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Local energy control for a bounded constant-source solution

theorem OAI.RegularPointCoordinates.IsConstantLaplacianOn.cutoff_energy_le line 19

Source documentation

The source term adds its natural amplitude contribution to the usual cutoff energy bound. No gradient bound on the Poisson solution is assumed.

theorem IsConstantLaplacianOn.cutoff_energy_le
    {Ω : Set X} (hfin : μ Ω ≠ ∞)
    (f η : SobolevSpace μ hQ) (c : ℝ) (hf : IsConstantLaplacianOn μ hQ Ω f c)
    {χ : X → ℝ} {L A : ℝ≥0} (hχ : LipschitzWith L χ)
    (hs : HasCompactSupport χ) (hb : ∀ x, 0 ≤ χ x ∧ χ x ≤ 1)
    (hsupp : tsupport χ ⊆ Ω) (hη : SobolevSpace.toLp μ hQ η =ᵐ[μ] χ)
    (hA : ∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ f x| ≤ A) :
    (∫ x, (χ x)^2*(SobolevSpace.minimalSlope μ hQ f x)^2 ∂μ) ≤
      (2*|c| *A+4*(A:ℝ)^2*(L:ℝ)^2)*μ.real Ω := by
…

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