SubsolutionLevelMoment.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Sobolev moments of upper-level weak subsolutions

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.subsolution_level_cutoff_moment line 19

Source documentation

The extra potential is controlled by the gap from a preceding level. This is the moment estimate used in the local Bochner iteration.

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

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