SubsolutionSmallNorm.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Small normalized L² mass bounds a weak subsolution on the half ball

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.subsolution_small_l2_upper_bound line 16

Source documentation

Vanishing level energies imply the upper bound on the fixed half ball.

theorem NoncollapsedRCD.subsolution_small_l2_upper_bound {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) (Λ : ℝ) (hΛ : 0 ≤ Λ) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (x : X) (R : ℝ), 0 < R → -1 ≤ K*R^2 →
      ∀ (u : SobolevSpace (hausdorff n X) hX.quadratic) (a : ℝ), 0 ≤ a → a*R^2 ≤ Λ →
      IsWeakSubsolutionOn (hausdorff n X) hX.quadratic (ball x R) u a →
      (∫ y in ball x R, (SobolevSpace.toLp (hausdorff n X) hX.quadratic u y)^2
        ∂hausdorff n X) ≤ δ*(hausdorff n X).real (ball x R) →
      ∀ᵐ y ∂(hausdorff n X).restrict (ball x (R/2)),
        SobolevSpace.toLp (hausdorff n X) hX.quadratic u y ≤ 1 := by
…

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