The finite approximate velocity and its genuine time derivative share the profile bounds.
theorem
EulerPacketCylinderField.ProfileRegularity.velocityGrade_bound
{P T : ℝ}
[Fact (0 < P)]
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(hT : 0 < T)
(G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i))
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(n : ℕ)
:
(velocityGradeField hT G n).WordBound 6 R (3 * S.H0 ^ (2 * n)) (EulerPacketShiftArithmetic.highShift n)
theorem
EulerPacketCylinderField.ProfileRegularity.velocityGradeDerivative_bound
{P T : ℝ}
[Fact (0 < P)]
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(hT : 0 < T)
(G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i))
{S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)}
{R : ℝ}
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(n : ℕ)
:
(velocityGradeDerivativeField hT G n).WordBound 6 R (3 * S.H0 ^ (2 * n)) (EulerPacketShiftArithmetic.highShift n)