TorsionSuperlevel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Nonlinear superlevel inequality for the Dirichlet torsion solution

Bounded two-level tests, rather than a prior integrability assertion for an unbounded power of the solution, justify each use of Sobolev and Hölder.

theorem OAI.RegularPointCoordinates.level_superlevel_measure_le line 20

Source documentation

The bounded level moment controls the measure of the upper superlevel.

theorem level_superlevel_measure_le {X : Type*} [MeasurableSpace X]
    (ν : Measure X) [IsFiniteMeasure ν] {u : X → ℝ} (hu : Measurable u)
    {k l p B : ℝ} (hkl : k < l) (hp : 0 < p)
    (hbound : (∫ x, levelClip k l (u x) ^ p ∂ν) ≤ B) :
    ν.real {x | l ≤ u x} ≤ B / (l - k) ^ p := by
…

Mentions: OAI.RegularPointCoordinates.levelClip

theorem OAI.RegularPointCoordinates.torsion_superlevel_le line 55

Source documentation

The superlinear measure recurrence underlying the torsion height bound.

theorem torsion_superlevel_le (Ω : Set X) (hΩfin : μ Ω ≠ ∞)
    (u : SobolevSpace.dirichlet μ hQ Ω)
    (hsolve : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      energyForm μ hQ u.val φ.val = ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ)
    {d C : ℝ} (hd : 1 < d) (hC : 0 ≤ C)
    (hsob : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (∫ x in Ω, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
        C * energyForm μ hQ φ.val φ.val)
    {k l : ℝ} (hk : 0 ≤ k) (hkl : k < l) :
    (μ.restrict Ω).real {x | l ≤ SobolevSpace.toLp μ hQ u.val x} ≤
      C ^ (2 * d) *
        ((μ.restrict Ω).real {x | k < SobolevSpace.toLp μ hQ u.val x}) ^ (2 * d - 1) /
…

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