Restricting the actual parent to a nested horizon preserves its flow identities, physical-label budget and the source low-order guards.

noncomputable def EulerParentPacketFrames.Parent.restrictTime (G : Parent) (S : ℝ) (hS : 0 < S) (hST : S ≤ G.T) : Parent

Restrict time, bundling T, T_pos, ell, ell_pos and the required compatibility proofs.

Equations

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

theorem EulerParentPacketFrames.Parent.restrictTime_frame (G : Parent) (S : ℝ) (hS : 0 < S) (hST : S ≤ G.T) (t : ↑(Set.Icc 0 S)) (x : EulerSmoothLimit.Space) : ((G.restrictTime S hS hST).frame.field t) x = (G.frame.field ((EulerTimeIntervalRestriction.initialInclusion G.T S hST) t)) x

theorem EulerParentPacketFrames.Parent.restrictTime_first (G : Parent) (S : ℝ) (hS : 0 < S) (hST : S ≤ G.T) (t : ↑(Set.Icc 0 S)) (x : EulerSmoothLimit.Space) : ((G.restrictTime S hS hST).first.field t) x = (G.first.field ((EulerTimeIntervalRestriction.initialInclusion G.T S hST) t)) x

theorem EulerParentPacketFrames.Parent.restrictTime_second (G : Parent) (S : ℝ) (hS : 0 < S) (hST : S ≤ G.T) (t : ↑(Set.Icc 0 S)) (x : EulerSmoothLimit.Space) : ((G.restrictTime S hS hST).second.field t) x = (G.second.field ((EulerTimeIntervalRestriction.initialInclusion G.T S hST) t)) x

theorem EulerParentPacketFrames.Parent.restrictTime_inverse (G : Parent) (S : ℝ) (hS : 0 < S) (hST : S ≤ G.T) (t : ↑(Set.Icc 0 S)) (x : EulerSmoothLimit.Space) : ((G.restrictTime S hS hST).inverse.field t) x = (G.inverse.field ((EulerTimeIntervalRestriction.initialInclusion G.T S hST) t)) x

theorem EulerParentPacketFrames.Parent.restrictTime_strain (G : Parent) (S : ℝ) (hS : 0 < S) (hST : S ≤ G.T) (t : ↑(Set.Icc 0 S)) (x : EulerSmoothLimit.Space) : ((G.restrictTime S hS hST).strain.field t) x = (G.strain.field ((EulerTimeIntervalRestriction.initialInclusion G.T S hST) t)) x

theorem EulerParentPacketFrames.Parent.restrictTime_curvature (G : Parent) (S : ℝ) (hS : 0 < S) (hST : S ≤ G.T) (t : ↑(Set.Icc 0 S)) (x : EulerSmoothLimit.Space) : ((G.restrictTime S hS hST).curvature.field t) x = (G.curvature.field ((EulerTimeIntervalRestriction.initialInclusion G.T S hST) t)) x

theorem EulerParentPacketFrames.Parent.restrictTime_initialStrain (G : Parent) (S : ℝ) (hS : 0 < S) (hST : S ≤ G.T) (x : EulerSmoothLimit.Space) : (G.restrictTime S hS hST).initialStrain.field x = G.initialStrain.field x

def EulerParentPacketFrames.LabelData.restrictTime {G : Parent} (L : LabelData G) (S : ℝ) (hS : 0 < S) (hST : S ≤ G.T) : LabelData (G.restrictTime S hS hST)

Restrict time, bundling K, K_one, displacement, velocity and the required compatibility proofs.

Equations

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

def EulerParentPacketFrames.LowBounds.restrictTime {G : Parent} (H : LowBounds G) (S : ℝ) (hS : 0 < S) (hST : S ≤ G.T) : LowBounds (G.restrictTime S hS hST)

Restrict time, bundling Be, Bc, L, r and the required compatibility proofs.

Equations

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