PoissonReplacement.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Constant-Laplacian replacements with prescribed Sobolev boundary data

def OAI.RegularPointCoordinates.dirichletSource line 18
Source documentation
Integration against an actual L² source on the Dirichlet space.
```
def dirichletSource (Ω : Set X) (g : Lp ℝ 2 μ) :
    SobolevSpace.dirichlet μ hQ Ω →L[ℝ] ℝ :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace.dirichlet
theorem OAI.RegularPointCoordinates.dirichletSource_apply line 23
theorem OAI.RegularPointCoordinates.dirichletSource_indicator line 28
Source documentation
The finite-measure indicator is the constant source on the domain.
```
theorem dirichletSource_indicator (Ω : Set X) (hΩ : MeasurableSet Ω)
    (hfin : μ Ω ≠ ∞) (c : ℝ) (φ : SobolevSpace.dirichlet μ hQ Ω) :
    dirichletSource μ hQ Ω (indicatorConstLp 2 hΩ hfin c) φ =
      c * ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.dirichletSource, OAI.RegularPointCoordinates.SobolevSpace.toLp
theorem OAI.RegularPointCoordinates.norm_indicator_source_sq line 42

theorem OAI.RegularPointCoordinates.dirichlet_solution_energy_le line 58

Source documentation

Testing a Dirichlet solution with itself gives its quantitative energy bound from the L² source and the Poincare constant.

theorem dirichlet_solution_energy_le (Ω : Set X) {P : ℝ} (hP : 0 ≤ P)
    (hbound : ∀ f : SobolevSpace.dirichlet μ hQ Ω,
      ‖SobolevSpace.toLp μ hQ f.val‖ ^ 2 ≤ P * energyForm μ hQ f.val f.val)
    (g : Lp ℝ 2 μ) (f : SobolevSpace.dirichlet μ hQ Ω)
    (hsolve : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      energyForm μ hQ f.val φ.val = -dirichletSource μ hQ Ω g φ) :
    energyForm μ hQ f.val f.val ≤ P * ‖g‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.dirichletSource

theorem OAI.RegularPointCoordinates.exists_constant_laplacian_replacement line 93

Source documentation

Solves Delta v = c with v-u in the genuine zero-boundary Sobolev space. Only the displayed Poincare bound and finite domain measure are used.

theorem exists_constant_laplacian_replacement (Ω : Set X) (hΩ : MeasurableSet Ω)
    (hfin : μ Ω ≠ ∞) {P : ℝ} (hP : 0 ≤ P)
    (hbound : ∀ f : SobolevSpace.dirichlet μ hQ Ω,
      ‖SobolevSpace.toLp μ hQ f.val‖ ^ 2 ≤ P * energyForm μ hQ f.val f.val)
    (c : ℝ) (u : SobolevSpace μ hQ) :
    ∃ v : SobolevSpace μ hQ, v - u ∈ SobolevSpace.dirichlet μ hQ Ω ∧
      ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
        energyForm μ hQ v φ.val = -c * ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.SobolevSpace

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_constant_laplacian_replacement line 119

Source documentation

The RCD hypotheses supply both the finite measure and the Poincare bound used by the constant-Laplacian construction.

theorem NoncollapsedRCD.exists_constant_laplacian_replacement
    (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X)
    (p : X) {R : ℝ} (hR : 0 ≤ R) (Ω B : Set X)
    (hΩ : MeasurableSet Ω) (hB : MeasurableSet B)
    (hΩ0 : hausdorff n X Ω ≠ 0) (hB0 : hausdorff n X B ≠ 0)
    (hsΩ : Ω ⊆ Metric.closedBall p R) (hsB : B ⊆ Metric.closedBall p R)
    (hBΩ : B ⊆ Ωᶜ) (c : ℝ) (u : SobolevSpace (hausdorff n X) hX.quadratic) :
    ∃ v : SobolevSpace (hausdorff n X) hX.quadratic,
      v - u ∈ SobolevSpace.dirichlet (hausdorff n X) hX.quadratic Ω ∧
      ∀ φ : SobolevSpace.dirichlet (hausdorff n X) hX.quadratic Ω,
        energyForm (hausdorff n X) hX.quadratic v φ.val =
          -c * ∫ x in Ω, SobolevSpace.toLp (hausdorff n X) hX.quadratic φ.val x ∂hausdorff n X := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.SobolevSpace.toLp