OAI/Geometry/SurfaceImmersion/Primitive/AtlasBoundaryProfile.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Read the exact immersion's five profiles in the real coordinate chart used by the Gauss and boundary calculations.

  1. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.realChartMap line 18
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.realChartMap_smooth line 21
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.realChartMap_profile line 26
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.realChartMap_profile_error line 41

    Source documentation

    The exact primitive's Euclidean profile estimate gives the real-coordinate estimate used by the boundary preservation lemmas.

    lemma realChartMap_profile_error (i : A.centers) {F : M → Space}
    (hF : ContMDiff planeModel spaceModel ∞ F) (z : ℝ) (p : JetPolynomial.Base)
    (J : EuclideanBoundaryProfile) {ε : ℝ} (hε : 0 < ε)
    (hclose : ‖SurfaceVelocityFamily.Loop.primitiveJetProfile (A.vectorChartRead i F) z p - J‖ <
      ε / (‖boundaryProfileMap‖ + 1)) :
    ‖realBoundaryProfile (A.realChartMap i F) z (baseEquiv p) - boundaryProfileMap J‖ < ε := by
…

    Mentions: OAI.ClosedSurfaceR4.Space, OAI.ClosedSurfaceR4.planeModel, OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.primitiveJetProfile