The actual ray in the source time and coordinate scaling.

noncomputable def EulerPacketMovingFrame.physicalTime (t₀ a ε τ : ℝ) : ℝ

Physical time, given by t₀ + (ε/a)*τ.

Equations

• EulerPacketMovingFrame.physicalTime t₀ a ε τ = t₀ + ε / a * τ

theorem EulerPacketMovingFrame.physicalTime_hasDerivAt (t₀ a ε τ : ℝ) : HasDerivAt (physicalTime t₀ a ε) (ε / a) τ

theorem EulerPacketMovingFrame.rayScale_ne_zero {ε : ℝ} (hε : ε ≠ 0) (i : Fin 3) : EulerPacketRay.rayScale ε i ≠ 0

theorem EulerPacketMovingFrame.scaledRayRate_algebra {a ε s₀ : ℝ} (ha : a ≠ 0) (hε : ε ≠ 0) (hs₀ : s₀ ≠ 0) (M S : Fin 3 → Fin 3 → ℝ) (R : Fin 3 → ℝ) (i : Fin 3) : (-∑ j : Fin 3, (M j i - S j i) * R j) * (ε / a) / (s₀ * EulerPacketRay.rayScale ε i) = ∑ j : Fin 3, EulerPacketRay.scaledRayEntry a ε M S i j * (R j / (s₀ * EulerPacketRay.rayScale ε j))

noncomputable def EulerPacketMovingFrame.scaledRay (m v r : ℝ → EulerSmoothLimit.Space) (s₀ t₀ a ε τ : ℝ) (i : Fin 3) : ℝ

Scaled ray, given by movingRay m v r (physicalTime t₀ a ε τ) i / (s₀*rayScale ε i).

Equations

• EulerPacketMovingFrame.scaledRay m v r s₀ t₀ a ε τ i = EulerPacketMovingFrame.movingRay m v r (EulerPacketMovingFrame.physicalTime t₀ a ε τ) i / (s₀ * EulerPacketRay.rayScale ε i)

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

The physical ODE supplies exactly the scaled coefficient matrix whose entrywise errors are controlled in the existing propagation proof.

theorem EulerPacketMovingFrame.scaledRay_hasDerivWithinAt (B M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) {m v r : ℝ → EulerSmoothLimit.Space} {s₀ t₀ a ε τ : ℝ} {S U : Set ℝ} (ha : a ≠ 0) (hε : ε ≠ 0) (hs₀ : s₀ ≠ 0) (hmap : Set.MapsTo (physicalTime t₀ a ε) U S) (hm : HasDerivWithinAt m (-(ContinuousLinearMap.adjoint B) (m (physicalTime t₀ a ε τ))) S (physicalTime t₀ a ε τ)) (hv : HasDerivWithinAt v (-B (v (physicalTime t₀ a ε τ)) + (2 * inner ℝ (m (physicalTime t₀ a ε τ)) (B (v (physicalTime t₀ a ε τ))) / ‖m (physicalTime t₀ a ε τ)‖ ^ 2) • m (physicalTime t₀ a ε τ)) S (physicalTime t₀ a ε τ)) (hr : HasDerivWithinAt r (-(ContinuousLinearMap.adjoint M) (r (physicalTime t₀ a ε τ))) S (physicalTime t₀ a ε τ)) (hm0 : m (physicalTime t₀ a ε τ) ≠ 0) (hv0 : v (physicalTime t₀ a ε τ) ≠ 0) (hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0) (i : Fin 3) : HasDerivWithinAt (fun (σ : ℝ) => scaledRay m v r s₀ t₀ a ε σ i) (∑ j : Fin 3, EulerPacketRay.scaledRayEntry a ε (frameMatrix M (EulerPacketNormalizedPrimary.unit (m (physicalTime t₀ a ε τ))) (EulerPacketNormalizedPrimary.unit (v (physicalTime t₀ a ε τ)))) (EulerPacketRay.frameSkew (frameMatrix B (EulerPacketNormalizedPrimary.unit (m (physicalTime t₀ a ε τ))) (EulerPacketNormalizedPrimary.unit (v (physicalTime t₀ a ε τ))))) i j * scaledRay m v r s₀ t₀ a ε τ j) U τ

The same rescaling for actual one-sided time derivatives.