OAI/Geometry/SurfaceImmersion/Atlas/AtlasPhaseChartBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed smooth phases have uniform directional-derivative bounds in every atlas chart.

  1. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phase_chart_gradient_bound line 30

    Source documentation

    The coordinate derivatives used by the polynomial phase estimates obey fixed profiles as the slow scale varies.

    theorem phase_chart_gradient_bound {ι : Type*} [Fintype ι]
    (φ : ι → M → ℝ) (hφ : ∀ a, ContMDiff planeModel 𝓘(ℝ) ∞ (φ a)) (m : ℕ) :
    ∃ P : ℝ, 0 ≤ P ∧ ∀ k a (s : ℝ), 0 ≤ s → s ≤ 1 → ∀ v : Fin 2,
      WeightedEstimates.WeightedBound univ s m P
        (fun x => fderiv ℝ (A.vectorChartRead k (φ a)) x (coordinateVector v)) := by
…

    Mentions: OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.WeightedEstimates.WeightedBound