OAI/Geometry/SurfaceImmersion/Primitive/CrossingComponents.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Exact scalar identities used in the later-curve crossing calculation.

  1. def OAI.ClosedSurfaceR4.GeometryPreservation.frameXX line 11

    Source documentation

    The normal components forced by the Gauss identity when the transverse second-form component is (S,0).

    def frameXX (S D N L k : ℝ) : ℝ × ℝ := ((k+D^2+N^2)/S,L)
  2. def OAI.ClosedSurfaceR4.GeometryPreservation.frameXY line 12
  3. def OAI.ClosedSurfaceR4.GeometryPreservation.frameYY line 13
  4. def OAI.ClosedSurfaceR4.GeometryPreservation.pureComponents line 15
  5. def OAI.ClosedSurfaceR4.GeometryPreservation.slopePure line 18
  6. def OAI.ClosedSurfaceR4.GeometryPreservation.slopeMixed line 21
  7. lemma OAI.ClosedSurfaceR4.GeometryPreservation.frame_gauss line 24
  8. lemma OAI.ClosedSurfaceR4.GeometryPreservation.pure_first_identity line 29
  9. lemma OAI.ClosedSurfaceR4.GeometryPreservation.pure_second_identity line 34
  10. lemma OAI.ClosedSurfaceR4.GeometryPreservation.pure_unit_slope line 40
  11. lemma OAI.ClosedSurfaceR4.GeometryPreservation.mixed_sub_left line 44
  12. lemma OAI.ClosedSurfaceR4.GeometryPreservation.mixed_sub_right line 49