The physical ray ODE in the actual normalized moving frame.

theorem EulerPacketMovingFrame.frame_inner_expand (p q : EulerSmoothLimit.Space) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) (x y : EulerSmoothLimit.Space) : ∑ j : Fin 3, inner ℝ (frame p q j) x * inner ℝ (frame p q j) y = inner ℝ x y

theorem EulerPacketMovingFrame.movingRayRate_identity (B M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q x : EulerSmoothLimit.Space) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) (i : Fin 3) : -inner ℝ (M (frame p q i)) x + inner ℝ (frameRate B p q i) x = -∑ j : Fin 3, (frameMatrix M p q j i - EulerPacketRay.frameSkew (frameMatrix B p q) j i) * inner ℝ (frame p q j) x

noncomputable def EulerPacketMovingFrame.movingRay (m v r : ℝ → EulerSmoothLimit.Space) (t : ℝ) (i : Fin 3) : ℝ

Moving ray, given by ⟪normalizedFrame m v t i,r t⟫_ℝ.

Equations

• EulerPacketMovingFrame.movingRay m v r t i = inner ℝ (EulerPacketMovingFrame.normalizedFrame m v t i) (r t)

theorem EulerPacketMovingFrame.movingRay_hasDerivAt (B M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {m v r : ℝ → EulerSmoothLimit.Space} {t : ℝ} (hm : HasDerivAt m (-(ContinuousLinearMap.adjoint B) (m t)) t) (hv : HasDerivAt v (-B (v t) + (2 * inner ℝ (m t) (B (v t)) / ‖m t‖ ^ 2) • m t) t) (hr : HasDerivAt r (-(ContinuousLinearMap.adjoint M) (r t)) t) (hm0 : m t ≠ 0) (hv0 : v t ≠ 0) (hmv : inner ℝ (m t) (v t) = 0) (i : Fin 3) : HasDerivAt (fun (s : ℝ) => movingRay m v r s i) (-∑ j : Fin 3, (frameMatrix M (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t)) j i - EulerPacketRay.frameSkew (frameMatrix B (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t))) j i) * movingRay m v r t j) t

The actual moving-coordinate ray obeys -(M-S)ᵀ, with the skew matrix already derived from the older primary ODE.

theorem EulerPacketMovingFrame.movingRay_hasDerivWithinAt (B M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {m v r : ℝ → EulerSmoothLimit.Space} {t : ℝ} {S : Set ℝ} (hm : HasDerivWithinAt m (-(ContinuousLinearMap.adjoint B) (m t)) S t) (hv : HasDerivWithinAt v (-B (v t) + (2 * inner ℝ (m t) (B (v t)) / ‖m t‖ ^ 2) • m t) S t) (hr : HasDerivWithinAt r (-(ContinuousLinearMap.adjoint M) (r t)) S t) (hm0 : m t ≠ 0) (hv0 : v t ≠ 0) (hmv : inner ℝ (m t) (v t) = 0) (i : Fin 3) : HasDerivWithinAt (fun (s : ℝ) => movingRay m v r s i) (-∑ j : Fin 3, (frameMatrix M (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t)) j i - EulerPacketRay.frameSkew (frameMatrix B (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t))) j i) * movingRay m v r t j) S t

The same physical coordinate equation holds with one-sided endpoint derivatives.