PoissonLocality.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Local representatives and bounded truncation of Poisson solutions

theorem OAI.RegularPointCoordinates.energyForm_eq_of_ae_eq_on line 18
Source documentation
Agreement on the working set preserves every zero-boundary pairing.
```
theorem energyForm_eq_of_ae_eq_on {Ω : Set X} (hΩ : MeasurableSet Ω)
    {f g : SobolevSpace μ hQ}
    (hfg : SobolevSpace.toLp μ hQ f =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ g)
    (φ : SobolevSpace.dirichlet μ hQ Ω) : energyForm μ hQ f φ.val = energyForm μ hQ g φ.val := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.energyForm
theorem OAI.RegularPointCoordinates.IsConstantLaplacianOn.congr_ae line 30
Source documentation
The local weak Poisson equation only depends on the representative inside its domain.
```
theorem IsConstantLaplacianOn.congr_ae {Ω : Set X} (hΩ : MeasurableSet Ω)
    {f g : SobolevSpace μ hQ} {c : ℝ}
    (hf : IsConstantLaplacianOn μ hQ Ω f c)
    (hfg : SobolevSpace.toLp μ hQ f =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ g) :
    IsConstantLaplacianOn μ hQ Ω g c := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.SobolevSpace.toLp

theorem OAI.RegularPointCoordinates.IsConstantLaplacianOn.bounded_extension line 41

Source documentation

A local amplitude bound permits a globally bounded representative in the same Sobolev class on the working domain, without changing its source.

theorem IsConstantLaplacianOn.bounded_extension {Ω : Set X} (hΩ : MeasurableSet Ω)
    {f : SobolevSpace μ hQ} {c : ℝ} (hf : IsConstantLaplacianOn μ hQ Ω f c)
    (A : ℝ≥0) (hA : ∀ᵐ x ∂μ.restrict Ω, |SobolevSpace.toLp μ hQ f x| ≤ A) :
    ∃ g : SobolevSpace μ hQ,
      IsConstantLaplacianOn μ hQ Ω g c ∧
      (∀ᵐ x ∂μ, |SobolevSpace.toLp μ hQ g x| ≤ A) ∧
      SobolevSpace.toLp μ hQ f =ᵐ[μ.restrict Ω] SobolevSpace.toLp μ hQ g := by
…

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