The first packet's complete source budgets come from actual parent label fields and its short-time low strain bound. The growth profile is the constant one, proved by the actual tangent equation.

structure EulerParentPacketFrames.ForwardInputs {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (M : EulerMeanPacketProvider.Data) (D : EulerTransversePacketProvider.Data U) : Type

Forward inputs data, collecting linear, normal, mean.

• linear : EulerTransversePacketForward.Budget D (Fin 4) 6

  Linear of ForwardInputs, of type EulerTransversePacketForward.Budget D (Fin 4) 6.

• normal : EulerTransversePacketJoin.NormalBudget D 6 self.linear.R

  Normal of ForwardInputs, of type EulerTransversePacketJoin.NormalBudget D 6 linear.R.

• mean : EulerMeanPacketProvider.Budget M 6 self.linear.R

  Mean field of ForwardInputs, of type EulerMeanPacketProvider.Budget M 6 linear.R.

noncomputable def EulerParentPacketFrames.LabelData.forwardRaw {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {G : Parent} (L : LabelData G) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (CM : ℝ) (hCM : 0 ≤ CM) (hM : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖(G.strain.field t) x‖ ≤ CM) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hshort : CM * G.T ≤ 1 / 2) : EulerTransversePacketForward.Budget (G.transverseData m hm R S hS) (Fin 4) 6

Forward raw, constructed using shortPhysicalForwardBudget.

Equations

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

noncomputable def EulerParentPacketFrames.LabelData.forwardInputs {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {G : Parent} (L : LabelData G) (H : LowBounds G) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (CM : ℝ) (hCM : 0 ≤ CM) (hM : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖(G.strain.field t) x‖ ≤ CM) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hshort : CM * G.T ≤ 1 / 2) (Ti : ℝ) (hT1 : G.T ≤ 1) (hTi : G.T⁻¹ ≤ Ti) : ForwardInputs (G.meanData H) (G.transverseData m hm R S hS)

Forward inputs as an element of ForwardInputs (G.meanData H) (G.transverseData m hm R S hS).

Equations

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

theorem EulerParentPacketFrames.LabelData.forwardInputs_growth {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {G : Parent} (L : LabelData G) (H : LowBounds G) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (CM : ℝ) (hCM : 0 ≤ CM) (hM : ∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖(G.strain.field t) x‖ ≤ CM) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hshort : CM * G.T ≤ 1 / 2) (Ti : ℝ) (hT1 : G.T ≤ 1) (hTi : G.T⁻¹ ≤ Ti) : (L.forwardInputs H m hm R S hS CM hCM hM Ω hΩ hΩo hsub hΩball hshort Ti hT1 hTi).linear.g = 1