OAI/Geometry/SurfaceImmersion/Correction/SmoothingResidual.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Iterated smoothing residuals give arbitrary finite approximation order.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual line 15
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_compact line 19
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual_smooth line 23
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual_compact line 29
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.fderiv_residual line 36

    Source documentation

    Differentiation commutes with every finite residual.

    lemma fderiv_residual {s : ℝ} (hs : 0 < s) (n : ℕ) {f : Base → E}
    (hf : ContDiff ℝ ∞ f) (hfc : HasCompactSupport f) :
    fderiv ℝ (residual s n f) = residual s n (fderiv ℝ f) := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual