The literal compact initial wave supplies the seven-field primary budget for the direct-forward, zero-history packet construction.
theorem
EulerTransversePacketForward.Budget.primary_profile_budget
{P : ℝ}
[Fact (0 < P)]
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(L : Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(C : ℝ)
(W : L.GradeGuards N C)
(Y : EulerTransversePacketProvider.InitialData P D)
(α : ℝ)
(hα : 0 < α)
(hYb :
∀ (n : ℕ),
EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑Y.value) n 0 ≤ α * C * EulerGevrey.majorant L.R 0 n)
(O : EulerPacketProfileRecursion.Operators)
(hcorrector : O.curlCorrector = D.curlCorrector P)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 D.T))
(hgrowth : S.growth = α • L.g)
:
EulerPacketCylinderField.ProfileBudget (EulerPacketForwardPrimary.regularity D Y O hcorrector) S L.R 1
theorem
EulerPacketTerminalDatum.forwardPrimary_profile_budget
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(N : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(δ : ℝ)
(hδ : 0 < δ)
(hδ1 : δ ≤ 1)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(W : L.GradeGuards N (wordCost (Fin 4) 6 δ * ‖ξ‖))
(O : EulerPacketProfileRecursion.Operators)
(hcorrector : O.curlCorrector = D.curlCorrector period)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 D.T))
(hgrowth : S.growth = α • L.g)
:
EulerPacketCylinderField.ProfileBudget (forwardPrimaryRegularity D δ hδ (α • ξ) hs O hcorrector) S L.R 1