AtlasMetricJetMargins.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform first-jet geometry of approximate isometries in a fixed atlas.

lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.modeSupport_subset_coordinateDomain line 29
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.metricPlaneRead_on_support line 37

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.metric_firstJet_margin line 49

Source documentation

The constants depend on the prescribed metric and fixed atlas, not on any derivatives of the approximate immersion.

theorem metric_firstJet_margin (g : SmoothMetric M) :
    ∃ ε R c : ℝ, 0 < ε ∧ 0 < R ∧ 0 < c ∧
      ∀ V : M → Space, ContMDiff planeModel spaceModel ∞ V →
      ∀ b : ℝ, 0 ≤ b → b < ε →
      A.TensorWeightedBound 1 0 b (inducedTensor V-g.inner) →
      ∀ i x, x ∈ (modeSupport (A.chartWeightCompact i) : Set SmallModes.Base) →
      ‖firstJetPair (spaceCoordinates ∘ A.vectorPlaneRead i V) x‖ ≤ R ∧
        c ≤ NormalFrame.gramDet
          (firstJetPair (spaceCoordinates ∘ A.vectorPlaneRead i V) x).1
          (firstJetPair (spaceCoordinates ∘ A.vectorPlaneRead i V) x).2 := by
…

Mentions: OAI.ClosedSurfaceR4.SmoothMetric, OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.inducedTensor, OAI.ClosedSurfaceR4.SmallModes.Base, OAI.ClosedSurfaceR4.spaceCoordinates, OAI.ClosedSurfaceR4.NormalFrame.gramDet