NormalizedSobolevMoment.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A superquadratic moment for normalized Dirichlet functions

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.normalized_dirichlet_moment line 21

Source documentation

The dyadic support estimate improves the exponent above two. Only the annulus, bounded rescaled curvature, and unit energy normalization are needed; all constants precede the center and radius.

theorem NoncollapsedRCD.normalized_dirichlet_moment {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) :
    ∃ p C : ℝ, 2 < p ∧ 0 < C ∧ ∀ (x : X) (R : ℝ), 0 < R → -1 ≤ K*(2*R)^2 →
      2*(hausdorff n X).real (ball x R) ≤ (hausdorff n X).real (ball x (2*R)) →
      ∀ w : SobolevSpace.dirichlet (hausdorff n X) hX.quadratic (ball x R),
      R^2*energyForm (hausdorff n X) hX.quadratic w.val w.val ≤
        (hausdorff n X).real (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) ≤ C*(hausdorff n X).real (ball x R) := by
…

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