Actual source data on the history and forward time intervals

These constructions restrict the given deformation and its inverse. The time derivative follows by restriction or by the affine change t = τ+s; spatial derivatives are retained literally by continuous precomposition.

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.instTransversePacketIntervalData1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.instTransversePacketIntervalData1 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.instTransversePacketIntervalData2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.instTransversePacketIntervalData2 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.instTransversePacketIntervalData3 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.instTransversePacketIntervalData3 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.instTransversePacketIntervalData4 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.instTransversePacketIntervalData4 = inferInstance

noncomputable def EulerTransversePacketProvider.Data.initial {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (τ : ℝ) (hτ : 0 < τ) (hτT : τ ≤ D.T) : Data U

The prescribed source fields on [0,τ].

Equations

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

noncomputable def EulerTransversePacketProvider.Data.tail {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (τ : ℝ) (hτ : 0 ≤ τ) (hτT : τ < D.T) : Data U

The prescribed source fields on [τ,T], with elapsed time starting at zero.

Equations

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

@[simp]

theorem EulerTransversePacketProvider.Data.initial_frame_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (τ : ℝ) (hτ : 0 < τ) (hτT : τ ≤ D.T) (t : ↑(Set.Icc 0 τ)) (x : EulerSmoothLimit.Space) (v : U) : (((D.initial τ hτ hτT).frame.field t) x) v = ((D.frame.field ((EulerTimeIntervalRestriction.initialInclusion D.T τ hτT) t)) x) v

@[simp]

theorem EulerTransversePacketProvider.Data.tail_frame_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (τ : ℝ) (hτ : 0 ≤ τ) (hτT : τ < D.T) (t : ↑(Set.Icc 0 (D.T - τ))) (x : EulerSmoothLimit.Space) (v : U) : (((D.tail τ hτ hτT).frame.field t) x) v = ((D.frame.field ((EulerTimeIntervalRestriction.tailInclusion D.T τ hτ) t)) x) v

theorem EulerTransversePacketProvider.Data.initial_inverseBound_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (τ : ℝ) (hτ : 0 < τ) (hτT : τ ≤ D.T) : (D.initial τ hτ hτT).inverseBound ≤ D.inverseBound

theorem EulerTransversePacketProvider.Data.tail_inverseBound_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (τ : ℝ) (hτ : 0 ≤ τ) (hτT : τ < D.T) : (D.tail τ hτ hτT).inverseBound ≤ D.inverseBound

noncomputable def EulerTransversePacketProvider.HistoryData.initial {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} (B : HistoryData D) (τ : ℝ) (hτ : 0 < τ) (hτT : τ ≤ D.T) : HistoryData (D.initial τ hτ hτT)

The source Jacobi law and positivity remain valid on the actual history interval.

Equations

• B.initial τ hτ hτT = { H := B.H.comp (EulerTimeIntervalRestriction.initialInclusion D.T τ hτT), jacobi := ⋯, potential := B.potential, potential_nonneg := ⋯, potential_bound := ⋯, small := ⋯ }