OAI/Geometry/SurfaceImmersion/Atlas/BundleCutoffCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Reading a section with an arbitrary compact chart cutoff is bounded by its atlas norm. This allows phase patches to use unweighted tensor values.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleCutoff line 27
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleCutoff_restore line 32
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleCutoff_smooth line 55
  4. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.bundleCutoff_bound line 65

    Source documentation

    Cutoff coordinates lose no derivatives and have constants independent of both the section and its weighted scale.

    theorem bundleCutoff_bound (i : A.centers) {ψ : M → ℝ}
    (hψ : ContMDiff planeModel 𝓘(ℝ) ∞ ψ)
    (hsupp : tsupport ψ ⊆ (chart (i : M)).source) (m : ℕ) :
    ∃ D : ℝ, 0 ≤ D ∧ ∀ (u : ∀ x, E x) (s C : ℝ),
      0 < s → s ≤ 1 → 0 ≤ C →
      ContMDiff planeModel (planeModel.prod 𝓘(ℝ, F)) ∞
        (fun x => TotalSpace.mk' F x (u x)) → A.BundleWeightedBound e s m C u →
      WeightedBound univ s m (D * C) (A.bundleCutoff e i ψ u) := by
…

    Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.chart, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.WeightedBound