OAI/Geometry/SurfaceImmersion/Correction/BundleSmoothingIdentity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact reconstruction and error identities for bundle smoothing.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleRestore_sub line 25
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleRestore_localize line 32
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundle_sum_restore_localize line 46
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundle_smoothing_error line 52

    Source documentation

    The smoothing tail is exactly the finite restoration of coordinate tails.

    theorem bundle_smoothing_error (r : ℕ) (s : ℝ) (u : ∀ x, E x) (x : M) :
    u x - A.bundleSmooth e r s u x =
      ∑ i : A.centers, A.bundleRestore e i (residual s r (A.bundleLocalize e i u)) x := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.residual