PositiveSourceMeasure.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Positive measure sources and bounded Dirichlet tests

Bounded clipping of the Lipschitz core converges in L2 with uniformly bounded Sobolev norm. Weak energy convergence therefore extends a source mass bound to every bounded nonnegative Dirichlet test. This argument needs no values of an arbitrary Sobolev representative on a singular source measure.

theorem OAI.RegularPointCoordinates.bounded_dirichlet_test_bound_of_core line 25

Source documentation

Extend a bound on bounded Lipschitz core tests by weak Sobolev convergence.

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

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

def OAI.RegularPointCoordinates.IsDirichletMeasureSource line 81
Source documentation
The distributional positive source on the Dirichlet Lipschitz core. The source is integrated only on continuous representatives.
```
def IsDirichletMeasureSource (Ω : Set X) (H : SobolevSpace μ hQ)
    (σ : Measure X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.SobolevSpace

theorem OAI.RegularPointCoordinates.IsDirichletMeasureSource.bounded_test_bound line 92

Source documentation

A finite positive source controls every bounded nonnegative Dirichlet energy test by its mass on the domain.

theorem IsDirichletMeasureSource.bounded_test_bound (Ω : Set X)
    (H : SobolevSpace μ hQ) (σ : Measure X) [IsFiniteMeasure σ]
    (hΩ : MeasurableSet Ω) (hsource : IsDirichletMeasureSource μ hQ Ω H σ)
    (φ : SobolevSpace.dirichlet μ hQ Ω) {s : ℝ} (hs : 0 ≤ s)
    (hφ : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x ∧
      SobolevSpace.toLp μ hQ φ.val x ≤ s) :
    energyForm μ hQ H φ.val ≤ σ.real Ω * s := by
…

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

theorem OAI.RegularPointCoordinates.positive_source_bounds_of_measure line 123

Source documentation

The manuscript's positive-source bounds from a positive measure identity on compact Lipschitz tests. Singular source mass is retained.

theorem positive_source_bounds_of_measure (Ω : Set X) (hΩ : MeasurableSet Ω)
    (hΩfin : μ Ω ≠ ∞) (H : SobolevSpace.dirichlet μ hQ Ω)
    (σ : Measure X) [IsFiniteMeasure σ]
    (hsource : IsDirichletMeasureSource μ hQ Ω H.val σ)
    {d C B : ℝ} (hd : 1 < d) (hC : 0 ≤ C) (hB : 0 ≤ B)
    (hH : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H.val x ∧
      SobolevSpace.toLp μ hQ H.val x ≤ B)
    (hsob : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (∫ x in Ω, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
        C * energyForm μ hQ φ.val φ.val) :
    IntegrableOn (fun x => SobolevSpace.minimalSlope μ hQ H.val x) Ω μ ∧
      (∫ x in Ω, SobolevSpace.minimalSlope μ hQ H.val x ∂μ) ≤
…

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