OAI/Geometry/SurfaceImmersion/Atlas/PhaseChartGeometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.phaseDerivative_comp_smooth line 13
2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.inverse_chart_derivative line 23
3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.inverse_chart_derivative_injective line 32
4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.inverse_chart_phase_covector line 42
5. theorem OAI.ClosedSurfaceR4.PhaseGeometry.realModeDomain_smooth_phase_chart line 57

   Source documentation

   A nonlinear first-coordinate chart carries precisely the good direction needed by the local free and forced mode constructions.

   theorem realModeDomain_smooth_phase_chart {F : RField 4} (hF : ContDiff ℝ ∞ F)
       {φ : Base → ℝ} (hφ : ContDiff ℝ ∞ φ)
       (e : OpenPartialHomeomorph Base Base) (he : ContDiff ℝ ∞ e) (hi : ContDiff ℝ ∞ e.symm)
       (hphase : ∀ x, (e x).1 = φ x)
       (hImm : ∀ x ∈ e.source, Function.Injective (fderiv ℝ F x))
       (hgood : ∀ x ∈ e.source, Good (realSecondTensor F x) (phaseDerivative φ x)) :
       RealModeDomain (F ∘ e.symm) e.target := by
   …

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