The actual terminal-data primary supplies the grade-one profile and all regularity/locality data required by the recursive packet construction.
noncomputable def
EulerTransversePacketPrimary.profileRegularity
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(Y : EulerTransversePacketProvider.InitialData P D)
(O : EulerPacketProfileRecursion.Operators)
(hcorrector : O.curlCorrector = D.curlCorrector P)
:
EulerPacketCylinderField.ProfileRegularity P D.T ⋯ D.support
(EulerPacketProfileRecursion.primaryProfile O (vector τ hτ hτT B Y) (scalar τ hτ hτT B Y))
This primary is constructed from the terminal history and its genuine forward continuation, including its actual pressure and slow curl.
Equations
- One or more equations did not get rendered due to their size.