OAI/Geometry/RCD/Sobolev/PoissonHarmonicLimitSubsequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.PoissonHarmonicLimit.subsequence line 17

   Source documentation

   All value moments and radial gradient tests retain the SAME model under any later strictly increasing subsequence.

   theorem PoissonHarmonicLimit.subsequence {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
       {S : ℝ} {p : ℕ → X} {r : ℕ → ℝ}
       {u : ℕ → Fin n → SobolevSpace (hausdorff n X) hX.quadratic}
       {V : ℕ → X → Euclidean n} {w f : ℕ → SobolevSpace (hausdorff n X) hX.quadratic}
       {model : EuclideanHarmonicModel n S} (h : PoissonHarmonicLimit hX S p r u V w f model)
       (t : ℕ → ℕ) (ht : StrictMono t) :
       PoissonHarmonicLimit hX S (p ∘ t) (r ∘ t) (u ∘ t) (V ∘ t) (w ∘ t) (f ∘ t) model := by
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.EuclideanHarmonicModel, OAI.RegularPointCoordinates.PoissonHarmonicLimit