OAI/Geometry/SurfaceImmersion/Correction/BundleSmoothingTransition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Chart transitions for the actual bundle smoother.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleTransition line 28
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleTransition_smooth line 34
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleLocalize_restore line 43
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundle_pair_weighted_bound line 66

    Source documentation

    Fiber transitions preserve each weighted derivative norm without a scale loss.

    theorem bundle_pair_weighted_bound (i j : A.centers) (m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (h : Base → F) (s C : ℝ),
      0 < s → s ≤ 1 → 0 ≤ C → ContDiff ℝ ∞ h → WeightedBound Set.univ s m C h →
      WeightedBound Set.univ s m (D * C)
        (A.bundleLocalize e i (A.bundleRestore e j h)) := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.WeightedBound