PoissonSourceEstimates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Positive-source estimates for the actual Poisson replacement

The positive Laplacian defect is specified on the boundary datum and compact Lipschitz tests. Its action on the difference with the constructed replacement is proved, then used for positivity, height and linear gradient estimates.

theorem OAI.RegularPointCoordinates.replacement_has_measure_source line 27

Source documentation

The Laplacian defect of the boundary datum is the positive source of its difference with the constant-Laplacian replacement.

theorem replacement_has_measure_source (Ω : Set X) (q f : SobolevSpace μ hQ)
    (σ : Measure X) (a : ℝ)
    (hdefect : ∀ (ψ : SobolevSpace μ hQ) (v : X → ℝ) (C : ℝ≥0),
      LipschitzWith C v → HasCompactSupport v → tsupport v ⊆ Ω →
      SobolevSpace.toLp μ hQ ψ =ᵐ[μ] v →
      energyForm μ hQ q ψ + a * (∫ x in Ω, v x ∂μ) = ∫ x, v x ∂σ)
    (hsolve : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      energyForm μ hQ f φ.val = -a * ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ) :
    IsDirichletMeasureSource μ hQ Ω (q - f) σ := by
…

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

theorem OAI.RegularPointCoordinates.comparison_of_replacement_source line 48

Source documentation

The positive source on compact tests implies the full weak comparison inequality used by the Dirichlet maximum principle.

theorem comparison_of_replacement_source (Ω : Set X) (q f : SobolevSpace μ hQ)
    (σ : Measure X) (a : ℝ)
    (hsource : IsDirichletMeasureSource μ hQ Ω (q - f) σ)
    (hsolve : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      energyForm μ hQ f φ.val = -a * ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ)
    (φ : SobolevSpace.dirichlet μ hQ Ω)
    (hφ : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x) :
    -energyForm μ hQ q φ.val ≤ a * ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ := by
…

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

theorem OAI.RegularPointCoordinates.poisson_source_estimates line 64

Source documentation

The analytic Poisson bounds in fixed rescaled units, with constants coming from torsion and the positive-source estimate.

theorem poisson_source_estimates (Ω : Set X) (hΩ : MeasurableSet Ω)
    (hfin : μ Ω ≠ ∞) {P : ℝ} (hP : 0 ≤ P)
    (hpoin : ∀ v : SobolevSpace.dirichlet μ hQ Ω,
      ‖SobolevSpace.toLp μ hQ v.val‖ ^ 2 ≤ P * energyForm μ hQ v.val v.val)
    (q f : SobolevSpace μ hQ) (Q : X → ℝ) {L : ℝ≥0}
    (hQlip : LipschitzWith L Q) (hQ0 : ∀ x, 0 ≤ Q x)
    (hq : SobolevSpace.toLp μ hQ q =ᵐ[μ] Q)
    {a B K A d C : ℝ} (ha : 0 ≤ a) (hB : 0 ≤ B) (hK : 0 ≤ K)
    (hA : 0 ≤ A) (hd : 1 < d) (hC : 0 ≤ C)
    (hQB : ∀ᵐ x ∂μ.restrict Ω, Q x ≤ B)
    (hgradq : ∀ᵐ x ∂μ.restrict Ω, SobolevSpace.minimalSlope μ hQ q x ≤ A)
    (τ : SobolevSpace.dirichlet μ hQ Ω)
…

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