SmoothingDerivativeBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Smoothing is bounded in every original derivative norm. The bound uses only the input derivative of that order and the fixed kernel L1 norm.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.iterated_smooth_norm_le line 19

Source documentation

Exact derivative commutation gives the scale-independent bound at every order on localized inputs.

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

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

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_weighted_bound line 39
Source documentation
The boundedness part of finite-order smoothing in weighted norms. The weight scale may differ from the kernel scale.
```
theorem smooth_weighted_bound (r : ℕ) {s t C : ℝ} (hs : 0 < s) (ht : 0 < t)
    (m : ℕ) {f : Base → E} (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f)
    (hb : WeightedBound Set.univ t m C f) :
    WeightedBound Set.univ t m ((∫ y, ‖kernel r y‖) * C) (smooth r s f) := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.kernel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth