OAI/Geometry/SurfaceImmersion/Atlas/PhaseChartStability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed good phase chart remains admissible throughout a C2 neighborhood.

  1. lemma OAI.ClosedSurfaceR4.RealModes.norm_realTwoJet_le_on line 16
  2. theorem OAI.ClosedSurfaceR4.RealModes.compact_twoJet_comp_bound line 38
  3. theorem OAI.ClosedSurfaceR4.PhaseGeometry.GoodPhaseChart.uniform_jet_neighborhood line 67

    Source documentation

    The compact jet neighborhood and radius are fixed before the perturbed map, using the smooth inverse of the reference map.

    theorem GoodPhaseChart.uniform_jet_neighborhood {F : RField 4} (hF : ContDiff ℝ ∞ F)
    {φ : Base → ℝ} (c : GoodPhaseChart F φ) :
    ∃ (ρ : ℝ) (Q : Set RealTwoJet), 0 < ρ ∧ IsCompact Q ∧ Q ⊆ admissibleRealJets ∧
      ∀ (G : RField 4), ContDiff ℝ ∞ G → ∀ C : ℝ, 0 ≤ C → C < ρ →
      WeightedBound univ 1 2 C (G-F) →
      MapsTo (realTwoJet (G ∘ c.chart.symm)) c.chart.target Q ∧
        RealModeDomain (G ∘ c.chart.symm) c.chart.target := by
…

    Mentions: OAI.ClosedSurfaceR4.PhaseGeometry.GoodPhaseChart