The physical parent decomposition and moving-frame coefficient bounds in source (23). Frame motion and primary shear motion are derived from the actual homogeneous ray and velocity equations.

theorem EulerPacketMovingFrame.abs_inner_map_le (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {p q : EulerSmoothLimit.Space} (hp : ‖p‖ = 1) (hq : ‖q‖ = 1) : |inner ℝ p (B q)| ≤ ‖B‖

theorem EulerPacketMovingFrame.frameMatrix_abs_le (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) : |frameMatrix B p q i j| ≤ ‖B‖

theorem EulerPacketMovingFrame.frameMatrix_parent (B E : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (h : ℝ) (p q : EulerSmoothLimit.Space) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) : frameMatrix (B + h • ((InnerProductSpace.rankOne ℝ) q) p + E) p q = EulerPacketRay.parentEntry (frameMatrix B p q) (frameMatrix E p q) h

The shear is exactly the (q,p) entry in the actual orthonormal frame.

theorem EulerPacketMovingFrame.rayRate_norm_le (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {p : EulerSmoothLimit.Space} (hp : ‖p‖ = 1) : ‖EulerPacketNormalizedPrimary.rayRate B p‖ ≤ 2 * ‖B‖

theorem EulerPacketMovingFrame.velocityRate_norm_le (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {p q : EulerSmoothLimit.Space} (hp : ‖p‖ = 1) (hq : ‖q‖ = 1) : ‖EulerPacketNormalizedPrimary.velocityRate B p q‖ ≤ 4 * ‖B‖

theorem EulerPacketMovingFrame.frameRate_norm_le (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q : EulerSmoothLimit.Space) (hp : ‖p‖ = 1) (hq : ‖q‖ = 1) (i : Fin 3) : ‖frameRate B p q i‖ ≤ 6 * ‖B‖

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

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

Equations

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

theorem EulerPacketMovingFrame.frameMatrix_hasDerivWithinAt {B : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} {B₁ : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} {m v : ℝ → EulerSmoothLimit.Space} {t : ℝ} {S : Set ℝ} (hB : HasDerivWithinAt B B₁ S t) (hm : HasDerivWithinAt m (-(ContinuousLinearMap.adjoint (B t)) (m t)) S t) (hv : HasDerivWithinAt v (-(B t) (v t) + (2 * inner ℝ (m t) ((B t) (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 j : Fin 3) : HasDerivWithinAt (fun (s : ℝ) => frameMatrix (B s) (EulerPacketNormalizedPrimary.unit (m s)) (EulerPacketNormalizedPrimary.unit (v s)) i j) (frameMatrixRate (B t) B₁ (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t)) i j) S t

theorem EulerPacketMovingFrame.frameMatrixRate_abs_le (B 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) : |frameMatrixRate B B₁ p q i j| ≤ ‖B₁‖ + 12 * ‖B‖ ^ 2

noncomputable def EulerPacketMovingFrame.primaryShear (c : ℝ) (m v : ℝ → EulerSmoothLimit.Space) (t : ℝ) : ℝ

Primary shear, given by c*(‖m t‖*‖v t‖).

Equations

• EulerPacketMovingFrame.primaryShear c m v t = c * (‖m t‖ * ‖v t‖)

theorem EulerPacketMovingFrame.primaryShear_hasDerivWithinAt (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (c : ℝ) {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) : HasDerivWithinAt (primaryShear c m v) (-(frameMatrix B (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t)) 0 0 + frameMatrix B (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t)) 1 1) * primaryShear c m v t) S t

In particular, the logarithmic shear law in source (23) holds for the actual amplitude c * ‖m‖ * ‖v‖.

theorem EulerPacketMovingFrame.primaryShear_rate_bound (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (c : ℝ) (m v : ℝ → EulerSmoothLimit.Space) (t : ℝ) (hm0 : m t ≠ 0) (hv0 : v t ≠ 0) (hmv : inner ℝ (m t) (v t) = 0) : |-(frameMatrix B (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t)) 0 0 + frameMatrix B (EulerPacketNormalizedPrimary.unit (m t)) (EulerPacketNormalizedPrimary.unit (v t)) 1 1) * primaryShear c m v t| ≤ 2 * ‖B‖ * |primaryShear c m v t|