OAI/Geometry/SurfaceImmersion/Correction/SmoothPhaseChart.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A noncritical smooth phase is the first coordinate of a smooth local chart.

  1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.phaseLinear_phaseDerivative line 13
  2. theorem OAI.ClosedSurfaceR4.PhaseGeometry.exists_smooth_phase_chart line 24

    Source documentation

    The chart is globally smooth as a function, and its inverse is smooth on its target. Later cutoff extensions can make the inverse globally smooth.

    theorem exists_smooth_phase_chart {φ : Base → ℝ} (hφ : ContDiff ℝ ∞ φ)
    {p : Base} (hp : phaseDerivative φ p ≠ 0) :
    ∃ e : OpenPartialHomeomorph Base Base, p ∈ e.source ∧
      (∀ x, (e x).1 = φ x) ∧ ContDiff ℝ ∞ e ∧ ContDiffOn ℝ ∞ e.symm e.target := by
…

    Mentions: OAI.ClosedSurfaceR4.phaseDerivative