ShrinkingWeightMultiplier.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed smooth multiplier for a whole compact range of smaller radii. This removes the apparent moving denominator from all derivative estimates.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_shrinkingWeight_multiplier line 18
Source documentation
The ratio-cutoff family is multiplication by one fixed smooth function on every smaller radius box. Constants for that multiplier are chosen before any radius in the box.
```
theorem exists_shrinkingWeight_multiplier (p : M) (w : M → ℝ)
    (hw : ContMDiff planeModel 𝓘(ℝ) ∞ w) {r0 R : ℝ}
    (hreg0 : circularCoordinateRegion p r0 ⊆ (coordinateChart p).target)
    (hR : R^2 < r0^2) :
    ∃ a : M → ℝ, ContMDiff planeModel 𝓘(ℝ) ∞ a ∧
      tsupport a ⊆ circularCoordinateDisk p r0 ∧
      ∀ r : ℝ, r^2 ≤ R^2 → shrinkingCircularWeight p w r0 r =
        fun x => a x * circularManifoldBump p r x := by
…
```
Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateDisk, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularManifoldBump