OAI/Geometry/SurfaceImmersion/Atlas/GoodPhaseNeighborhood.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.continuous_phaseDerivative line 12
2. theorem OAI.ClosedSurfaceR4.PhaseGeometry.exists_good_phase_neighborhood line 19

   Source documentation

   A good phase at an immersed point has an actual smaller phase chart with compact source and target bounds inside a larger good-mode domain.

   theorem exists_good_phase_neighborhood {F : RField 4} (hF : ContDiff ℝ ∞ F)
       {φ : Base → ℝ} (hφ : ContDiff ℝ ∞ φ) {p : Base}
       (hImm : Function.Injective (fderiv ℝ F p))
       (hgood : Good (realSecondTensor F p) (phaseDerivative φ p)) :
       ∃ (d : OpenPartialHomeomorph Base Base) (KE KV Ω : Set Base),
         p ∈ d.source ∧ (∀ x, (d x).1 = φ x) ∧
         ContDiff ℝ ∞ d ∧ ContDiff ℝ ∞ d.symm ∧
         IsCompact KE ∧ IsCompact KV ∧ d.source ⊆ KE ∧ d.target ⊆ KV ∧ KV ⊆ Ω ∧
         RealModeDomain (F ∘ d.symm) Ω := by
   …

   Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.Good, OAI.ClosedSurfaceR4.phaseDerivative