OAI/Geometry/RCD/Sobolev/DirichletMaximum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.dirichlet_solution_nonneg line 19

   Source documentation

   A Dirichlet solution of a nonnegative functional is nonnegative. The proof uses the actual positive-part contraction and its energy inequality.

   theorem dirichlet_solution_nonneg (Ω : Set X) {P : ℝ} (hP : 0 ≤ P)
       (hbound : ∀ f : SobolevSpace.dirichlet μ hQ Ω,
         ‖SobolevSpace.toLp μ hQ f.val‖ ^ 2 ≤ P * energyForm μ hQ f.val f.val)
       (F : SobolevSpace.dirichlet μ hQ Ω →L[ℝ] ℝ)
       (hpositive : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
         (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x) → 0 ≤ F φ)
       (f : SobolevSpace.dirichlet μ hQ Ω)
       (hsolve : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
         energyForm μ hQ f.val φ.val = F φ) :
       ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ f.val x := by
   …

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

2. theorem OAI.RegularPointCoordinates.exists_nonnegative_dirichlet_solution line 71

   Source documentation

   The positive solution exists for every positive continuous source.

   theorem exists_nonnegative_dirichlet_solution (Ω : Set X) {P : ℝ} (hP : 0 ≤ P)
       (hbound : ∀ f : SobolevSpace.dirichlet μ hQ Ω,
         ‖SobolevSpace.toLp μ hQ f.val‖ ^ 2 ≤ P * energyForm μ hQ f.val f.val)
       (F : SobolevSpace.dirichlet μ hQ Ω →L[ℝ] ℝ)
       (hpositive : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
         (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x) → 0 ≤ F φ) :
       ∃ f : SobolevSpace.dirichlet μ hQ Ω,
         (∀ φ : SobolevSpace.dirichlet μ hQ Ω,
           energyForm μ hQ f.val φ.val = F φ) ∧
         (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ f.val x) := by
   …

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