OAI/Geometry/SurfaceImmersion/Primitive/SurfaceVelocityFamily.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Convert a geometric second-jet velocity loop into the exact family of Euclidean data used by the supported finite periodic recursion.

  1. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.normal line 18
  2. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.tangent line 19
  3. structure OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop line 23

    Source documentation

    The actual geometric hypotheses on the second-jet neighborhood. The first and second derivatives are fixed coordinate projections of that jet.

    structure Loop (O : TopologicalSpace.Opens LowJet) where
…
  4. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.smoothNormal line 41
  5. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.smoothTangent line 47
  6. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.q line 49
  7. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.smoothQ line 51
  8. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.q_pos line 54
  9. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.euclideanVelocity line 57
  10. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.euclideanVelocity_apply line 62
  11. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.euclideanVelocity_smooth line 66
  12. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.euclideanVelocity_mean line 70
  13. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.euclideanVelocity_length line 79
  14. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.plane line 86
  15. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.mem_plane line 90
  16. lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.tangent_perp line 94
  17. def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.geometry line 103

    Source documentation

    Pulling back through the actual second jet supplies the differentiated constraint Y_y=C, rather than adding that constraint as a new input.

    def geometry {S : TopologicalSpace.Opens JetPolynomial.Base}
    (G : JetPolynomial.Base → JetPolynomial.Space) (hG : ContDiff ℝ ∞ G)
    (hGO : MapsTo (lowJet G) S O) : Geometry (E := Euclidean) S (coordinateVector 1) where
…

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.Space