IndependentShrinkingWeights.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One open box of independent radius choices preserves a finite family of actual circular weights uniformly.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.independent_shrinking_weights line 17

Source documentation

The radius neighborhood is fixed before all independent choices.

theorem independent_shrinking_weights (p : ι → M) (w : ι → M → ℝ) (r0 : ι → ℝ)
    (hw : ∀ i, ContMDiff planeModel 𝓘(ℝ) ∞ (w i))
    (hnon : ∀ i x, 0 ≤ w i x) (hr0 : ∀ i, 0 < r0 i)
    (hreg : ∀ i, circularCoordinateRegion (p i) (r0 i) ⊆ (coordinateChart (p i)).target)
    (hpos : ∀ i x, 0 < w i x ↔ x ∈ circularCoordinateDisk (p i) (r0 i))
    {eps : ℝ} (heps : 0 < eps) :
    ∃ delta : ℝ, 0 < delta ∧ (∀ i, delta ≤ r0 i / 2) ∧ ∀ r : ι → ℝ,
      (∀ i, r0 i-delta < r i ∧ r i < r0 i) →
      (∀ i, 0 < r i) ∧
      (∀ i, ContMDiff planeModel 𝓘(ℝ) ∞ (shrinkingCircularWeight (p i) (w i) (r0 i) (r i))) ∧
      (∀ i x, 0 < shrinkingCircularWeight (p i) (w i) (r0 i) (r i) x ↔
        x ∈ circularCoordinateDisk (p i) (r i)) ∧
…

Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateDisk, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight