AtlasCorrectionLimit.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual fixed-atlas correction bounds imply a smooth manifold limit and convergence of the manifold differentials.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.exists_weight_ne_zero line 24
Source documentation
Every point is seen by at least one genuine partition weight.
```
lemma exists_weight_ne_zero (p : M) : ∃ i : A.centers, A.weight i p ≠ 0 := by
…
```
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.vectorPlaneRead_coordinateChart_of_outer_one line 35
Source documentation
Where its outer cutoff is one, the coordinate representative agrees with the original map, for every map simultaneously.
```
lemma vectorPlaneRead_coordinateChart_of_outer_one (i : A.centers) (V : M → Space)
    {x : M} (hx : x ∈ (chart (i : M)).source) (ho : A.outer i x = 1) :
    V x = A.vectorPlaneRead i V (coordinateChart (i : M) x) := by
…
```
Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.coordinateChart

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.correction_limit line 44

Source documentation

The global atlas norm can be used directly; the summable bound only has to hold eventually for each fixed derivative order.

theorem correction_limit
    {F : M → Space} {U : ℕ → M → Space} {ρ : ℕ → ℝ}
    (hF : ContMDiff planeModel spaceModel ∞ F)
    (hU : ∀ n, ContMDiff planeModel spaceModel ∞ (U n))
    (hρ : Summable ρ)
    (hbound : ∀ m : ℕ, ∀ᶠ n in atTop, A.WeightedBound 1 m (ρ n) (U n))
    (houter : ∀ i x, x ∈ tsupport (A.weight i) →
      A.outer i =ᶠ[𝓝 x] (fun _ => 1)) :
    ContMDiff planeModel spaceModel ∞ (manifoldLimitMap F U) ∧
      ∀ p, Tendsto (fun N => mfderiv planeModel spaceModel (manifoldPartialMap F U N) p)
        atTop (𝓝 (mfderiv planeModel spaceModel (manifoldLimitMap F U) p)) := by
…

Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel