OAI/Geometry/RCD/Harmonic/ReplaceHarmonicSequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RegularPointCoordinates.RadialCompactnessSequence.with_harmonic line 20

   Source documentation

   The radial and coordinate convergence data remain unchanged when an arbitrary normalized harmonic sequence replaces the harmonic member. The local energy bound follows from Jiang's published interior estimate.

   def RadialCompactnessSequence.with_harmonic {K : ℝ} {n : ℕ}
       {hX : NoncollapsedRCD K n X} {S : ℝ} (q : RadialCompactnessSequence hX S)
       (hgradient : LocalHarmonicL2GradientInput hX) (hn : 2 ≤ n) (hS : 0 < S)
       (w : ℕ → SobolevSpace (hausdorff n X) hX.quadratic)
       (hw : ∀ i, IsSobolevHarmonicOn (hausdorff n X) hX.quadratic
         (ball (q.center i) (S * q.radius i)) (w i))
       (hwnorm : ∀ i, ‖normalizeLocalL2 (hausdorff n X) (ball (q.center i) (S * q.radius i))
         (ne_of_lt (hX.finiteOnBounded _ isBounded_ball))
         (SobolevSpace.restrictLp (hausdorff n X) hX.quadratic
           (ball (q.center i) (S * q.radius i)) (w i))‖ ≤ 1) :
       RadialCompactnessSequence hX S where
   …

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