SmoothingC1Approximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform approximation of C1 coordinate maps by the existing smooth kernel.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.fderiv_smooth_C1 line 16
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_uniform_approximation line 32
Source documentation
Uniform continuity suffices for uniform convergence of the signed finite-moment kernel. Positivity of the kernel is not required.
```
theorem smooth_uniform_approximation (r : ℕ) {f : Base → E}
    (hf : UniformContinuous f) {ε : ℝ} (hε : 0 < ε) :
    ∃ η : ℝ, 0 < η ∧ ∀ s : ℝ, 0 < s → s < η →
      ∀ x : Base, ‖smooth r s f x-f x‖ ≤ ε := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_C1_approximation line 85

Source documentation

Compactly supported C1 maps have smooth approximants converging uniformly both as maps and in their first derivatives.

theorem smooth_C1_approximation (r : ℕ) {f : Base → E}
    (hf : ContDiff ℝ 1 f) (hfc : HasCompactSupport f) {ε : ℝ} (hε : 0 < ε) :
    ∃ η : ℝ, 0 < η ∧ ∀ s : ℝ, 0 < s → s < η →
      ContDiff ℝ ∞ (smooth r s f) ∧
      ∀ x, ‖smooth r s f x-f x‖ ≤ ε ∧
        ‖fderiv ℝ (smooth r s f) x-fderiv ℝ f x‖ ≤ ε := by
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth