OAI/Geometry/RCD/Sobolev/NoEulerCountersequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.no_euler_countersequence line 23

   Source documentation

   There is no normalized orthogonal Euler countersequence satisfying the actual analytic preconditions of Ambrosio--Honda compactness. The coefficient subsequence is extracted after the joint function limit, so all pairings and the nonzero norm refer to one and the same limit.

   theorem no_euler_countersequence {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X}
       (hcompact : LocalPoissonHarmonicCompactnessInput hX) (hn : 2 ≤ n)
       {S : ℝ} (hS : 0 < S) (q : RadialCompactnessSequence hX S)
       (B : ℕ → ℝ)
       (hf : ∀ i, ∀ᵐ x ∂(hausdorff n X).restrict (ball (q.center i) (S * q.radius i)),
         localGamma (hausdorff n X) hX.quadratic (q.radialFunction i) (q.radialFunction i) x ≤ B i)
       (e : ℕ → SobolevSpace (hausdorff n X) hX.quadratic)
       (b : ℕ → Euclidean n) (k : ℕ → ℝ) {C : ℝ} (hcoeff : ∀ i, ‖b i‖ + |k i| ≤ C)
       (he : Tendsto (fun 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)) (e i))‖)
         atTop (𝓝 0))
   …

   Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalPoissonHarmonicCompactnessInput, OAI.RegularPointCoordinates.RadialCompactnessSequence, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.localGamma, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.normalizeLocalL2, OAI.RegularPointCoordinates.SobolevSpace.restrictLp