Low packet grades retain fixed polynomial costs; higher grades use one common tail base.

def EulerPacketCylinderField.fixedVelocityGradeCost (R H : ℝ) (n : ℕ) : ℝ

Fixed velocity grade cost, given by (3*H^(2*n))*((4*R)^(highShift n)*((highShift n).factorial : ℝ)^2).

Equations

• EulerPacketCylinderField.fixedVelocityGradeCost R H n = 3 * H ^ (2 * n) * ((4 * R) ^ EulerPacketShiftArithmetic.highShift n * ↑(EulerPacketShiftArithmetic.highShift n).factorial ^ 2)

theorem EulerPacketCylinderField.fixedVelocityGradeCost_nonneg (R H : ℝ) (hR : 0 ≤ R) (n : ℕ) : 0 ≤ fixedVelocityGradeCost R H n

theorem EulerPacketCylinderField.Field.WordBound.split_fixed_shift {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (hR : 0 ≤ R) (hA : 0 ≤ A) : G.WordBound q (4 * R) (A * ((4 * R) ^ d * ↑d.factorial ^ 2)) 0

theorem EulerPacketCylinderField.Field.WordBound.fixed_velocity_grade {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q n : ℕ} {R H : ℝ} (hG : G.WordBound q R (3 * H ^ (2 * n)) (EulerPacketShiftArithmetic.highShift n)) (hR : 0 ≤ R) (hH : 0 ≤ H) : G.WordBound q (4 * R) (fixedVelocityGradeCost R H n) 0

theorem EulerPacketCylinderField.Field.WordBound.coarse_velocity_grade {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q n : ℕ} {R H : ℝ} (hG : G.WordBound q R (3 * H ^ (2 * n)) (EulerPacketShiftArithmetic.highShift n)) (hR : 1 ≤ R) (hH : 1 ≤ H) (C : ℝ) (hC : 1 ≤ C) (N : ℕ) (hN : 1 ≤ N) (hn : n ≤ 2 * N + 2) : G.WordBound q (4 * R) (EulerPacketCoarseMajorant.tailBase R H C N ^ (n + 1)) 0