Packet Coefficient Control

theorem EulerPacketCoefficientControl.motion_displacement_bound {Θ L : ℝ} {f f₁ : ℝ → ℝ} (_hΘ : 0 ≤ Θ) (hL : 0 ≤ L) (hf : ∀ t ∈ Set.Icc 0 Θ, HasDerivAt f (f₁ t) t) (hb : ∀ t ∈ Set.Icc 0 Θ, |f₁ t| ≤ L) (t : ℝ) : t ∈ Set.Icc 0 Θ → |f t - f 0| ≤ L * Θ

A derivative bound controls the change of a scalar coefficient on the entire finite time interval.

theorem EulerPacketCoefficientControl.multiplicative_motion_bound {Θ k : ℝ} {H H₁ : ℝ → ℝ} (hΘ : 0 ≤ Θ) (hk : 0 ≤ k) (hsmall : k * Θ ≤ 1 / 2) (hH : ∀ t ∈ Set.Icc 0 Θ, HasDerivAt H (H₁ t) t) (hH0 : H 0 = 1) (hb : ∀ t ∈ Set.Icc 0 Θ, |H₁ t| ≤ k * |H t|) (t : ℝ) : t ∈ Set.Icc 0 Θ → |H t| ≤ 2 ∧ |H t - 1| ≤ 2 * k * Θ

A multiplicative differential bound keeps the normalized shear near one. Positivity or an a priori shear bound is not assumed.

theorem EulerPacketCoefficientControl.normalized_motion_errors {a ε Θ G d β : ℝ} {B E : ℝ → Fin 3 → Fin 3 → ℝ} {h h₁ b₁ k₁ : ℝ → ℝ} (ha : 1 / 2 ≤ a) (hε : 0 < ε) (hΘ : 1 ≤ Θ) (hG : 1 ≤ G) (hd : 0 ≤ d) (hsmall : 16 * (ε * Θ * G ^ 2 + d) ≤ 1) (hB : ∀ t ∈ Set.Icc 0 Θ, ∀ (i j : Fin 3), |B t i j| ≤ G) (hE : ∀ t ∈ Set.Icc 0 Θ, ∀ (i j : Fin 3), |E t i j| ≤ d) (hb : ∀ t ∈ Set.Icc 0 Θ, HasDerivAt (fun (s : ℝ) => B s 0 1) (b₁ t) t) (hk : ∀ t ∈ Set.Icc 0 Θ, HasDerivAt (fun (s : ℝ) => B s 2 1) (k₁ t) t) (hbBound : ∀ t ∈ Set.Icc 0 Θ, |b₁ t| ≤ 2 * ε * G ^ 2) (hkBound : ∀ t ∈ Set.Icc 0 Θ, |k₁ t| ≤ 2 * ε * G ^ 2) (hShear : ∀ t ∈ Set.Icc 0 Θ, HasDerivAt h (h₁ t) t) (hShearBound : ∀ t ∈ Set.Icc 0 Θ, |h₁ t| ≤ 4 * ε * G * |h t|) (hb0 : B 0 0 1 = a) (hk0 : B 0 2 1 = a * β) (hh0 : h 0 = a / ε ^ 2) : have e := 16 * (ε * Θ * G ^ 2 + d); ε ≤ e ∧ ∀ t ∈ Set.Icc 0 Θ, (∀ (i j : Fin 3), |ε * B t i j / a| ≤ e) ∧ (∀ (i j : Fin 3), |E t i j / a| ≤ e) ∧ |ε ^ 2 * h t / a - 1| ≤ e ∧ |B t 0 1 / a - 1| ≤ e ∧ |B t 2 1 / a - β| ≤ e

Raw moving-frame coefficient motion implies the normalized error bounds used in the ray and velocity reductions.

theorem EulerPacketCoefficientControl.raw_frame_matrix_errors {a ε e β h : ℝ} {B E : Fin 3 → Fin 3 → ℝ} (ha : a ≠ 0) (hε : 0 < ε) (hεe : ε ≤ e) (he : 0 ≤ e) (heSmall : e ≤ 1) (hB : ∀ (i j : Fin 3), |ε * B i j / a| ≤ e) (hE : ∀ (i j : Fin 3), |E i j / a| ≤ e) (hH : |ε ^ 2 * h / a - 1| ≤ e) (hα : |B 0 1 / a - 1| ≤ e) (hκ : |B 2 1 / a - β| ≤ e) : (∀ (i j : Fin 3), |EulerPacketRay.scaledRayEntry a ε (EulerPacketRay.parentEntry B E h) (EulerPacketRay.frameSkew B) i j - EulerPacketRay.idealRayEntry β i j| ≤ 4 * e) ∧ (∀ (i j : Fin 3), |EulerPacketRay.scaledVelocityEntry a ε (EulerPacketRay.parentEntry B E h) i j - EulerPacketRay.idealVelocityEntry β i j| ≤ 3 * e) ∧ ∀ (j : Fin 3), |EulerPacketRay.scaledVelocityEntry a ε (fun (i j : Fin 3) => EulerPacketRay.parentEntry B E h i j + EulerPacketRay.frameSkew B i j) 0 j - EulerPacketRay.idealUnprojectedEntry 0 j| ≤ 5 * e ∧ |EulerPacketRay.scaledVelocityEntry a ε (fun (i j : Fin 3) => EulerPacketRay.parentEntry B E h i j + EulerPacketRay.frameSkew B i j) 1 j - EulerPacketRay.idealUnprojectedEntry 1 j| ≤ 5 * e

The exact raw moving-frame matrices satisfy the coefficient-error hypotheses of the controlled-stage theorem.