OAI/Geometry/SurfaceImmersion/Atlas/ExtendedPhaseChart.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClosedSurfaceR4.PhaseGeometry.extend_local_chart_inverse line 15

   Source documentation

   Shrinking a smooth local chart lets its inverse be represented by an actual globally smooth function, as needed by the supported mode solver.

   theorem extend_local_chart_inverse (e : OpenPartialHomeomorph Base Base)
       (he : ContDiff ℝ ∞ e) (hi : ContDiffOn ℝ ∞ e.symm e.target)
       {p : Base} (hp : p ∈ e.source) :
       ∃ d : OpenPartialHomeomorph Base Base, p ∈ d.source ∧
         (d : Base → Base) = e ∧ d.source ⊆ e.source ∧ d.target ⊆ e.target ∧
         ContDiff ℝ ∞ d ∧ ContDiff ℝ ∞ d.symm := by
   …

2. theorem OAI.ClosedSurfaceR4.PhaseGeometry.exists_extended_phase_chart line 55

   Source documentation

   Every noncritical phase admits the globally smooth representatives used by local polynomial cancellation. This is a geometric construction.

   theorem exists_extended_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 ∧ ContDiff ℝ ∞ e.symm := by
   …

   Mentions: OAI.ClosedSurfaceR4.phaseDerivative