OAI/Geometry/SurfaceImmersion/Primitive/BoundaryProfileCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The five Euclidean profiles used by the exact primitive determine the canonical normal frame in the real surface coordinates.

  1. abbrev OAI.ClosedSurfaceR4.GeometryPreservation.EuclideanBoundaryProfile line 16
  2. def OAI.ClosedSurfaceR4.GeometryPreservation.boundaryProfileMap line 18
  3. lemma OAI.ClosedSurfaceR4.GeometryPreservation.boundaryProfileMap_apply line 22
  4. lemma OAI.ClosedSurfaceR4.GeometryPreservation.directional_euclidean_chart line 25
  5. lemma OAI.ClosedSurfaceR4.GeometryPreservation.boundaryProfileMap_chart line 37
  6. theorem OAI.ClosedSurfaceR4.GeometryPreservation.compact_euclidean_boundary_stability line 81

    Source documentation

    Transfer the exact primitive's Euclidean error directly into the normal frame and all four second-form coefficients.

    theorem compact_euclidean_boundary_stability {K : Set EuclideanBoundaryProfile}
    (hK : IsCompact K) (hregular : ∀ J ∈ K, boundaryProfileMap J ∈ regularBoundaryProfiles) :
    ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧
      ∀ J ∈ K, ∀ H : EuclideanBoundaryProfile, ‖H-J‖ ≤ δ →
        boundaryProfileMap H ∈ regularBoundaryProfiles ∧
        ‖profileGeometry (boundaryProfileMap H)-profileGeometry (boundaryProfileMap J)‖ < ε := by
…

    Mentions: OAI.ClosedSurfaceR4.GeometryPreservation.EuclideanBoundaryProfile, OAI.ClosedSurfaceR4.GeometryPreservation.boundaryProfileMap, OAI.ClosedSurfaceR4.GeometryPreservation.regularBoundaryProfiles, OAI.ClosedSurfaceR4.GeometryPreservation.profileGeometry