NormalizedTorsion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Torsion bounds with the correct radius-squared scaling

theorem OAI.RegularPointCoordinates.exists_normalized_torsion_bound line 19

Source documentation

A normalized Sobolev inequality gives a torsion height proportional to its length-squared parameter, uniformly as the volume tends to zero.

theorem exists_normalized_torsion_bound {d C : ℝ} (hd : 1 < d) (hC : 0 ≤ C) :
    ∃ K : ℝ, 0 < K ∧ ∀ (Ω : Set X), μ Ω ≠ ∞ → 0 < μ.real Ω →
      ∀ s : ℝ, 0 < s → ∀ 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 * s * (μ.real Ω) ^ (1 / d - 1)) * energyForm μ hQ φ.val φ.val) →
      ∀ᵐ x ∂μ.restrict Ω, SobolevSpace.toLp μ hQ u.val x ≤ K * s := by
…

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

theorem OAI.RegularPointCoordinates.exists_uniform_normalized_bounded_torsion line 63

Source documentation

Coercivity constructs the torsion solution; normalized Sobolev controls its height by a uniform multiple of the length-squared parameter.

theorem exists_uniform_normalized_bounded_torsion {d C : ℝ} (hd : 1 < d) (hC : 0 ≤ C) :
    ∃ K : ℝ, 0 < K ∧ ∀ (Ω : Set X), MeasurableSet Ω → μ Ω ≠ ∞ → 0 < μ.real Ω →
      ∀ s : ℝ, 0 < s → ∀ P : ℝ, 0 ≤ P →
      (∀ v : SobolevSpace.dirichlet μ hQ Ω,
        ‖SobolevSpace.toLp μ hQ v.val‖ ^ 2 ≤ P * energyForm μ hQ v.val v.val) →
      (∀ φ : SobolevSpace.dirichlet μ hQ Ω,
        (∫ x in Ω, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
          (C * s * (μ.real Ω) ^ (1 / d - 1)) * energyForm μ hQ φ.val φ.val) →
      ∃ τ : SobolevSpace.dirichlet μ hQ Ω,
        (∀ φ : SobolevSpace.dirichlet μ hQ Ω,
          energyForm μ hQ τ.val φ.val = ∫ x in Ω, SobolevSpace.toLp μ hQ φ.val x ∂μ) ∧
        (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ τ.val x ∧
…

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