OAI/Geometry/RCD/Sobolev/RescaledHarmonicEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput.rescaled_interior_energy line 18

   Source documentation

   The physical radius is S * r, while the compactness energy is normalized by r². The interior estimate supplies the required bound uniformly over every center and every admissible radius.

   theorem LocalHarmonicL2GradientInput.rescaled_interior_energy {K : ℝ} {n : ℕ}
       {hX : NoncollapsedRCD K n X} (hinput : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n)
       {S ρ : ℝ} (hS : 0 < S) (hρ : 0 < ρ) (hρS : ρ < S) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ (p : X) (r : ℝ), 0 < r → -1 ≤ K * r ^ 2 →
         ∀ w : SobolevSpace (hausdorff n X) hX.quadratic,
           IsSobolevHarmonicOn (hausdorff n X) hX.quadratic (ball p (S * r)) w →
           ‖normalizeLocalL2 (hausdorff n X) (ball p (S * r))
             (ne_of_lt (hX.finiteOnBounded _ isBounded_ball))
             (SobolevSpace.restrictLp (hausdorff n X) hX.quadratic (ball p (S * r)) w)‖ ≤ 1 →
           r ^ 2 * ((hausdorff n X).real (ball p (S * r)))⁻¹ *
             (∫ x in ball p (ρ * r), localGamma (hausdorff n X) hX.quadratic w w x
               ∂hausdorff n X) ≤ C := by
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalHarmonicL2GradientInput, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp, OAI.RegularPointCoordinates.localGamma