PositiveDirichletFunctional.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Positive source functionals on the Dirichlet space

Positivity on the nonnegative Lipschitz core passes to all nonnegative Dirichlet tests by positive-part approximation and weak energy convergence.

theorem OAI.RegularPointCoordinates.dirichlet_test_nonneg_of_core line 25

Source documentation

Positivity on the core suffices, without pointwise evaluation of Sobolev representatives against the source.

theorem dirichlet_test_nonneg_of_core (Ω : Set X) (H : SobolevSpace μ hQ)
    (hcore : ∀ (ψ : SobolevSpace μ hQ) (v : X → ℝ) (C : ℝ≥0),
      LipschitzWith C v → HasCompactSupport v → tsupport v ⊆ Ω →
      SobolevSpace.toLp μ hQ ψ =ᵐ[μ] v → (∀ x, 0 ≤ v x) →
      0 ≤ energyForm μ hQ H ψ)
    (φ : SobolevSpace.dirichlet μ hQ Ω)
    (hφ : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x) :
    0 ≤ energyForm μ hQ H φ.val := by
…

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

theorem OAI.RegularPointCoordinates.IsDirichletMeasureSource.test_nonneg line 70
Source documentation
A positive measure source is a positive functional on every nonnegative Dirichlet test.
```
theorem IsDirichletMeasureSource.test_nonneg (Ω : Set X)
    (H : SobolevSpace μ hQ) (σ : Measure X)
    (hsource : IsDirichletMeasureSource μ hQ Ω H σ)
    (φ : SobolevSpace.dirichlet μ hQ Ω)
    (hφ : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x) :
    0 ≤ energyForm μ hQ H φ.val := by
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.IsDirichletMeasureSource, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm

theorem OAI.RegularPointCoordinates.IsDirichletMeasureSource.solution_nonneg line 83

Source documentation

Coercivity and positivity of the measure source imply nonnegativity of its Dirichlet solution.

theorem IsDirichletMeasureSource.solution_nonneg (Ω : Set X)
    {P : ℝ} (hP : 0 ≤ P)
    (hpoin : ∀ v : SobolevSpace.dirichlet μ hQ Ω,
      ‖SobolevSpace.toLp μ hQ v.val‖ ^ 2 ≤ P * energyForm μ hQ v.val v.val)
    (H : SobolevSpace.dirichlet μ hQ Ω) (σ : Measure X)
    (hsource : IsDirichletMeasureSource μ hQ Ω H.val σ) :
    ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H.val x := by
…

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