SmoothingResidualOperator.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bounds in unchanged derivative norms for repeated residual operators.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual_bounded line 17
Source documentation
The residual operator is bounded in the original norm, independently of its smoothing scale.
```
theorem residual_bounded {s C : ℝ} (hs : 0 < s) (n : ℕ)
    {f : Base → E} (hb : ∀ x, ‖f x‖ ≤ C) (x : Base) :
    ‖residual s n f x‖ ≤ (1 + ∫ y, ‖kernel 0 y‖) ^ n * C := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.iterated_residual_bounded line 32

Source documentation

Repeated residuals are bounded in every original derivative norm.

theorem iterated_residual_bounded {s C : ℝ} (hs : 0 < s) (n m : ℕ)
    {f : Base → E} (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f)
    (hb : ∀ x, ‖iteratedFDeriv ℝ m f x‖ ≤ C) (x : Base) :
    ‖iteratedFDeriv ℝ m (residual s n f) x‖ ≤
      (1 + ∫ y, ‖kernel 0 y‖) ^ n * C := by
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel