FiniteSmootherBounds.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds and derivative gain for the same finite-order smoother.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth_bounded line 16

Source documentation

Every original derivative norm remains bounded independently of scale.

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

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

def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gainConstant line 30
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gainConstant_nonneg line 34

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth_gain line 41

Source documentation

A gain of m derivatives uses just the zeroth input norm.

theorem finiteSmooth_gain (n m : ℕ) {s C : ℝ} (hs : 0 < s)
    {f : Base → E} (hf : ContDiff ℝ ∞ f) (hb : ∀ x, ‖f x‖ ≤ C) (x : Base) :
    ‖iteratedFDeriv ℝ m (finiteSmooth n s f) x‖ ≤
      (s ^ m)⁻¹ * gainConstant n m * C := by
…

Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gainConstant

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth_gain_from_derivatives line 65
Source documentation
Additional output derivatives cost the smoothing scale, while the original q input derivatives commute through the same operator.
```
theorem finiteSmooth_gain_from_derivatives (n q m : ℕ) {s C : ℝ} (hs : 0 < s)
    {f : Base → E} (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f)
    (hb : ∀ x, ‖iteratedFDeriv ℝ q f x‖ ≤ C) (x : Base) :
    ‖iteratedFDeriv ℝ (q + m) (finiteSmooth n s f) x‖ ≤
      (s ^ m)⁻¹ * gainConstant n m * C := by
…
```
Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.gainConstant