The actual parent strain obeys the matrix Riccati equation. Its inverse derivative is derived from the polynomial cofactor construction and the genuine frame identity, including the time-interval endpoints.

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

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

Equations

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

@[simp]

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

theorem EulerParentPacketFrames.Parent.inverse_time (G : Parent) : SmoothTimeField.TimeDerivative G.T ⋯ G.inverse G.inverseDerivative

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

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

Equations

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

@[simp]

theorem EulerParentPacketFrames.Parent.strainDerivative_apply (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.strainDerivative.field t) x = -(G.strain.field t) x ∘SL (G.strain.field t) x - (G.curvature.field t) x

theorem EulerParentPacketFrames.Parent.strain_time (G : Parent) : SmoothTimeField.TimeDerivative G.T ⋯ G.strain G.strainDerivative

theorem EulerParentPacketFrames.Parent.strain_within (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath G.T ⋯ G.strain.field s) x) (-(G.strain.field t) x ∘SL (G.strain.field t) x - (G.curvature.field t) x) (Set.Icc 0 G.T) ↑t

The exact clamped-time form used by the source ray/velocity dynamics.

theorem EulerParentPacketFrames.Parent.strainDerivative_norm_le (G : Parent) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : ‖(G.strainDerivative.field t) x‖ ≤ ‖(G.strain.field t) x‖ ^ 2 + ‖(G.curvature.field t) x‖

theorem EulerParentPacketFrames.Parent.strainDerivative_norm_bound (G : Parent) (CM CH : ℝ) (hCM : 0 ≤ CM) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) (hM : ‖(G.strain.field t) x‖ ≤ CM) (hH : ‖(G.curvature.field t) x‖ ≤ CH) : ‖(G.strainDerivative.field t) x‖ ≤ CM ^ 2 + CH

noncomputable def EulerParentPacketFrames.Parent.centerStrain (G : Parent) (t : ℝ) : EulerPacketCofactor.EndSpace

Center strain, given by extendPath G.T G.T_pos.le G.strain.field t 0.

Equations

• G.centerStrain t = (EulerVolterraConvolution.extendPath G.T ⋯ G.strain.field t) 0

noncomputable def EulerParentPacketFrames.Parent.centerCurvature (G : Parent) (t : ℝ) : EulerPacketCofactor.EndSpace

Center curvature, given by extendPath G.T G.T_pos.le G.curvature.field t 0.

Equations

• G.centerCurvature t = (EulerVolterraConvolution.extendPath G.T ⋯ G.curvature.field t) 0

noncomputable def EulerParentPacketFrames.Parent.centerStrainDerivative (G : Parent) (t : ℝ) : EulerPacketCofactor.EndSpace

Center strain derivative, given by extendPath G.T G.T_pos.le G.strainDerivative.field t 0.

Equations

• G.centerStrainDerivative t = (EulerVolterraConvolution.extendPath G.T ⋯ G.strainDerivative.field t) 0

theorem EulerParentPacketFrames.Parent.centerStrainDerivative_eq (G : Parent) (t : ℝ) : G.centerStrainDerivative t = -G.centerStrain t ∘SL G.centerStrain t - G.centerCurvature t

theorem EulerParentPacketFrames.Parent.centerStrain_derivative (G : Parent) (τ : ℝ) (hτ : 0 ≤ τ) (t : ℝ) (ht : t ∈ Set.Icc τ G.T) : HasDerivWithinAt G.centerStrain (G.centerStrainDerivative t) (Set.Icc τ G.T) t

theorem EulerParentPacketFrames.Parent.centerStrainDerivative_bound (G : Parent) (τ CM CH K : ℝ) (hτ : 0 ≤ τ) (hCM : 0 ≤ CM) (hM : ∀ t ∈ Set.Icc τ G.T, ‖G.centerStrain t‖ ≤ CM) (hH : ∀ t ∈ Set.Icc τ G.T, ‖G.centerCurvature t‖ ≤ CH) (hK : CM ^ 2 + CH ≤ K ^ 2) (t : ℝ) (ht : t ∈ Set.Icc τ G.T) : ‖G.centerStrainDerivative t‖ ≤ K ^ 2

The fixed-center derivative bound needed by the next geometric stage follows from the actual strain/curvature bounds and one scalar guard.

theorem EulerParentPacketFrames.Parent.transverse_strain_within (G : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath G.T ⋯ (G.transverseData m hm R S hS).M.field s) x) (-((G.transverseData m hm R S hS).M.field t) x ∘SL ((G.transverseData m hm R S hS).M.field t) x - (G.curvature.field t) x) (Set.Icc 0 G.T) ↑t