LocalZeroSetCoercivity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Local coercivity for functions with a large zero set

The zero set controls the constant in the local Poincare estimate. This is the local ingredient for the support-sensitive Sobolev estimate.

theorem OAI.RegularPointCoordinates.integral_sq_le_six_variance line 17

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_zero_set_coercivity line 55

Source documentation

Under bounded rescaled curvature, a zero set occupying at least half of the ball removes the additive constant, uniformly in its center.

theorem NoncollapsedRCD.local_zero_set_coercivity {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) {κ : ℝ} (hκ : 0 ≤ κ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (p : X) (r : ℝ), 0 < r → -κ ≤ K*r^2 →
      ∀ w : SobolevSpace (hausdorff n X) hX.quadratic,
      ∀ B : Set X, MeasurableSet B → B ⊆ ball p r →
      (hausdorff n X).real (ball p r) ≤ 2*(hausdorff n X).real B →
      (SobolevSpace.toLp (hausdorff n X) hX.quadratic w =ᵐ[
        (hausdorff n X).restrict B] 0) →
      (∫ x in ball p r, (SobolevSpace.toLp (hausdorff n X) hX.quadratic w x)^2
        ∂hausdorff n X) ≤ C*r^2 *
        ∫ x in ball p (8*r), localGamma (hausdorff n X) hX.quadratic w w x
          ∂hausdorff n X := by
…

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