HarmonicAffineSequence.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Harmonic affine improvement along an actual RCD rescaling sequence

structure OAI.RegularPointCoordinates.HarmonicCompactnessSequence line 18
Source documentation
The local bounds and measured approximations appearing in the published harmonic-compactness input, bundled for subsequence restriction.
```
structure HarmonicCompactnessSequence {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (S : ℝ) where
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD
def OAI.RegularPointCoordinates.HarmonicCompactnessSequence.subsequence line 51
Source documentation
Restricting to an increasing subsequence preserves precisely the analytic and geometric hypotheses of local harmonic compactness.
```
def subsequence (d : HarmonicCompactnessSequence hX S) (s : ℕ → ℕ) (hs : StrictMono s) :
    HarmonicCompactnessSequence hX S where
…
```
Mentions: OAI.RegularPointCoordinates.HarmonicCompactnessSequence
def OAI.RegularPointCoordinates.HarmonicCompactnessSequence.residualNorm line 71

theorem OAI.RegularPointCoordinates.HarmonicCompactnessSequence.eventual_affine_contraction line 83

Source documentation

Actual local harmonic compactness gives the affine contraction for all sufficiently late members of each admissible rescaling sequence.

theorem eventual_affine_contraction (hcompact : LocalHarmonicMomentCompactnessInput hX)
    {m : ℕ} (hm : 3 ≤ m)
    (hmodel : ∀ S : ℝ, 0 < S → ∀ w : EuclideanHarmonicModel n S,
      ∃ (c : ℝ) (v : Euclidean n), ∃ hρS : (1 / 2 : ℝ) ^ m * S ≤ S,
        ‖∑ i, affineErrorCoefficients c (fun j => v j) i • w.moments hρS i‖ <
          (1 / 4 : ℝ) * (1 / 2 : ℝ) ^ m * Real.sqrt ((1 / 2 : ℝ) ^ m))
    (hS : 0 < S) (d : HarmonicCompactnessSequence hX S) :
    ∀ᶠ k in atTop, d.residualNorm ((1 / 2 : ℝ) ^ m * S) k <
      (1 / 2 : ℝ) * (1 / 2 : ℝ) ^ m * Real.sqrt ((1 / 2 : ℝ) ^ m) := by
…

Mentions: OAI.RegularPointCoordinates.LocalHarmonicMomentCompactnessInput, OAI.RegularPointCoordinates.EuclideanHarmonicModel, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.affineErrorCoefficients, OAI.RegularPointCoordinates.HarmonicCompactnessSequence