Actual physical norms and normalized next-frame coupling in the scaled coordinates of source (28). These are identities for the constructed coordinate maps, rather than assumptions on a model system.

def EulerPacketMovingFrame.velocityDenominator (ε r w₃ : ℝ) : ℝ

Velocity denominator, given by 1+ε^2*(r^2+w₃^2).

Equations

• EulerPacketMovingFrame.velocityDenominator ε r w₃ = 1 + ε ^ 2 * (r ^ 2 + w₃ ^ 2)

theorem EulerPacketMovingFrame.velocityDenominator_pos (ε r w₃ : ℝ) : 0 < velocityDenominator ε r w₃

noncomputable def EulerPacketMovingFrame.normalizedCoupling (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (r w : EulerSmoothLimit.Space) : ℝ

Normalized coupling, given by ⟪unit r,M (unit w)⟫_ℝ.

Equations

• EulerPacketMovingFrame.normalizedCoupling M r w = inner ℝ (EulerPacketNormalizedPrimary.unit r) (M (EulerPacketNormalizedPrimary.unit w))

noncomputable def EulerPacketMovingFrame.normalizedTilt (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (r w : EulerSmoothLimit.Space) : ℝ

Normalized tilt, given by ⟪cross (unit r) (unit w),M (unit w)⟫_ℝ/normalizedCoupling M r w.

Equations

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

theorem EulerPacketMovingFrame.normalizedCoupling_eq (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (r w : EulerSmoothLimit.Space) : normalizedCoupling M r w = inner ℝ r (M w) / (‖r‖ * ‖w‖)

theorem EulerPacketMovingFrame.cross_smul_smul (a b : ℝ) (r w : EulerSmoothLimit.Space) : EulerPacketCrossProduct.cross (a • r) (b • w) = (a * b) • EulerPacketCrossProduct.cross r w

theorem EulerPacketMovingFrame.normalizedTilt_eq (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (r w : EulerSmoothLimit.Space) (hr : r ≠ 0) (hw : w ≠ 0) (hflux : inner ℝ r (M w) ≠ 0) : normalizedTilt M r w = inner ℝ (EulerPacketCrossProduct.cross r w) (M w) / (‖w‖ * inner ℝ r (M w))

theorem EulerPacketMovingFrame.scaledRay_norm_sq (m v r : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε τ : ℝ} (hs₀ : s₀ ≠ 0) (hε : ε ≠ 0) (hm : m (physicalTime t₀ a ε τ) ≠ 0) (hv : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) : ‖r (physicalTime t₀ a ε τ)‖ ^ 2 = s₀ ^ 2 * EulerPacketRay.rayDenominator ε (scaledRay m v r s₀ t₀ a ε τ 0) (scaledRay m v r s₀ t₀ a ε τ 1) (scaledRay m v r s₀ t₀ a ε τ 2)

theorem EulerPacketMovingFrame.scaledRay_norm (m v r : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε τ : ℝ} (hs₀ : s₀ ≠ 0) (hε : ε ≠ 0) (hm : m (physicalTime t₀ a ε τ) ≠ 0) (hv : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) : ‖r (physicalTime t₀ a ε τ)‖ = |s₀| * √(EulerPacketRay.rayDenominator ε (scaledRay m v r s₀ t₀ a ε τ 0) (scaledRay m v r s₀ t₀ a ε τ 1) (scaledRay m v r s₀ t₀ a ε τ 2))

theorem EulerPacketMovingFrame.scaledVelocity_norm_sq (m v w : ℝ → EulerSmoothLimit.Space) {t₀ a ε τ : ℝ} (hε : ε ≠ 0) (hm : m (physicalTime t₀ a ε τ) ≠ 0) (hv : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) : ‖w (physicalTime t₀ a ε τ)‖ ^ 2 = ε ^ 2 * scaledVelocity m v w t₀ a ε τ 0 ^ 2 + scaledVelocity m v w t₀ a ε τ 1 ^ 2 + ε ^ 2 * scaledVelocity m v w t₀ a ε τ 2 ^ 2

theorem EulerPacketMovingFrame.scaledVelocity_norm_ratio_sq (m v w : ℝ → EulerSmoothLimit.Space) {t₀ a ε τ : ℝ} (hε : ε ≠ 0) (hm : m (physicalTime t₀ a ε τ) ≠ 0) (hv : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) (hV : scaledVelocity m v w t₀ a ε τ 1 ≠ 0) : ‖w (physicalTime t₀ a ε τ)‖ ^ 2 = scaledVelocity m v w t₀ a ε τ 1 ^ 2 * velocityDenominator ε (scaledVelocity m v w t₀ a ε τ 0 / scaledVelocity m v w t₀ a ε τ 1) (scaledVelocity m v w t₀ a ε τ 2 / scaledVelocity m v w t₀ a ε τ 1)

theorem EulerPacketMovingFrame.scaledVelocity_norm_ratio (m v w : ℝ → EulerSmoothLimit.Space) {t₀ a ε τ : ℝ} (hε : ε ≠ 0) (hm : m (physicalTime t₀ a ε τ) ≠ 0) (hv : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) (hV : scaledVelocity m v w t₀ a ε τ 1 ≠ 0) : ‖w (physicalTime t₀ a ε τ)‖ = |scaledVelocity m v w t₀ a ε τ 1| * √(velocityDenominator ε (scaledVelocity m v w t₀ a ε τ 0 / scaledVelocity m v w t₀ a ε τ 1) (scaledVelocity m v w t₀ a ε τ 2 / scaledVelocity m v w t₀ a ε τ 1))

theorem EulerPacketMovingFrame.physical_primary_size (m v r w : ℝ → EulerSmoothLimit.Space) {s₀ t₀ a ε τ : ℝ} (hs₀ : 0 < s₀) (hε : ε ≠ 0) (hm : m (physicalTime t₀ a ε τ) ≠ 0) (hv : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) (hV : 0 < scaledVelocity m v w t₀ a ε τ 1) : have R := scaledRay m v r s₀ t₀ a ε τ; have V := scaledVelocity m v w t₀ a ε τ; ‖r (physicalTime t₀ a ε τ)‖ * ‖w (physicalTime t₀ a ε τ)‖ = s₀ * √(EulerPacketRay.rayDenominator ε (R 0) (R 1) (R 2)) * V 1 * √(velocityDenominator ε (V 0 / V 1) (V 2 / V 1))

The exact physical size used in source (36), expressed through actual ray and velocity coordinates.