HarmonicUnitMean.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The harmonic L² mean-value bound at unit rescaled curvature

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.harmonic_unit_mean_value line 17

Source documentation

Rescaling the actual harmonic function removes the smallness condition in the level-set argument.

theorem NoncollapsedRCD.harmonic_unit_mean_value {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) :
    ∃ C : ℝ, 1 ≤ 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 →
      ∀ᵐ y ∂(hausdorff n X).restrict (ball x (R/2)),
        |SobolevSpace.toLp (hausdorff n X) hX.quadratic u y| ≤
          C*harmonicTargetNorm hX x R u := by
…

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