Physical operator bounds and the actual homogeneous primary imply the small scaled matrix errors used in source propagation. The fixed numerical loss absorbs rotation of the normalized frame.

noncomputable def EulerPacketMovingFrame.rescaledFrame (B : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m v : ℝ → EulerSmoothLimit.Space) (t₀ a ε τ : ℝ) : Fin 3 → Fin 3 → ℝ

Rescaled frame, given by frameMatrix (B (physicalTime t₀ a ε τ)) (unit (m (physicalTime t₀ a ε τ))) (unit (v (physicalTime t₀ a ε τ))).

Equations

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

noncomputable def EulerPacketMovingFrame.rescaledShear (c : ℝ) (m v : ℝ → EulerSmoothLimit.Space) (t₀ a ε τ : ℝ) : ℝ

Rescaled shear, given by primaryShear c m v (physicalTime t₀ a ε τ).

Equations

• EulerPacketMovingFrame.rescaledShear c m v t₀ a ε τ = EulerPacketMovingFrame.primaryShear c m v (EulerPacketMovingFrame.physicalTime t₀ a ε τ)

theorem EulerPacketMovingFrame.physical_matrix_errors {B B₁ M E : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} {m v : ℝ → EulerSmoothLimit.Space} {c t₀ a ε Θ G d β : ℝ} {S : Set ℝ} (ha : 1 / 2 ≤ a) (hε : 0 < ε) (hΘ : 1 ≤ Θ) (hG : 1 ≤ G) (hd : 0 ≤ d) (hsmall : 16 * (ε * Θ * (4 * G) ^ 2 + d) ≤ 1) (hmap : Set.MapsTo (physicalTime t₀ a ε) (Set.Icc 0 Θ) S) (hBd : ∀ t ∈ S, HasDerivWithinAt B (B₁ t) S t) (hmd : ∀ t ∈ S, HasDerivWithinAt m (-(ContinuousLinearMap.adjoint (B t)) (m t)) S t) (hvd : ∀ t ∈ S, HasDerivWithinAt v (-(B t) (v t) + (2 * inner ℝ (m t) ((B t) (v t)) / ‖m t‖ ^ 2) • m t) S t) (hm0 : ∀ t ∈ S, m t ≠ 0) (hv0 : ∀ t ∈ S, v t ≠ 0) (hmv : ∀ t ∈ S, inner ℝ (m t) (v t) = 0) (hB : ∀ t ∈ S, ‖B t‖ ≤ G) (hB₁ : ∀ t ∈ S, ‖B₁ t‖ ≤ G ^ 2) (hE : ∀ t ∈ S, ‖E t‖ ≤ d) (hparent : ∀ t ∈ S, M t = B t + primaryShear c m v t • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit (v t))) (EulerPacketNormalizedPrimary.unit (m t)) + E t) (hb0 : rescaledFrame B m v t₀ a ε 0 0 1 = a) (hk0 : rescaledFrame B m v t₀ a ε 0 2 1 = a * β) (hh0 : rescaledShear c m v t₀ a ε 0 = a / ε ^ 2) : have e := 16 * (ε * Θ * (4 * G) ^ 2 + d); ε ≤ e ∧ ∀ τ ∈ Set.Icc 0 Θ, (∀ (i j : Fin 3), |EulerPacketRay.scaledRayEntry a ε (rescaledFrame M m v t₀ a ε τ) (EulerPacketRay.frameSkew (rescaledFrame B m v t₀ a ε τ)) i j - EulerPacketRay.idealRayEntry β i j| ≤ 4 * e) ∧ (∀ (i j : Fin 3), |EulerPacketRay.scaledVelocityEntry a ε (rescaledFrame M m v t₀ a ε τ) i j - EulerPacketRay.idealVelocityEntry β i j| ≤ 3 * e) ∧ ∀ (j : Fin 3), |EulerPacketRay.scaledVelocityEntry a ε (fun (i j : Fin 3) => rescaledFrame M m v t₀ a ε τ i j + EulerPacketRay.frameSkew (rescaledFrame B m v t₀ a ε τ) i j) 0 j - EulerPacketRay.idealUnprojectedEntry 0 j| ≤ 5 * e ∧ |EulerPacketRay.scaledVelocityEntry a ε (fun (i j : Fin 3) => rescaledFrame M m v t₀ a ε τ i j + EulerPacketRay.frameSkew (rescaledFrame B m v t₀ a ε τ) i j) 1 j - EulerPacketRay.idealUnprojectedEntry 1 j| ≤ 5 * e

All three coefficient-error bounds follow from physical norm and time derivative bounds. In particular, no frame-motion or scaled matrix bound appears as a hypothesis.