OAI/Geometry/RCD/Sobolev/BalancedSourceGradient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.balancedGradientConstant line 13
2. theorem OAI.RegularPointCoordinates.balancedGradientConstant_pos line 16
3. theorem OAI.RegularPointCoordinates.balanced_positive_source_gradient line 26

   Source documentation

   When the tail coefficient is at most the domain volume, the weighted energy argument gives the correctly homogeneous square-gradient estimate.

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

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