OAI/Geometry/SurfaceImmersion/Correction/ManifoldSmoothing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual smoothing maps on a closed surface, assembled from a fixed atlas.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.restore line 18
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.restore_smooth line 21
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.restore_sub line 33
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.smooth line 44

    Source documentation

    The actual global operator; no choice in its definition depends on f.

    def smooth (r : ℕ) (s : ℝ) (f : M → V) : M → V :=
…
  5. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.error line 48

    Source documentation

    The corresponding global error, written entirely in coordinate residuals.

    def error (r : ℕ) (s : ℝ) (f : M → V) : M → V :=
…
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.smooth_smooth line 53
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.restore_localize line 67
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.sum_restore_localize line 80
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.sub_smooth_eq_error line 89

    Source documentation

    Global smoothing error is exactly the sum of the localized residuals. This identity is the link for transporting the coordinate tail estimates.

    lemma sub_smooth_eq_error (r : ℕ) (s : ℝ) (f : M → V) :
    f - A.smooth r s f = A.error r s f := by
…