PoissonHeight.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Height control for the Poisson replacement

A bounded torsion solution and the weak boundary maximum principle provide the bound needed by the positive-source gradient estimate.

theorem OAI.RegularPointCoordinates.exists_uniform_bounded_torsion line 26

Source documentation

Coercivity constructs torsion and the Sobolev iteration bounds it with a constant uniform over all the displayed domains.

theorem exists_uniform_bounded_torsion {d C V : ℝ} (hd : 1 < d)
    (hC : 0 ≤ C) (hV : 0 ≤ V) :
    ∃ K : ℝ, 0 < K ∧ ∀ (Ω : Set X), MeasurableSet Ω → μ Ω ≠ ∞ → μ.real Ω ≤ V →
      ∀ P : ℝ, 0 ≤ P →
      (∀ v : SobolevSpace.dirichlet μ hQ Ω,
        ‖SobolevSpace.toLp μ hQ v.val‖ ^ 2 ≤ P * energyForm μ hQ v.val v.val) →
      (∀ φ : SobolevSpace.dirichlet μ hQ Ω,
        (∫ x in Ω, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
          C * energyForm μ hQ φ.val φ.val) →
      ∃ τ : SobolevSpace.dirichlet μ hQ Ω,
        (∀ φ : SobolevSpace.dirichlet μ hQ Ω,
          energyForm μ hQ τ.val φ.val = ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ) ∧
…

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

theorem OAI.RegularPointCoordinates.poisson_replacement_height_le line 64

Source documentation

Torsion comparison bounds the nonnegative difference of the boundary datum and its constant-Laplacian replacement.

theorem poisson_replacement_height_le (Ω : 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 : ℝ} (ha : 0 ≤ a) (hB : 0 ≤ B) (hK : 0 ≤ K)
    (hQB : ∀ᵐ x ∂μ.restrict Ω, Q x ≤ B)
    (τ : SobolevSpace.dirichlet μ hQ Ω)
    (hτ : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      energyForm μ hQ τ.val φ.val = ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ)
…

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