OAI/Geometry/RCD/Harmonic/RadialCompactnessSequence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The concrete sequence data for the sharp projection argument

  1. structure OAI.RegularPointCoordinates.RadialCompactnessSequence line 17

    Source documentation

    All analytic preconditions of the published local compactness theorem. No projected Euler equation or affine approximation is part of this data.

    structure RadialCompactnessSequence {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) (S : ℝ) where
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD

  2. theorem OAI.RegularPointCoordinates.LocalPoissonHarmonicCompactnessInput.extract_sequence line 59