OAI/Geometry/SurfaceImmersion/Atlas/GoodPhaseStability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A compact good-phase condition persists under a uniform two-jet perturbation.

  1. def OAI.ClosedSurfaceR4.RealModes.secondTensorFromJet line 13
  2. lemma OAI.ClosedSurfaceR4.RealModes.secondTensorFromJet_realTwoJet line 17
  3. lemma OAI.ClosedSurfaceR4.RealModes.contDiffAt_secondTensorFromJet line 20
  4. def OAI.ClosedSurfaceR4.RealModes.goodJetPhase line 32
  5. lemma OAI.ClosedSurfaceR4.RealModes.isOpen_goodJetPhase line 35
  6. theorem OAI.ClosedSurfaceR4.RealModes.compact_good_phase_stability line 49

    Source documentation

    The radius depends on the fixed immersion, phase and compact set, and is independent of all higher derivatives of the perturbed map.

    theorem compact_good_phase_stability {F : RField 4} (hF : ContDiff ℝ ∞ F)
    {φ : Base → ℝ} (hφ : ContDiff ℝ ∞ φ) (K : TopologicalSpace.Compacts Base)
    (hImm : ∀ p ∈ (K : Set Base), Function.Injective (fderiv ℝ F p))
    (hgood : ∀ p ∈ (K : Set Base), Good (realSecondTensor F p) (phaseDerivative φ p)) :
    ∃ ε : ℝ, 0 < ε ∧ ∀ G : RField 4,
      (∀ p ∈ (K : Set Base), ‖realTwoJet G p - realTwoJet F p‖ < ε) →
      ∀ p ∈ (K : Set Base), Function.Injective (fderiv ℝ G p) ∧
        Good (realSecondTensor G p) (phaseDerivative φ p) := by
…

    Mentions: OAI.ClosedSurfaceR4.RealModes.RField, OAI.ClosedSurfaceR4.RealModes.realSecondTensor, OAI.ClosedSurfaceR4.phaseDerivative, OAI.ClosedSurfaceR4.RealModes.realTwoJet