JetLoopPullback.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Transfer the constructed geometric loop to the ordered coordinate jets used by the quantitative finite correction.

def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.jetDomain line 15

def OAI.ClosedSurfaceR4.SurfaceVelocityFamily.Loop.ofGeometric line 21

Source documentation

The velocity supplied by the geometric construction, expressed in the analytic second-jet coordinates. All its identities survive this pullback.

def Loop.ofGeometric {Ω : TopologicalSpace.Opens CollarVelocity.JetBase}
    {a : CollarVelocity.JetBase → ℝ} {V : CollarVelocity.JetBase × ℝ → RVec 4}
    (ha : ContDiffOn ℝ ∞ a Ω) (hV : ContDiffOn ℝ ∞ V (Ω ×ˢ univ))
    (hper : ∀ j ∈ Ω, Function.Periodic (fun t => V (j, t)) 1)
    (hD : ∀ j ∈ Ω, NormalFrame.gramDet (j.2 1) (j.2 4) ≠ 0)
    (hn : ∀ j ∈ Ω, realNormalPart (j.2 1) (j.2 4) (j.2 0) ≠ 0 ∨ a j ≠ 0)
    (hy : ∀ j ∈ Ω, ∀ t, j.2 1 ⬝ᵥ V (j, t) = 0)
    (hc : ∀ j ∈ Ω, ∀ t, j.2 4 ⬝ᵥ V (j, t) = 0)
    (hlen : ∀ j ∈ Ω, ∀ t, V (j, t) ⬝ᵥ V (j, t) =
      realNormalPart (j.2 1) (j.2 4) (j.2 0) ⬝ᵥ
        realNormalPart (j.2 1) (j.2 4) (j.2 0) + a j ^ 2)
    (hm : ∀ j ∈ Ω, (∫ t in 0..1, V (j, t)) = realNormalPart (j.2 1) (j.2 4) (j.2 0)) :
…

Mentions: OAI.ClosedSurfaceR4.CollarVelocity.JetBase, OAI.ClosedSurfaceR4.NormalFrame.gramDet

lemma OAI.ClosedSurfaceR4.SurfaceVelocityFamily.actual_jet_mem line 48