TorsionBound.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform height of the Dirichlet torsion solution

The constant is chosen before the domain and the solution. Only the Dirichlet Sobolev constant, its exponent, and an upper volume bound enter.

theorem OAI.RegularPointCoordinates.exists_uniform_torsion_bound line 24

Source documentation

A uniform torsion bound from the displayed Dirichlet Sobolev inequality.

theorem exists_uniform_torsion_bound {d C V : ℝ} (hd : 1 < d)
    (hC : 0 ≤ C) (hV : 0 ≤ V) :
    ∃ K : ℝ, 0 < K ∧ ∀ (Ω : Set X), μ Ω ≠ ∞ → μ.real Ω ≤ V →
      ∀ u : SobolevSpace.dirichlet μ hQ Ω,
      (∀ φ : SobolevSpace.dirichlet μ hQ Ω,
        energyForm μ hQ u.val φ.val = ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ) →
      (∀ φ : SobolevSpace.dirichlet μ hQ Ω,
        (∫ x in Ω, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
          C * energyForm μ hQ φ.val φ.val) →
      ∀ᵐ x ∂μ.restrict Ω, SobolevSpace.toLp μ hQ u.val x ≤ K := by
…

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