SmoothingResidualBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary finite approximation order from a finite input derivative bound.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual_norm_le line 17
Source documentation
Applying the smoothing residual n times gains s^n, using just the n-th derivative of the original input.
```
theorem residual_norm_le {s C : ℝ} (hs : 0 < s) (n : ℕ)
    {f : Base → E} (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f)
    (hb : ∀ x, ‖iteratedFDeriv ℝ n f x‖ ≤ C) (x : Base) :
    ‖residual s n f x‖ ≤ (s * firstMoment (kernel 0)) ^ n * C := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.firstMoment, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.iterated_residual_norm_le line 39
Source documentation
The same finite-order approximation estimate in each higher derivative.
```
theorem iterated_residual_norm_le {s C : ℝ} (hs : 0 < s) (n m : ℕ)
    {f : Base → E} (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f)
    (hb : ∀ x, ‖iteratedFDeriv ℝ (n + m) f x‖ ≤ C) (x : Base) :
    ‖iteratedFDeriv ℝ m (residual s n f) x‖ ≤
      (s * firstMoment (kernel 0)) ^ n * C := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.firstMoment, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel