NormalizedSourceGradient.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Linear positive-source bounds in normalized ball units

theorem OAI.RegularPointCoordinates.normalized_source_gradient_of_pos line 18

Source documentation

A normalized Sobolev inequality gives a linear source-mass estimate with a constant proportional to the square root of the length-squared scale.

theorem normalized_source_gradient_of_pos (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (hvol : 0 < μ.real Ω) (H : SobolevSpace.dirichlet μ hQ Ω)
    (hH : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H.val x)
    {d q C s P : ℝ} (hq : 1 < q) (hqd : q < d) (hC : 0 < C) (hs : 0 < s) (hP : 0 < P)
    (hsob : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (∫ x in Ω, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
        (C * s * (μ.real Ω) ^ (1 / d - 1)) * energyForm μ hQ φ.val φ.val)
    (hsource : ∀ φ : SobolevSpace.dirichlet μ hQ Ω, ∀ t : ℝ, 0 ≤ t →
      (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x ∧ SobolevSpace.toLp μ hQ φ.val x ≤ t) →
      energyForm μ hQ H.val φ.val ≤ P * t) :
    IntegrableOn (fun x => SobolevSpace.minimalSlope μ hQ H.val x) Ω μ ∧
      (∫ x in Ω, SobolevSpace.minimalSlope μ hQ H.val x ∂μ) ≤
…

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

theorem OAI.RegularPointCoordinates.normalized_source_gradient line 102

Source documentation

The scale-correct linear bound also includes zero source mass.

theorem normalized_source_gradient (Ω : Set X) (hfin : μ Ω ≠ ∞)
    (hvol : 0 < μ.real Ω) (H : SobolevSpace.dirichlet μ hQ Ω)
    (hH : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H.val x)
    {d q C s P : ℝ} (hq : 1 < q) (hqd : q < d) (hC : 0 < C) (hs : 0 < s) (hP : 0 ≤ P)
    (hsob : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (∫ x in Ω, |SobolevSpace.toLp μ hQ φ.val x| ^ (2 * d) ∂μ) ^ (1 / d) ≤
        (C * s * (μ.real Ω) ^ (1 / d - 1)) * energyForm μ hQ φ.val φ.val)
    (hsource : ∀ φ : SobolevSpace.dirichlet μ hQ Ω, ∀ t : ℝ, 0 ≤ t →
      (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x ∧ SobolevSpace.toLp μ hQ φ.val x ≤ t) →
      energyForm μ hQ H.val φ.val ≤ P * t) :
    IntegrableOn (fun x => SobolevSpace.minimalSlope μ hQ H.val x) Ω μ ∧
      (∫ x in Ω, SobolevSpace.minimalSlope μ hQ H.val x ∂μ) ≤
…