ShrinkingAtlasWeightBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed atlas bounds for an entire compact box of actual smaller-radius weights.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.shrinking_weight_atlas_bounds line 19
Source documentation
All finite derivative bounds are fixed before selecting the new radius.
```
theorem shrinking_weight_atlas_bounds (i : A.centers) {r0 R : ℝ}
    (hreg0 : circularCoordinateRegion (i : M) r0 ⊆ (coordinateChart (i : M)).target)
    (hR : R^2 < r0^2) :
    ∃ C : ℕ → ℝ, (∀ m, 0 ≤ C m) ∧ ∀ r : ℝ, r^2 ≤ R^2 →
      ∀ m, A.WeightedBound 1 m (C m) (shrinkingCircularWeight (i : M) (A.weight i) r0 r) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight