C1ManifoldSmoothing.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Smoothing C1 maps on the fixed finite surface atlas.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.localize_C1 line 18
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.restore_C1 line 37
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.smooth_C1_input line 62
Source documentation
The already defined first-order finite smoother is smooth even when its input map has only one derivative.
```
lemma smooth_C1_input {s : ℝ} (hs : 0 < s) {f : M → V}
    (hf : ContMDiff planeModel 𝓘(ℝ, V) 1 f) :
    ContMDiff planeModel 𝓘(ℝ, V) ∞ (A.smooth 1 s f) := by
…
```
Mentions: OAI.ClosedSurfaceR4.planeModel
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.C1Bound line 78
Source documentation
The value and derivative bounds used to preserve immersion under smoothing.
```
def C1Bound (C : ℝ) (f : M → V) : Prop :=
…
```
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.restoration_C1_bound line 83

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.smooth_C1_approximation line 126

Source documentation

The fixed atlas smoother converges in C1 for C1 input maps.

theorem smooth_C1_approximation {f : M → V}
    (hf : ContMDiff planeModel 𝓘(ℝ,V) 1 f) {ε : ℝ} (hε : 0 < ε) :
    ∃ η : ℝ, 0 < η ∧ ∀ s : ℝ, 0 < s → s < η →
      ContMDiff planeModel 𝓘(ℝ,V) ∞ (A.smooth 1 s f) ∧
      A.C1Bound ε (A.smooth 1 s f-f) := by
…

Mentions: OAI.ClosedSurfaceR4.planeModel