OAI/Geometry/SurfaceImmersion/Correction/BundleSmoothing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

An actual finite-atlas smoothing operator on smooth vector-bundle sections.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleComponent line 28

    Source documentation

    Fiber coordinates, used only on the corresponding base chart.

    def bundleComponent (i : A.centers) (u : ∀ x, E x) (x : M) : F :=
…
  2. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleLocalize line 31
  3. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleRestore line 34
  4. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleSmooth line 37
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleComponent_smooth_on line 43
  6. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleLocalize_smooth line 55
  7. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleRestore_smooth line 63
  8. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleSmooth_smooth line 79

    Source documentation

    Smoothing produces a smooth section of the original bundle.

    theorem bundleSmooth_smooth (r : ℕ) {s : ℝ} (hs : 0 < s) {u : ∀ x, E x}
    (hu : ContMDiff planeModel (planeModel.prod 𝓘(ℝ, F)) ∞
      (fun x => TotalSpace.mk' F x (u x))) :
    ContMDiff planeModel (planeModel.prod 𝓘(ℝ, F)) ∞
      (fun x => TotalSpace.mk' F x (A.bundleSmooth e r s u x)) := by
…

    Mentions: OAI.ClosedSurfaceR4.planeModel