PerturbedCircularCutoffs.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual independent radius perturbations of circular manifold cutoffs. A fixed larger disk supplies common support and uniform continuity.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion_mono line 16
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularDiskClosure_mono line 22
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularManifoldBump_zero_off_larger_disk line 27
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularManifoldBump_joint_continuousAt line 42
Source documentation
The radius and base point vary continuously together, including at the chart boundary where the common compact support forces the cutoff to vanish.
```
lemma circularManifoldBump_joint_continuousAt (p : M) {R r : ℝ}
    (hregion : circularCoordinateRegion p R ⊆ (coordinateChart p).target)
    (hr : |r| < R) (x : M) :
    ContinuousAt (fun z : ℝ × M => circularManifoldBump p z.1 z.2) (r,x) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularManifoldBump
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularManifoldBump_uniform_perturbation line 79
Source documentation
Moving one radius slightly gives an actual smooth cutoff with one fixed compact support and arbitrarily small global C0 error. The radius may be chosen independently for each member of a later finite family.
```
theorem circularManifoldBump_uniform_perturbation (p : M) {R r : ℝ}
    (hregion : circularCoordinateRegion p R ⊆ (coordinateChart p).target)
    (hr : |r| < R) {eps : ℝ} (heps : 0 < eps) :
    ∃ delta : ℝ, 0 < delta ∧ ∀ r' : ℝ, |r'-r| < delta →
      |r'| < R ∧ ContMDiff planeModel 𝓘(ℝ) ∞ (circularManifoldBump p r') ∧
      tsupport (circularManifoldBump p r') ⊆ circularDiskClosure p R ∧
      ∀ x : M, |circularManifoldBump p r' x-circularManifoldBump p r x| < eps := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularCoordinateRegion, OAI.ClosedSurfaceR4.coordinateChart, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularManifoldBump, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.circularDiskClosure