OAI/Geometry/SurfaceImmersion/Atlas/BundleAtlasBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Weighted atlas bounds for section restoration.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.BundleWeightedBound line 25
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleLocalize_sum line 28
  3. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundle_restoration_bound line 41

    Source documentation

    A finite family of local sections can be restored with fixed weighted bounds at every order.

    theorem bundle_restoration_bound (m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (h : A.centers → Base → F) (s C : ℝ),
      0 < s → s ≤ 1 → 0 ≤ C → (∀ i, ContDiff ℝ ∞ (h i)) →
      (∀ i, WeightedBound univ s m C (h i)) →
      A.BundleWeightedBound e s m (D * C)
        (fun x => ∑ i : A.centers, A.bundleRestore e i (h i) x) := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.WeightedBound