InhomogeneousSobolev.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Relative Dirichlet Sobolev inequality with an L² term

Keeping the L² term removes the exterior-annulus condition. This is the form used by the local harmonic boundedness iteration.

theorem OAI.RegularPointCoordinates.inhomogeneous_power_bound line 17

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.inhomogeneous_dirichlet_sobolev line 45

Source documentation

A fixed exponent above two, with an inhomogeneous energy term, at bounded rescaled curvature. No exterior-annulus assumption is needed.

theorem NoncollapsedRCD.inhomogeneous_dirichlet_sobolev {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) :
    ∃ p C : ℝ, 2 < p ∧ 0 < C ∧ ∀ (x : X) (R : ℝ), 0 < R → -1 ≤ K*R^2 →
      ∀ w : SobolevSpace.dirichlet (hausdorff n X) hX.quadratic (ball x R),
      IntegrableOn (fun y => |SobolevSpace.toLp (hausdorff n X) hX.quadratic w.val y|^p)
        (ball x R) (hausdorff n X) ∧
      (∫ y in ball x R, |SobolevSpace.toLp (hausdorff n X) hX.quadratic w.val y|^p
        ∂hausdorff n X)^(2/p) ≤
      C*((hausdorff n X).real (ball x R))^(2/p-1)*
        (R^2*energyForm (hausdorff n X) hX.quadratic w.val w.val+
          ‖SobolevSpace.toLp (hausdorff n X) hX.quadratic w.val‖^2) := by
…

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