BoundaryMaximum.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Weak maximum principle with nonnegative Lipschitz boundary data

The negative part is placed in the genuine Dirichlet space by bounded-energy approximation of the Lipschitz core. This is the boundary comparison needed for the boundedness of the Poisson replacement.

theorem OAI.RegularPointCoordinates.energyForm_add_right line 23

theorem OAI.RegularPointCoordinates.positivePart_mem_dirichlet_of_boundary_nonpos line 30

Source documentation

Adding nonpositive Lipschitz boundary data does not obstruct the Dirichlet membership of the positive part.

theorem positivePart_mem_dirichlet_of_boundary_nonpos (Ω : Set X)
    (q : SobolevSpace μ hQ) (Q : X → ℝ) {C : ℝ≥0} (hQlip : LipschitzWith C Q)
    (hQnonpos : ∀ x, Q x ≤ 0) (hq : SobolevSpace.toLp μ hQ q =ᵐ[μ] Q)
    (v : SobolevSpace.dirichlet μ hQ Ω) :
    SobolevSpace.compContraction μ hQ
      ((LipschitzWith.id : LipschitzWith 1 (fun t : ℝ => t)).max_const 0)
      (max_self 0) (q + v.val) ∈ SobolevSpace.dirichlet μ hQ Ω := by
…

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

theorem OAI.RegularPointCoordinates.harmonic_nonneg_of_boundary line 78

Source documentation

A weakly harmonic function with nonnegative Lipschitz boundary values is nonnegative. The Poincare bound is on the actual closed Dirichlet space.

theorem harmonic_nonneg_of_boundary (Ω : Set X) {P : ℝ} (hP : 0 ≤ P)
    (hbound : ∀ v : SobolevSpace.dirichlet μ hQ Ω,
      ‖SobolevSpace.toLp μ hQ v.val‖ ^ 2 ≤ P * energyForm μ hQ v.val v.val)
    (f q : SobolevSpace μ hQ) (Q : X → ℝ) {C : ℝ≥0}
    (hQlip : LipschitzWith C Q) (hQnonneg : ∀ x, 0 ≤ Q x)
    (hq : SobolevSpace.toLp μ hQ q =ᵐ[μ] Q)
    (hfq : f - q ∈ SobolevSpace.dirichlet μ hQ Ω)
    (hf : ∀ φ : SobolevSpace.dirichlet μ hQ Ω, energyForm μ hQ f φ.val = 0) :
    ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ f x := by
…

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