HarmonicLevelMoment.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A superquadratic moment for harmonic upper-level cutoff functions

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.harmonic_level_cutoff_moment line 19

Source documentation

Caccioppoli and the relative Sobolev estimate give a moment bound for the actual cutoff of each harmonic upper-level part.

theorem NoncollapsedRCD.harmonic_level_cutoff_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 →
      ∀ u : SobolevSpace (hausdorff n X) hX.quadratic,
      IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball x R) u →
      ∀ k : ℝ, 0 ≤ k → ∀ (χ : X → ℝ) (L : ℝ≥0),
      LipschitzWith L χ → HasCompactSupport χ →
      (∀ y, |χ y| ≤ (1:ℝ≥0)) → (∀ y, 0 ≤ χ y) →
      tsupport χ ⊆ ball x R → ∀ A : Set X, MeasurableSet A → tsupport χ ⊆ A →
      ∃ w : SobolevSpace.dirichlet (hausdorff n X) hX.quadratic (ball x R),
        (SobolevSpace.toLp (hausdorff n X) hX.quadratic w.val =ᵐ[hausdorff n X]
          fun y => χ y*max (SobolevSpace.toLp (hausdorff n X) hX.quadratic u y-k) 0) ∧
…

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