OAI/Geometry/SurfaceImmersion/Primitive/BoundaryProfileGeometry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Normal frames and scaled second-form coefficients are smooth functions of exactly the five derivative components retained by the primitive construction.

  1. abbrev OAI.ClosedSurfaceR4.GeometryPreservation.BoundaryProfile line 14
  2. def OAI.ClosedSurfaceR4.GeometryPreservation.profileNormalPart line 16
  3. def OAI.ClosedSurfaceR4.GeometryPreservation.profilePreferred line 19
  4. def OAI.ClosedSurfaceR4.GeometryPreservation.profileComplement line 22
  5. def OAI.ClosedSurfaceR4.GeometryPreservation.regularBoundaryProfiles line 25
  6. def OAI.ClosedSurfaceR4.GeometryPreservation.profileCoefficients line 30

    Source documentation

    The coordinates are S, D, N, and z L. The xx entry in the input has already been multiplied by the fast scale.

    def profileCoefficients (J : BoundaryProfile) : Fin 4 → ℝ :=
…

    Mentions: OAI.ClosedSurfaceR4.GeometryPreservation.BoundaryProfile

  7. def OAI.ClosedSurfaceR4.GeometryPreservation.profileGeometry line 35
  8. lemma OAI.ClosedSurfaceR4.GeometryPreservation.contDiffAt_profileNormalPart line 38
  9. lemma OAI.ClosedSurfaceR4.GeometryPreservation.contDiffAt_profilePreferred line 45
  10. lemma OAI.ClosedSurfaceR4.GeometryPreservation.contDiffAt_profileComplement line 49
  11. lemma OAI.ClosedSurfaceR4.GeometryPreservation.isOpen_regularBoundaryProfiles line 58
  12. lemma OAI.ClosedSurfaceR4.GeometryPreservation.contDiffAt_profileCoefficients line 67
  13. lemma OAI.ClosedSurfaceR4.GeometryPreservation.contDiffAt_profileGeometry line 84
  14. theorem OAI.ClosedSurfaceR4.GeometryPreservation.compact_boundary_profile_stability line 91

    Source documentation

    Uniformly transfer all five derivative estimates to the actual normal frame and its scaled coefficients on a compact family of regular profiles.

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

    Mentions: OAI.ClosedSurfaceR4.GeometryPreservation.BoundaryProfile, OAI.ClosedSurfaceR4.GeometryPreservation.regularBoundaryProfiles, OAI.ClosedSurfaceR4.GeometryPreservation.profileGeometry