HarmonicLevelDecay.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Vanishing harmonic upper-level energies on shrinking balls

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.harmonic_level_energies_tendsto_zero line 18

Source documentation

Small normalized L² mass forces geometric decay of the upper-level energies, with constants independent of the ball.

theorem NoncollapsedRCD.harmonic_level_energies_tendsto_zero {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (hn : 2 ≤ n) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (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 in ball x R, (SobolevSpace.toLp (hausdorff n X) hX.quadratic u y)^2
        ∂hausdorff n X) ≤ δ*(hausdorff n X).real (ball x R) →
      Tendsto (fun i : ℕ => ∫ y in closedBall x (R/2+R/(4*2^i)),
        (max (SobolevSpace.toLp (hausdorff n X) hX.quadratic u y-(1-(2^i:ℝ)⁻¹)) 0)^2
          ∂hausdorff n X) atTop (𝓝 0) := by
…

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