The oriented orthonormal frame built from the actual normalized primary. Its angular-velocity entries are derived from the physical ODEs and agree with the frameSkew matrix used in the source propagation estimates.

noncomputable def EulerPacketMovingFrame.crossBilinear : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Cross bilinear as an element of Space →L[ℝ] Space →L[ℝ] Space.

Equations

• EulerPacketMovingFrame.crossBilinear = { toFun := EulerPacketCrossProduct.crossLeft, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

theorem EulerPacketMovingFrame.crossBilinear_apply (a b : EulerSmoothLimit.Space) : (crossBilinear a) b = EulerPacketCrossProduct.cross a b

theorem EulerPacketMovingFrame.cross_hasDerivAt {p q : ℝ → EulerSmoothLimit.Space} {p' q' : EulerSmoothLimit.Space} {t : ℝ} (hp : HasDerivAt p p' t) (hq : HasDerivAt q q' t) : HasDerivAt (fun (s : ℝ) => EulerPacketCrossProduct.cross (p s) (q s)) (EulerPacketCrossProduct.cross p' (q t) + EulerPacketCrossProduct.cross (p t) q') t

theorem EulerPacketMovingFrame.cross_hasDerivWithinAt {p q : ℝ → EulerSmoothLimit.Space} {p' q' : EulerSmoothLimit.Space} {t : ℝ} {S : Set ℝ} (hp : HasDerivWithinAt p p' S t) (hq : HasDerivWithinAt q q' S t) : HasDerivWithinAt (fun (s : ℝ) => EulerPacketCrossProduct.cross (p s) (q s)) (EulerPacketCrossProduct.cross p' (q t) + EulerPacketCrossProduct.cross (p t) q') S t

theorem EulerPacketMovingFrame.inner_cross_first (p q : EulerSmoothLimit.Space) : inner ℝ p (EulerPacketCrossProduct.cross p q) = 0

theorem EulerPacketMovingFrame.inner_cross_second (p q : EulerSmoothLimit.Space) : inner ℝ q (EulerPacketCrossProduct.cross p q) = 0

theorem EulerPacketMovingFrame.inner_cross_cross (p q r s : EulerSmoothLimit.Space) : inner ℝ (EulerPacketCrossProduct.cross p q) (EulerPacketCrossProduct.cross r s) = inner ℝ p r * inner ℝ q s - inner ℝ p s * inner ℝ q r

theorem EulerPacketMovingFrame.inner_cross_exchange_first (p q r : EulerSmoothLimit.Space) : inner ℝ p (EulerPacketCrossProduct.cross q r) = -inner ℝ q (EulerPacketCrossProduct.cross p r)

theorem EulerPacketMovingFrame.inner_cross_exchange_last (p q r : EulerSmoothLimit.Space) : inner ℝ p (EulerPacketCrossProduct.cross q r) = -inner ℝ r (EulerPacketCrossProduct.cross q p)

def EulerPacketMovingFrame.frame (p q : EulerSmoothLimit.Space) : Fin 3 → EulerSmoothLimit.Space

Frame, given by ![p, q, cross p q].

Equations

• EulerPacketMovingFrame.frame p q = ![p, q, EulerPacketCrossProduct.cross p q]

noncomputable def EulerPacketMovingFrame.frameRate (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q : EulerSmoothLimit.Space) : Fin 3 → EulerSmoothLimit.Space

Frame rate, given by ![rayRate B p, velocityRate B p q, cross (rayRate B p) q + cross p (velocityRate B p q)].

Equations

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

noncomputable def EulerPacketMovingFrame.frameMatrix (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q : EulerSmoothLimit.Space) (i j : Fin 3) : ℝ

Frame matrix, given by ⟪frame p q i, B (frame p q j)⟫_ℝ.

Equations

• EulerPacketMovingFrame.frameMatrix B p q i j = inner ℝ (EulerPacketMovingFrame.frame p q i) (B (EulerPacketMovingFrame.frame p q j))

theorem EulerPacketMovingFrame.frame_orthonormal (p q : EulerSmoothLimit.Space) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) : Orthonormal ℝ (frame p q)

noncomputable def EulerPacketMovingFrame.frameBasis (p q : EulerSmoothLimit.Space) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) : OrthonormalBasis (Fin 3) ℝ EulerSmoothLimit.Space

Frame basis, constructed using OrthonormalBasis.mk.

Equations

• EulerPacketMovingFrame.frameBasis p q hp hq hpq = OrthonormalBasis.mk ⋯ ⋯

theorem EulerPacketMovingFrame.frameBasis_apply (p q : EulerSmoothLimit.Space) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) (i : Fin 3) : (frameBasis p q hp hq hpq) i = frame p q i

theorem EulerPacketMovingFrame.frameRate_skew (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q : EulerSmoothLimit.Space) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) (i j : Fin 3) : inner ℝ (frame p q i) (frameRate B p q j) = EulerPacketRay.frameSkew (frameMatrix B p q) i j

All nine entries of the actual frame rate, including their signs.

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

Normalized frame, given by frame (unit (m t)) (unit (v t)).

Equations

• EulerPacketMovingFrame.normalizedFrame m v t = EulerPacketMovingFrame.frame (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t))

theorem EulerPacketMovingFrame.normalizedFrame_hasDerivAt (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {m v : ℝ → 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) (hm0 : m t ≠ 0) (hv0 : v t ≠ 0) (hmv : inner ℝ (m t) (v t) = 0) (i : Fin 3) : HasDerivAt (fun (s : ℝ) => normalizedFrame m v s i) (frameRate B (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t)) i) t

theorem EulerPacketMovingFrame.normalizedFrame_hasDerivWithinAt (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {m v : ℝ → 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) (hm0 : m t ≠ 0) (hv0 : v t ≠ 0) (hmv : inner ℝ (m t) (v t) = 0) (i : Fin 3) : HasDerivWithinAt (fun (s : ℝ) => normalizedFrame m v s i) (frameRate B (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t)) i) S t

theorem EulerPacketMovingFrame.normalizedFrame_skew (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {m v : ℝ → 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) (hm0 : m t ≠ 0) (hv0 : v t ≠ 0) (hmv : inner ℝ (m t) (v t) = 0) (i j : Fin 3) : inner ℝ (normalizedFrame m v t i) (deriv (fun (s : ℝ) => normalizedFrame m v s j) t) = EulerPacketRay.frameSkew (frameMatrix B (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t))) i j

The source skew matrix is now identified with the derivative of the actual normalized ray/velocity frame.