The packet coefficients are constructed from the actual parent particle-map displacement and its two time derivatives. The inverse is the polynomial cofactor, and the strain and Jacobi curvature are their literal products; no separate inverse or coefficient evolution is assumed.

structure EulerParentPacketFrames.Parent : Type

Parent data, collecting T, T_pos, ell, ell_pos, ell_le_one, displacement and their compatibility conditions.

• T : ℝ

  Time horizon of Parent, of type ℝ.

• T_pos : 0 < self.T
• ell : ℝ

  Ell of Parent, of type ℝ.

• ell_pos : 0 < self.ell
• ell_le_one : self.ell ≤ 1
• displacement : SmoothTimeField (↑(Set.Icc 0 self.T)) EulerSmoothLimit.Space EulerSmoothLimit.Space

  Displacement of Parent, of type SmoothTimeField (Icc (0 : ℝ) T) Space Space.

• velocity : SmoothTimeField (↑(Set.Icc 0 self.T)) EulerSmoothLimit.Space EulerSmoothLimit.Space

  Velocity field of Parent, of type SmoothTimeField (Icc (0 : ℝ) T) Space Space.

• acceleration : SmoothTimeField (↑(Set.Icc 0 self.T)) EulerSmoothLimit.Space EulerSmoothLimit.Space

  Acceleration of Parent, of type SmoothTimeField (Icc (0 : ℝ) T) Space Space.

• displacement_time : SmoothTimeField.TimeDerivative self.T ⋯ self.displacement self.velocity
• velocity_time : SmoothTimeField.TimeDerivative self.T ⋯ self.velocity self.acceleration
• initial (x : EulerSmoothLimit.Space) : (self.displacement.field ⟨0, ⋯⟩) x = 0
• determinant (t : ↑(Set.Icc 0 self.T)) (x : EulerSmoothLimit.Space) : Matrix.det (EulerPacketPiola.operatorMatrix (ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ (⇑(self.displacement.field t)) (self.ell • x))) = 1

def EulerParentPacketFrames.Parent.zeroTime (G : Parent) : ↑(Set.Icc 0 G.T)

Zero time, given by ⟨0,le_rfl,G.T_pos.le⟩.

Equations

• G.zeroTime = ⟨0, ⋯⟩

noncomputable def EulerParentPacketFrames.Parent.frame (G : Parent) : SmoothTimeField (↑(Set.Icc 0 G.T)) EulerSmoothLimit.Space EulerPacketCofactor.EndSpace

Frame as an element of SmoothTimeField (Icc (0 : ℝ) G.T) Space EndSpace.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerParentPacketFrames.Parent.first (G : Parent) : SmoothTimeField (↑(Set.Icc 0 G.T)) EulerSmoothLimit.Space EulerPacketCofactor.EndSpace

First, given by G.velocity.derivative.precompLinear (G.ell • ContinuousLinearMap.id ℝ Space).

Equations

• G.first = G.velocity.derivative.precompLinear (G.ell • ContinuousLinearMap.id ℝ EulerSmoothLimit.Space)

noncomputable def EulerParentPacketFrames.Parent.second (G : Parent) : SmoothTimeField (↑(Set.Icc 0 G.T)) EulerSmoothLimit.Space EulerPacketCofactor.EndSpace

Second, given by G.acceleration.derivative.precompLinear (G.ell • ContinuousLinearMap.id ℝ Space).

Equations

• G.second = G.acceleration.derivative.precompLinear (G.ell • ContinuousLinearMap.id ℝ EulerSmoothLimit.Space)

noncomputable def EulerParentPacketFrames.Parent.inverse (G : Parent) : SmoothTimeField (↑(Set.Icc 0 G.T)) EulerSmoothLimit.Space EulerPacketCofactor.EndSpace

Inverse, given by SmoothTimeField.bilinear cofactorBilinear G.frame G.frame.

Equations

• G.inverse = SmoothTimeField.bilinear EulerPacketCofactor.cofactorBilinear G.frame G.frame

noncomputable def EulerParentPacketFrames.Parent.strain (G : Parent) : SmoothTimeField (↑(Set.Icc 0 G.T)) EulerSmoothLimit.Space EulerPacketCofactor.EndSpace

Strain, given by SmoothTimeField.bilinear (compL ℝ Space Space Space) G.first G.inverse.

Equations

• G.strain = SmoothTimeField.bilinear (ContinuousLinearMap.compL ℝ EulerSmoothLimit.Space EulerSmoothLimit.Space EulerSmoothLimit.Space) G.first G.inverse

noncomputable def EulerParentPacketFrames.Parent.curvature (G : Parent) : SmoothTimeField (↑(Set.Icc 0 G.T)) EulerSmoothLimit.Space EulerPacketCofactor.EndSpace

Curvature, given by (SmoothTimeField.bilinear (compL ℝ Space Space Space) G.second G.inverse).map (-ContinuousLinearMap.id ℝ EndSpace).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EulerParentPacketFrames.Parent.frame_apply (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.frame.field t) x = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ (⇑(G.displacement.field t)) (G.ell • x)

@[simp]

theorem EulerParentPacketFrames.Parent.first_apply (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.first.field t) x = fderiv ℝ (⇑(G.velocity.field t)) (G.ell • x)

@[simp]

theorem EulerParentPacketFrames.Parent.second_apply (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.second.field t) x = fderiv ℝ (⇑(G.acceleration.field t)) (G.ell • x)

@[simp]

theorem EulerParentPacketFrames.Parent.inverse_apply (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.inverse.field t) x = EulerPacketCofactor.adjugate ((G.frame.field t) x)

@[simp]

theorem EulerParentPacketFrames.Parent.strain_apply (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.strain.field t) x = (G.first.field t) x ∘SL (G.inverse.field t) x

@[simp]

theorem EulerParentPacketFrames.Parent.curvature_apply (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.curvature.field t) x = -(G.second.field t) x ∘SL (G.inverse.field t) x

theorem EulerParentPacketFrames.Parent.frame_det (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : Matrix.det (EulerPacketPiola.operatorMatrix ((G.frame.field t) x)) = 1

theorem EulerParentPacketFrames.Parent.inverse_left (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x v : EulerSmoothLimit.Space) : ((G.inverse.field t) x) (((G.frame.field t) x) v) = v

theorem EulerParentPacketFrames.Parent.inverse_right (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x v : EulerSmoothLimit.Space) : ((G.frame.field t) x) (((G.inverse.field t) x) v) = v

theorem EulerParentPacketFrames.Parent.frame_time (G : Parent) : SmoothTimeField.TimeDerivative G.T ⋯ G.frame G.first

theorem EulerParentPacketFrames.Parent.first_time (G : Parent) : SmoothTimeField.TimeDerivative G.T ⋯ G.first G.second

theorem EulerParentPacketFrames.Parent.frame_initial (G : Parent) (x : EulerSmoothLimit.Space) : (G.frame.field G.zeroTime) x = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space

theorem EulerParentPacketFrames.Parent.inverse_initial (G : Parent) (x v : EulerSmoothLimit.Space) : ((G.inverse.field G.zeroTime) x) v = v

theorem EulerParentPacketFrames.Parent.strain_equation (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x v : EulerSmoothLimit.Space) : ((G.first.field t) x) v = ((G.strain.field t) x) (((G.frame.field t) x) v)

theorem EulerParentPacketFrames.Parent.second_equation (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x v : EulerSmoothLimit.Space) : ((G.second.field t) x) v = -((G.curvature.field t) x) (((G.frame.field t) x) v)

noncomputable def EulerParentPacketFrames.Parent.initialStrain (G : Parent) : EulerMeanCoefficients.BoundedSmoothField EulerPacketCofactor.EndSpace

Initial strain, bundling field, smooth, bounded.

Equations

• G.initialStrain = { field := G.first.field G.zeroTime, smooth := ⋯, bounded := ⋯ }

@[simp]

theorem EulerParentPacketFrames.Parent.initialStrain_apply (G : Parent) (x : EulerSmoothLimit.Space) : G.initialStrain.field x = (G.first.field G.zeroTime) x