OAI/Geometry/SurfaceImmersion/Correction/SmoothingFirstMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

First-moment control of the error of the actual convolution operator.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.firstMoment line 14
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.firstMoment_nonneg line 16
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.firstMoment_dilate line 19
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_sub_norm_le line 40

    Source documentation

    The smoothing error loses one derivative and gains one power of its scale.

    theorem smooth_sub_norm_le (r : ℕ) {s C : ℝ} (hs : 0 < s)
    {f : Base → E} (hf : ContDiff ℝ ∞ f)
    (hb : ∀ x, ‖fderiv ℝ f x‖ ≤ C) (x : Base) :
    ‖f x - smooth r s f x‖ ≤ s * firstMoment (kernel r) * C := by
…

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