ShrinkingWeightBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite-order coordinate bounds for the actual radius family.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_parameter_slice_bounds line 14

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingWeight_coordinate_bounds line 61

Source documentation

One globally smooth coordinate multiplier represents all smaller ratio weights; its product with the circular bump has uniform finite-order bounds.

theorem shrinkingWeight_coordinate_bounds (p : M) (w : M → ℝ)
    (hw : ContMDiff planeModel 𝓘(ℝ) ∞ w) {r0 R : ℝ}
    (hreg0 : circularCoordinateRegion p r0 ⊆ (coordinateChart p).target)
    (hR : R^2 < r0^2) :
    ∃ a : SmallModes.Base → ℝ, ContDiff ℝ ∞ a ∧
      (∀ r : ℝ, r^2 ≤ R^2 → ∀ x ∈ (coordinateChart p).target,
        shrinkingCircularWeight p w r0 r ((coordinateChart p).symm x) =
          a x * circularFlatBump (coordinateChart p p) r x) ∧
      ∃ C : ℕ → ℝ, (∀ m, 0 ≤ C m) ∧ ∀ r : ℝ, r^2 ≤ R^2 →
        ∀ m, WeightedBound univ 1 m (C m)
          (fun x => a x * circularFlatBump (coordinateChart p p) r x) := by
…

Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight