Exact finite-dimensional algebra of the source ray/velocity scaling.

def EulerPacketMovingFrame.velocityScale (ε : ℝ) (i : Fin 3) : ℝ

Velocity scale, with branches according to i = 1.

Equations

• EulerPacketMovingFrame.velocityScale ε i = if i = 1 then 1 else ε

theorem EulerPacketMovingFrame.velocityScale_ne_zero {ε : ℝ} (hε : ε ≠ 0) (i : Fin 3) : velocityScale ε i ≠ 0

theorem EulerPacketMovingFrame.scaling_denominator (s₀ ε : ℝ) (R : Fin 3 → ℝ) : ∑ j : Fin 3, (s₀ * EulerPacketRay.rayScale ε j * R j) ^ 2 = s₀ ^ 2 * EulerPacketRay.rayDenominator ε (R 0) (R 1) (R 2)

theorem EulerPacketMovingFrame.scaling_flux {a : ℝ} (ha : a ≠ 0) (s₀ ε : ℝ) (M : Fin 3 → Fin 3 → ℝ) (R V : Fin 3 → ℝ) : ∑ i : Fin 3, s₀ * EulerPacketRay.rayScale ε i * R i * ∑ j : Fin 3, M i j * (velocityScale ε j * V j) = s₀ * a * EulerPacketRay.velocityNumerator (EulerPacketRay.scaledVelocityEntry a ε M) (R 0) (R 1) (R 2) (V 0) (V 1) (V 2)

theorem EulerPacketMovingFrame.scaling_pairing (s₀ ε : ℝ) (R V : Fin 3 → ℝ) : ∑ i : Fin 3, s₀ * EulerPacketRay.rayScale ε i * R i * (velocityScale ε i * V i) = s₀ * ε * (R 0 * V 0 + R 1 * V 1 + R 2 * V 2)

theorem EulerPacketMovingFrame.scaling_velocity_rate {a ε s₀ D : ℝ} (ha : a ≠ 0) (hε : ε ≠ 0) (hs₀ : s₀ ≠ 0) (hD : D ≠ 0) (M S : Fin 3 → Fin 3 → ℝ) (R V : Fin 3 → ℝ) (J : ℝ) (i : Fin 3) : (-∑ j : Fin 3, (M i j + S i j) * (velocityScale ε j * V j) + 2 * (s₀ * a * J) / (s₀ ^ 2 * D) * (s₀ * EulerPacketRay.rayScale ε i * R i)) * (ε / a) / velocityScale ε i = -∑ j : Fin 3, EulerPacketRay.scaledVelocityEntry a ε (fun (i j : Fin 3) => M i j + S i j) i j * V j + 2 * EulerPacketRay.rayScale ε i ^ 2 * R i * J / D

noncomputable def EulerPacketMovingFrame.scaledVelocityRhs (A C : Fin 3 → Fin 3 → ℝ) (ε : ℝ) (R V : Fin 3 → ℝ) (i : Fin 3) : ℝ

Scaled velocity rhs as an element of ℝ.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerPacketMovingFrame.thirdVelocity_of_pairing (R V : Fin 3 → ℝ) (hN : R 2 ≠ 0) (hRV : R 0 * V 0 + R 1 * V 1 + R 2 * V 2 = 0) : V 2 = EulerPacketRay.velocityThird (R 0) (R 1) (R 2) (V 0) (V 1)

theorem EulerPacketMovingFrame.scaledVelocityRhs_first (A C : Fin 3 → Fin 3 → ℝ) (ε : ℝ) (R V : Fin 3 → ℝ) (hV : V 2 = EulerPacketRay.velocityThird (R 0) (R 1) (R 2) (V 0) (V 1)) : scaledVelocityRhs A C ε R V 0 = EulerPacketRay.velocityFirstRhs A C ε (R 0) (R 1) (R 2) (V 0) (V 1)

theorem EulerPacketMovingFrame.scaledVelocityRhs_second (A C : Fin 3 → Fin 3 → ℝ) (ε : ℝ) (R V : Fin 3 → ℝ) (hV : V 2 = EulerPacketRay.velocityThird (R 0) (R 1) (R 2) (V 0) (V 1)) : scaledVelocityRhs A C ε R V 1 = EulerPacketRay.velocitySecondRhs A C ε (R 0) (R 1) (R 2) (V 0) (V 1)