ShrinkingWeightContinuity.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform convergence of the actual ratio cutoffs from smaller radii. The upper clamp permits an ordinary product-neighborhood argument at the original radius, including the boundary where numerator and denominator vanish.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularManifoldBump_joint_continuousAt_of_source line 17
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingRadius line 33
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingRadius_bounds line 35
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingRadius_of_mem line 39
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingRadius_continuous line 43
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight_joint_continuousAt_reference line 48
Source documentation
Joint continuity remains valid at a vanishing denominator, because the ratio cutoff lies between zero and the original continuous weight.
```
theorem shrinkingCircularWeight_joint_continuousAt_reference (p : M) (w : M → ℝ)
    (hw : ContMDiff planeModel 𝓘(ℝ) ∞ w) (hnon : ∀ x, 0 ≤ w x) {r0 : ℝ}
    (hr0 : 0 < r0)
    (hreg0 : circularCoordinateRegion p r0 ⊆ (coordinateChart p).target)
    (hpos : ∀ x, 0 < w x ↔ x ∈ circularCoordinateDisk p r0) (x : M) :
    ContinuousAt (fun z : ℝ × M =>
      shrinkingCircularWeight p w r0 (shrinkingRadius r0 z.1) z.2) (r0,x) := by
…
```
Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateDisk, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingRadius

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.shrinkingCircularWeight_uniform_perturbation line 95

Source documentation

Independent smaller radii can be chosen in one left neighborhood while preserving the weight uniformly on the entire compact manifold.

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

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