OAI/Geometry/SurfaceImmersion/Primitive/PhaseBoundaryProfile.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.phaseRealChartMap line 18
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseRealChartMap_smooth line 21
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseRealChartMap_profile line 27
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.SmoothingAtlas.phaseRealChartMap_profile_error line 43

    Source documentation

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

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

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