AtlasCorrectionBudget.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual correction series retains its finite atlas displacement budget.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize_tsum line 18
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.weightedBound_tsum line 31
Source documentation
Bounds at a fixed finite order pass to the actual sum with the sum of the bounds, rather than a larger coordinate-transition constant.
```
theorem weightedBound_tsum {U : ℕ → M → Space} {ρ : ℕ → ℝ} {m : ℕ}
    (hU : ∀ n, ContMDiff planeModel spaceModel ∞ (U n)) (hρ : Summable ρ)
    (hbound : ∀ n, A.WeightedBound 1 m (ρ n) (U n)) :
    A.WeightedBound 1 m (∑' n, ρ n) (fun x => ∑' n, U n x) := by
…
```
Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.increment_c2_bound line 60
Source documentation
Every constructed increment has the zeroth, first, and second derivative budget, including the stages before the order has increased.
```
lemma increment_c2_bound (seed : c.Stage t 0) (n : ℕ) :
    d.A.WeightedBound 1 2 (c.ρ*correctionScale t n)
      (c.increment hF ht htsmall seed n) :=
…
```
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.limit_seed_displacement_bound line 67
Source documentation
The limit remains within the total C² displacement budget of its seed.
```
theorem limit_seed_displacement_bound (seed : c.Stage t 0) :
    d.A.WeightedBound 1 2 (2*c.ρ*t)
      (manifoldLimitMap seed.map (c.increment hF ht htsmall seed)-seed.map) := by
…
```
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.PreparedCorrection.limit_reference_displacement_bound line 88
Source documentation
The initial margin and the convergent correction budget preserve the same fixed C² neighborhood used to construct the entire sequence.
```
theorem limit_reference_displacement_bound (seed : c.Stage t 0) :
    d.A.WeightedBound 1 2 (c.ρ/4)
      (manifoldLimitMap seed.map (c.increment hF ht htsmall seed)-F) := by
…
```