ShrinkingCircularWeight.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Weight-preserving independent disk shrinkage. The quotient is only used where the original bump is positive; the smaller compact support makes the resulting weight globally smooth.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularManifoldBump_mono_sq line 17
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularDiskClosure_subset_disk line 26
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight line 38
Source documentation
The original weight is recovered at the original radius, even though both circular bumps vanish on and outside its boundary.
```
def shrinkingCircularWeight (p : M) (w : M → ℝ) (r0 r : ℝ) (x : M) : ℝ :=
…
```
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight_nonneg_le line 42
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight_reference line 55
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight_pos_iff line 67
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight_support line 86
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight_smooth line 96
Source documentation
Every strictly smaller radius gives a globally smooth actual weight, with support in the smaller closed disk.
```
theorem shrinkingCircularWeight_smooth (p : M) (w : M → ℝ)
    (hw : ContMDiff planeModel 𝓘(ℝ) ∞ w) {r0 r : ℝ}
    (hreg0 : circularCoordinateRegion p r0 ⊆ (coordinateChart p).target)
    (hr : r^2 < r0^2) :
    ContMDiff planeModel 𝓘(ℝ) ∞ (shrinkingCircularWeight p w r0 r) ∧
      tsupport (shrinkingCircularWeight p w r0 r) ⊆ circularDiskClosure p r := by
…
```
Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularDiskClosure