OAI/Geometry/SurfaceImmersion/Atlas/LowJetCoordinateChange.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Exact order-two jet transport under a fixed smooth coordinate map. The new position is supplied separately, so no inverse coordinate map is required and the construction applies to arbitrary smooth maps.

  1. def OAI.ClosedSurfaceR4.JetPolynomial.coordinatePartial line 15

    Source documentation

    One fixed coordinate derivative of a scalar function.

    def coordinatePartial (f : Base → ℝ) (v : Fin 2) : Base → ℝ :=
…

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base

  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.coordinatePartial_smooth line 18
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.coordinateVector_expansion line 22
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.coordinatePartial_component line 27
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.coordinatePartial_comp line 34
  6. lemma OAI.ClosedSurfaceR4.JetPolynomial.coordinatePartial_coordinatePartial_comp line 49
  7. def OAI.ClosedSurfaceR4.JetPolynomial.firstJetSlot line 80

    Source documentation

    Slots of the two first and four ordered second coordinate derivatives.

    def firstJetSlot : Fin 2 → Fin 7 := ![1,2]
  8. def OAI.ClosedSurfaceR4.JetPolynomial.secondJetSlot line 81
  9. lemma OAI.ClosedSurfaceR4.JetPolynomial.lowJet_first_slot line 83
  10. lemma OAI.ClosedSurfaceR4.JetPolynomial.lowJet_second_slot line 87
  11. def OAI.ClosedSurfaceR4.JetPolynomial.coordinateChangeFirst line 93

    Source documentation

    First derivative of the composed map, linear in the supplied jet.

    def coordinateChangeFirst (T : Base → Base) (x : Base) (J : LowJet)
    (v : Fin 2) (a : Fin 4) : ℝ :=
…

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

  12. def OAI.ClosedSurfaceR4.JetPolynomial.coordinateChangeSecond line 98

    Source documentation

    Ordered second derivative, with both the Hessian and acceleration terms.

    def coordinateChangeSecond (T : Base → Base) (x : Base) (J : LowJet)
    (v w : Fin 2) (a : Fin 4) : ℝ :=
…

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

  13. def OAI.ClosedSurfaceR4.JetPolynomial.lowJetCoordinateChange line 108

    Source documentation

    Transport a positional low jet at T x to the positional low jet at x. The old positional components are unnecessary; the value and ordered jets are evaluated by the chain rule.

    def lowJetCoordinateChange (T : Base → Base) (p : Base × LowJet) : LowJet
  | .inl i => p.1 i
  | .inr (w,a) => ![p.2 (.inr (0,a)),
      coordinateChangeFirst T p.1 p.2 0 a,
      coordinateChangeFirst T p.1 p.2 1 a,
      coordinateChangeSecond T p.1 p.2 0 0 a,
      coordinateChangeSecond T p.1 p.2 0 1 a,
      coordinateChangeSecond T p.1 p.2 1 0 a,
      coordinateChangeSecond T p.1 p.2 1 1 a] w

    Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.coordinateChangeFirst, OAI.ClosedSurfaceR4.JetPolynomial.coordinateChangeSecond

  14. lemma OAI.ClosedSurfaceR4.JetPolynomial.coordinateChangeFirst_smooth line 118
  15. lemma OAI.ClosedSurfaceR4.JetPolynomial.coordinateChangeSecond_smooth line 126
  16. lemma OAI.ClosedSurfaceR4.JetPolynomial.lowJetCoordinateChange_smooth line 143
  17. theorem OAI.ClosedSurfaceR4.JetPolynomial.lowJetCoordinateChange_eval line 165

    Source documentation

    The finite-dimensional transport agrees exactly with the low jet of the composed smooth map.

    theorem lowJetCoordinateChange_eval {G : Base → Space} {T : Base → Base}
    (hG : ContDiff ℝ ∞ G) (hT : ContDiff ℝ ∞ T) (x : Base) :
    lowJetCoordinateChange T (x,lowJet G (T x)) = lowJet (G ∘ T) x := by
…

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

  18. lemma OAI.ClosedSurfaceR4.JetPolynomial.iteratedDirectional_eventuallyEq line 191
  19. lemma OAI.ClosedSurfaceR4.JetPolynomial.lowJet_eventuallyEq line 202

    Source documentation

    Positional jets only depend on the germ of the map.

    lemma lowJet_eventuallyEq {G H : Base → Space} {x : Base}
    (h : G =ᶠ[𝓝 x] H) : lowJet G x = lowJet H x := by
…

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

  20. lemma OAI.ClosedSurfaceR4.JetPolynomial.lowJetCoordinateChange_inverse_eval line 214

    Source documentation

    Evaluate the inverse-coordinate transport at T x. The only map identification required here is the actual local germ H ∘ S = G.

    lemma lowJetCoordinateChange_inverse_eval {G H : Base → Space} {T S : Base → Base}
    (hH : ContDiff ℝ ∞ H) (hS : ContDiff ℝ ∞ S) (x : Base)
    (hST : S (T x) = x) (hrel : (H ∘ S) =ᶠ[𝓝 (T x)] G) :
    lowJetCoordinateChange S (T x,lowJet H x) = lowJet G (T x) := by
…

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

  21. lemma OAI.ClosedSurfaceR4.JetPolynomial.lowJetCoordinateChange_local_inverse line 224

    Source documentation

    A local inverse and the local relation H = G ∘ T supply the germ in lowJetCoordinateChange_inverse_eval.

    lemma lowJetCoordinateChange_local_inverse {G H : Base → Space} {T S : Base → Base}
    (hH : ContDiff ℝ ∞ H) (hS : ContDiff ℝ ∞ S) (x : Base)
    (hST : S (T x) = x) (hTS : (T ∘ S) =ᶠ[𝓝 (T x)] id)
    (hrel : H =ᶠ[𝓝 x] (G ∘ T)) :
    lowJetCoordinateChange S (T x,lowJet H x) = lowJet G (T x) := by
…

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