LeadingProfileIdentification.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional leading-profile map evaluates to the exact geometric velocity and its derivatives in the primitive construction.

lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.jet_parameter_pullback_derivative line 15
lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.geometry_longitudinal_value line 41

theorem OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.leadingProfileMap_geometry line 52

Source documentation

All five entries depend on the third jet only through the single transverse derivative of the second jet.

theorem leadingProfileMap_geometry {S : TopologicalSpace.Opens JetPolynomial.Base}
    {G : JetPolynomial.Base → JetPolynomial.Space} (hG : ContDiff ℝ ∞ G)
    (hGO : MapsTo (lowJet G) S O) {p : JetPolynomial.Base} (hp : p ∈ S) (t : ℝ) :
    l.leadingProfileMap ((lowJet G p,t),lowDerivative G 1 p) =
      ![(l.geometry G hG hGO).longitudinal.val p (t : Period),
        (l.geometry G hG hGO).Y p,(l.geometry G hG hGO).C p,
        ((l.geometry G hG hGO).longitudinal.slow (coordinateVector 1)).val p (t : Period),
        (l.geometry G hG hGO).V.angle.val p (t : Period)] := by
…

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