SmoothingGain.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Scale-exact derivative gains for convolution by the constructed kernels.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.norm_iterated_dilate line 13
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.integral_norm_iterated_dilate line 26
theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_derivative_gain line 41
Source documentation
An arbitrarily high output derivative is bounded by the zeroth input norm and the corresponding fixed kernel derivative mass.
```
theorem smooth_derivative_gain (r n : ℕ) {s C : ℝ} (hs : 0 < s)
    {f : Base → E} (hf : Continuous f) (hb : ∀ x, ‖f x‖ ≤ C) (x : Base) :
    ‖iteratedFDeriv ℝ n (smooth r s f) x‖ ≤
      (s ^ n)⁻¹ * (∫ y, ‖iteratedFDeriv ℝ n (kernel r) y‖) * C := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel