PoissonComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Comparison for the constant-Laplacian Dirichlet replacement

theorem OAI.RegularPointCoordinates.constant_laplacian_replacement_le line 21

Source documentation

A distributional upper Laplacian bound on the boundary datum makes its constant-Laplacian replacement lie below it. This is the comparison used for the squared-distance datum in the Poisson pinching argument.

theorem constant_laplacian_replacement_le (Ω : 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 v : SobolevSpace μ hQ)
    (hboundary : v - u ∈ SobolevSpace.dirichlet μ hQ Ω)
    (hsolve : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      energyForm μ hQ v φ.val = -c * ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ)
    (hcomparison : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x) →
      -energyForm μ hQ u φ.val ≤ c * ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ) :
    ∀ᵐ x ∂μ, SobolevSpace.toLp μ hQ v x ≤ SobolevSpace.toLp μ hQ u x := by
…

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

theorem OAI.RegularPointCoordinates.exists_constant_laplacian_replacement_le line 62

Source documentation

Existence and the comparison conclusion are obtained together from coercivity and the actual distributional Laplacian inequality.

theorem exists_constant_laplacian_replacement_le
    (Ω : 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)
    (hcomparison : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x) →
      -energyForm μ hQ u φ.val ≤ c * ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ) :
    ∃ v : SobolevSpace μ hQ, v - u ∈ SobolevSpace.dirichlet μ hQ Ω ∧
      (∀ φ : SobolevSpace.dirichlet μ hQ Ω,
        energyForm μ hQ v φ.val = -c * ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ) ∧
…

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