NormalizedL2SobolevMoment.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A superquadratic moment under energy and L² normalization

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.normalized_dirichlet_l2_moment line 19

Source documentation

The dyadic tail estimate needs only energy and L² normalization. An exterior annulus is unnecessary when the L² bound is retained.

theorem NoncollapsedRCD.normalized_dirichlet_l2_moment {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),
      ‖SobolevSpace.toLp (hausdorff n X) hX.quadratic w.val‖^2 ≤
        (hausdorff n X).real (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.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm