The actual zero-history packet has a bounded normalized velocity and a small normal drift, at a single radius inherited from the profile construction.
theorem
EulerPacketCylinderField.forwardPacket_normalized_bound
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(Y : EulerTransversePacketProvider.InitialData P D)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB 1)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC : CoefficientBudget (sourceCoefficientData P M D (EulerTransversePacketProvider.InitialData.zero P D) hTime))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(α : ℝ)
(hα : 0 < α)
(hgrowth : timeProfileChange S.growth hTime = α • L.g)
(hprimaryBudget : ProfileBudget (forwardSourcePrimaryWitness P M D hTime Y) S L.R 1)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
:
((sourcePacketPullbackField P M D hTime (EulerTransversePacketProvider.InitialData.zero P D) Y N k⁻¹).smul k).WordBound
6 (4 * L.R) (BC.multiplierCost * (fixedVelocityGradeCost L.R S.H0 1 + fixedVelocityGradeCost L.R S.H0 2 + 1)) 0
theorem
EulerPacketCylinderField.forwardPacket_normal_bound
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(Y : EulerTransversePacketProvider.InitialData P D)
(L : EulerTransversePacketForward.Budget D (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB 1)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC : CoefficientBudget (sourceCoefficientData P M D (EulerTransversePacketProvider.InitialData.zero P D) hTime))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(α : ℝ)
(hα : 0 < α)
(hgrowth : timeProfileChange S.growth hTime = α • L.g)
(hprimaryBudget : ProfileBudget (forwardSourcePrimaryWitness P M D hTime Y) S L.R 1)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
:
(((sourcePacketPullbackField P M D hTime (EulerTransversePacketProvider.InitialData.zero P D) Y N k⁻¹).smul k).map
(normalComponentMap D.m₀)).WordBound
6 (4 * L.R) (BC.multiplierCost * (fixedVelocityGradeCost L.R S.H0 2 + 2) / k) 0