OAI/Geometry/SurfaceImmersion/Correction/FiniteSmootherApproximation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite-order smoother approximates using only the displayed finite number of input derivatives.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual_add_orders line 16
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.error_finiteSmooth line 24
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.approximationConstant line 29
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.approximationConstant_nonneg line 32
  5. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.finiteSmooth_approximation line 41

    Source documentation

    The q+j-th error derivative gains s^(r-j), using input derivatives only through q+r. Constants do not depend on the input or the scale.

    theorem finiteSmooth_approximation (r q j : ℕ) (hj : j ≤ r)
    {s C : ℝ} (hs : 0 < s) {f : Base → E}
    (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f)
    (hb : ∀ x, ‖iteratedFDeriv ℝ (q + r) f x‖ ≤ C) (x : Base) :
    ‖iteratedFDeriv ℝ (q + j) (f - finiteSmooth r s f) x‖ ≤
      approximationConstant r j * s ^ (r - j) * C := by
…

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