Fixed source costs for the normalized packet and its smaller transport drift.

def EulerPacketCorrectionConstants.velocity (R H C : ℝ) : ℝ

Velocity, given by C*(fixedVelocityGradeCost R H 1+fixedVelocityGradeCost R H 2+1).

Equations

• EulerPacketCorrectionConstants.velocity R H C = C * (EulerPacketCylinderField.fixedVelocityGradeCost R H 1 + EulerPacketCylinderField.fixedVelocityGradeCost R H 2 + 1)

def EulerPacketCorrectionConstants.normal (R H C : ℝ) : ℝ

Normal, given by C*(fixedVelocityGradeCost R H 2+2).

Equations

• EulerPacketCorrectionConstants.normal R H C = C * (EulerPacketCylinderField.fixedVelocityGradeCost R H 2 + 2)

def EulerPacketCorrectionConstants.drift (R H C : ℝ) : ℝ

Drift, given by 2*(3*velocity R H C+normal R H C).

Equations

• EulerPacketCorrectionConstants.drift R H C = 2 * (3 * EulerPacketCorrectionConstants.velocity R H C + EulerPacketCorrectionConstants.normal R H C)

theorem EulerPacketCorrectionConstants.velocity_nonneg (R H C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) : 0 ≤ velocity R H C

theorem EulerPacketCorrectionConstants.normal_nonneg (R H C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) : 0 ≤ normal R H C

theorem EulerPacketCorrectionConstants.drift_nonneg (R H C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) : 0 ≤ drift R H C

theorem EulerPacketCorrectionConstants.drift_div_frequency (R H C k : ℝ) (hk : 0 < k) : 2 * (3 * |k⁻¹| * velocity R H C + normal R H C / k) = drift R H C / k