OAI/Geometry/RCD/Sobolev/HarmonicSequenceEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.rescaled_harmonic_energy_of_gradient line 19

   Source documentation

   The gradient estimate supplies all the rescaled interior H¹ bounds required by harmonic compactness, uniformly along the sequence.

   theorem rescaled_harmonic_energy_of_gradient {K : ℝ} {n : ℕ}
       {hX : NoncollapsedRCD K n X} (hinput : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n)
       {S : ℝ} (hS : 0 < S) (p : ℕ → X) (r : ℕ → ℝ)
       (hr : ∀ k, 0 < r k) (hcurv : ∀ k, -1 ≤ K * r k ^ 2)
       (w : ℕ → SobolevSpace (hausdorff n X) hX.quadratic)
       (hw : ∀ k, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic
         (ball (p k) (S * r k)) (w k))
       (hnorm : ∀ k, ‖normalizeLocalL2 (hausdorff n X) (ball (p k) (S * r k))
         (ne_of_lt (hX.finiteOnBounded _ isBounded_ball))
         (SobolevSpace.restrictLp (hausdorff n X) hX.quadratic
           (ball (p k) (S * r k)) (w k))‖ ≤ 1) :
       ∀ ρ : ℝ, 0 < ρ → ρ < S → ∃ C : ℝ, 0 ≤ C ∧ ∀ k,
   …

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