BoundaryProfileFrame.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Identification of the five-profile coefficient map with the genuine second fundamental form of a smooth immersion.

def OAI.ClosedSurfaceR4.GeometryPreservation.realBoundaryProfile line 12
lemma OAI.ClosedSurfaceR4.GeometryPreservation.realNormalPart_dot_of_normal line 16
lemma OAI.ClosedSurfaceR4.GeometryPreservation.realBoundaryProfile_regular line 22
theorem OAI.ClosedSurfaceR4.GeometryPreservation.exists_profile_secondFormFrame line 30
Source documentation
The scaled longitudinal coefficient is read from z Fxx, so this identification is uniform even when Fxx itself diverges.
```
theorem exists_profile_secondFormFrame {F : RField 4} (hF : ContDiff ℝ ∞ F)
    (z : ℝ) (p : Base) (hJ : realBoundaryProfile F z p ∈ regularBoundaryProfiles) :
    ∃ d : SecondFormFrame F p
      (coordinateGauss (realMetric F dx dx) (realMetric F dx dy) (realMetric F dy dy) p),
      d.n = profilePreferred (realBoundaryProfile F z p) ∧
      d.m = profileComplement (realBoundaryProfile F z p) ∧
      profileCoefficients (realBoundaryProfile F z p) = ![d.S,d.D,d.N,z*d.L] := by
…
```
Mentions: OAI.ClosedSurfaceR4.GeometryPreservation.realBoundaryProfile, OAI.ClosedSurfaceR4.GeometryPreservation.regularBoundaryProfiles, OAI.ClosedSurfaceR4.GeometryPreservation.SecondFormFrame, OAI.ClosedSurfaceR4.GeometryPreservation.profilePreferred, OAI.ClosedSurfaceR4.GeometryPreservation.profileComplement, OAI.ClosedSurfaceR4.GeometryPreservation.profileCoefficients