WeakSubsolution.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Weak subsolutions and nonnegative Dirichlet tests

def OAI.RegularPointCoordinates.IsWeakSubsolutionOn line 19
Source documentation
The distributional inequality Δu ≥ -a u, expressed using only the actual Sobolev energy form and L² pairing.
```
def IsWeakSubsolutionOn (Ω : Set X) (u : SobolevSpace μ hQ) (a : ℝ) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace
theorem OAI.RegularPointCoordinates.IsWeakSubsolutionOn.smul line 24

theorem OAI.RegularPointCoordinates.weakSubsolution_of_core line 34

Source documentation

Positive-part approximation of the Lipschitz core extends the distributional inequality to every nonnegative Dirichlet test.

theorem weakSubsolution_of_core (Ω : Set X) (u : SobolevSpace μ hQ) (a : ℝ)
    (hcore : ∀ (ψ : SobolevSpace μ hQ) (v : X → ℝ) (C : ℝ≥0),
      LipschitzWith C v → HasCompactSupport v → tsupport v ⊆ Ω →
      SobolevSpace.toLp μ hQ ψ =ᵐ[μ] v → (∀ x, 0 ≤ v x) →
      energyForm μ hQ u ψ ≤ a*inner ℝ (SobolevSpace.toLp μ hQ u) (SobolevSpace.toLp μ hQ ψ)) :
    IsWeakSubsolutionOn μ hQ Ω u a := by
…

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