The normalized physical equations retain the actual neighboring initial discrepancy. The scalar comparison solutions below are constructed, and the third ray coordinate and all denominator bounds follow from the ray equation.

Relative stability with an actual initial velocity discrepancy. This keeps the neighbor-data contribution in the Duhamel estimate rather than requiring the perturbed velocity to have exactly the center initial data.

theorem EulerPacketMovingFrame.velocity_difference_bound {σ Θ T e : ℝ} {F F₁ G G₁ Z Z₁ U U₁ V V₁ : ℝ → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hT0 : 0 ≤ T) (hT : T ≤ Θ) (he : 0 ≤ e) (hsmall : 40 * e * Θ ^ 21 ≤ 1) (hF : ∀ (t : ℝ), 0 ≤ t → HasDerivAt F (F₁ t) t) (hG : ∀ (t : ℝ), 0 ≤ t → HasDerivAt G (G₁ t) t) (hfluxF : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * F₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * F t) t) (hfluxG : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * G₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * G t) t) (hF0 : F 0 = 1) (hF₁0 : F₁ 0 = 0) (hG₁0 : G₁ 0 = 1) (hU : ∀ t ∈ Set.Icc 0 T, HasDerivAt U (U₁ t) t) (hV : ∀ t ∈ Set.Icc 0 T, HasDerivAt V (V₁ t) t) (hU₁c : ContinuousOn U₁ (Set.Icc 0 T)) (hV₁c : ContinuousOn V₁ (Set.Icc 0 T)) (hZ : ∀ t ∈ Set.Icc 0 T, HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ t ∈ Set.Icc 0 T, HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (herror : ∀ t ∈ Set.Icc 0 T, |U₁ t - EulerPacketBridge.idealVelocityFirst (σ ^ 2) t (U t) (V t)| + |V₁ t + U t| ≤ e * Θ ^ 12 * (|U t| + |V t|)) (t : ℝ) : t ∈ Set.Icc 0 T → |V t - Z t| + |U t + Z₁ t| ≤ 20 * Θ ^ 8 * F t * (|V 0 - Z 0| + |U 0 + Z₁ 0|) + 800 * e * Θ ^ 29 * F t * (|V 0| + |U 0|)

theorem EulerPacketMovingFrame.velocity_difference_bound_within {σ Θ T e : ℝ} {F F₁ G G₁ Z Z₁ U U₁ V V₁ : ℝ → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hT0 : 0 < T) (hT : T ≤ Θ) (he : 0 ≤ e) (hsmall : 40 * e * Θ ^ 21 ≤ 1) (hF : ∀ (t : ℝ), 0 ≤ t → HasDerivAt F (F₁ t) t) (hG : ∀ (t : ℝ), 0 ≤ t → HasDerivAt G (G₁ t) t) (hfluxF : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * F₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * F t) t) (hfluxG : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * G₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * G t) t) (hF0 : F 0 = 1) (hF₁0 : F₁ 0 = 0) (hG₁0 : G₁ 0 = 1) (hU : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt U (U₁ t) (Set.Icc 0 T) t) (hV : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt V (V₁ t) (Set.Icc 0 T) t) (hU₁c : ContinuousOn U₁ (Set.Icc 0 T)) (hV₁c : ContinuousOn V₁ (Set.Icc 0 T)) (hZ : ∀ t ∈ Set.Icc 0 T, HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ t ∈ Set.Icc 0 T, HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (herror : ∀ t ∈ Set.Icc 0 T, |U₁ t - EulerPacketBridge.idealVelocityFirst (σ ^ 2) t (U t) (V t)| + |V₁ t + U t| ≤ e * Θ ^ 12 * (|U t| + |V t|)) (t : ℝ) : t ∈ Set.Icc 0 T → |V t - Z t| + |U t + Z₁ t| ≤ 20 * Θ ^ 8 * F t * (|V 0 - Z 0| + |U 0 + Z₁ 0|) + 800 * e * Θ ^ 29 * F t * (|V 0| + |U 0|)

theorem EulerPacketMovingFrame.neighbor_initial_error_bound {Θ e η lam Ft u₀ v₀ L : ℝ} (hΘ : 1 ≤ Θ) (he : 0 ≤ e) (hlam : 0 ≤ lam) (hFt : 0 ≤ Ft) (hi : |v₀ - 1| + |u₀ + lam| ≤ η) (hb : L ≤ 20 * Θ ^ 8 * Ft * (|v₀ - 1| + |u₀ + lam|) + 800 * e * Θ ^ 29 * Ft * (|v₀| + |u₀|)) : L ≤ (20 * η * Θ ^ 8 + 800 * e * Θ ^ 29 * (1 + lam + η)) * Ft

Converting the retained initial discrepancy to the source's neighbor normalization costs no additional power of Θ.

theorem EulerPacketMovingFrame.ray_controlled_velocity_error_within {β Θ T e ε : ℝ} {R A C : ℝ → Fin 3 → Fin 3 → ℝ} {P Q N : ℝ → ℝ} (hβ : 0 ≤ β) (hβupper : β ≤ 1) (hΘ : 1 ≤ Θ) (hT0 : 0 < T) (hT : T ≤ Θ) (he : 0 ≤ e) (hε : 0 ≤ ε) (hεe : ε ≤ e) (hsmall : 10000 * e * Θ ^ 5 ≤ 1) (hRc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => R t i j) (Set.Icc 0 T)) (hP : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt P (R t 0 0 * P t + R t 0 1 * Q t + R t 0 2 * N t) (Set.Icc 0 T) t) (hQ : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Q (R t 1 0 * P t + R t 1 1 * Q t + R t 1 2 * N t) (Set.Icc 0 T) t) (hN : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt N (R t 2 0 * P t + R t 2 1 * Q t + R t 2 2 * N t) (Set.Icc 0 T) t) (hRclose : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), |R t i j - EulerPacketRay.idealRayEntry β i j| ≤ 4 * e) (hAclose : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), |A t i j - EulerPacketRay.idealVelocityEntry β i j| ≤ 3 * e) (hCclose : ∀ t ∈ Set.Icc 0 T, ∀ (j : Fin 3), |C t 0 j - EulerPacketRay.idealUnprojectedEntry 0 j| ≤ 5 * e ∧ |C t 1 j - EulerPacketRay.idealUnprojectedEntry 1 j| ≤ 5 * e) (hinitial : EulerPacketRay.norm3 (P 0) (Q 0) (N 0 - 1) ≤ e) (t : ℝ) : t ∈ Set.Icc 0 T → (EulerPacketRay.norm3 (P t - β * t ^ 2) (Q t + 2 * β * t) (N t - 1) ≤ 800 * e * Θ ^ 5 ∧ 1 / 2 ≤ N t) ∧ ∀ (U V : ℝ), |EulerPacketRay.velocityFirstRhs (A t) (C t) ε (P t) (Q t) (N t) U V - EulerPacketBridge.idealVelocityFirst β t U V| + |EulerPacketRay.velocitySecondRhs (A t) (C t) ε (P t) (Q t) (N t) U V + U| ≤ 200000 * e * Θ ^ 12 * (|U| + |V|)

theorem EulerPacketMovingFrame.controlled_neighbor_relative_error_within {σ Θ T e ε lam : ℝ} {F F₁ G G₁ Z Z₁ U V P Q N : ℝ → ℝ} {R A C : ℝ → Fin 3 → Fin 3 → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hT0 : 0 < T) (hT : T ≤ Θ) (he : 0 ≤ e) (hε : 0 ≤ ε) (hεe : ε ≤ e) (hlam : 0 ≤ lam) (hsmall : 8000000 * e * Θ ^ 21 ≤ 1) (hF : ∀ (t : ℝ), 0 ≤ t → HasDerivAt F (F₁ t) t) (hG : ∀ (t : ℝ), 0 ≤ t → HasDerivAt G (G₁ t) t) (hfluxF : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * F₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * F t) t) (hfluxG : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * G₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * G t) t) (hF0 : F 0 = 1) (hF₁0 : F₁ 0 = 0) (hG₁0 : G₁ 0 = 1) (hRc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => R t i j) (Set.Icc 0 T)) (hAc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => A t i j) (Set.Icc 0 T)) (hCc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => C t i j) (Set.Icc 0 T)) (hP : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt P (R t 0 0 * P t + R t 0 1 * Q t + R t 0 2 * N t) (Set.Icc 0 T) t) (hQ : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Q (R t 1 0 * P t + R t 1 1 * Q t + R t 1 2 * N t) (Set.Icc 0 T) t) (hN : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt N (R t 2 0 * P t + R t 2 1 * Q t + R t 2 2 * N t) (Set.Icc 0 T) t) (hU : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt U (EulerPacketRay.velocityFirstRhs (A t) (C t) ε (P t) (Q t) (N t) (U t) (V t)) (Set.Icc 0 T) t) (hV : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt V (EulerPacketRay.velocitySecondRhs (A t) (C t) ε (P t) (Q t) (N t) (U t) (V t)) (Set.Icc 0 T) t) (hRclose : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), |R t i j - EulerPacketRay.idealRayEntry (σ ^ 2) i j| ≤ 4 * e) (hAclose : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), |A t i j - EulerPacketRay.idealVelocityEntry (σ ^ 2) i j| ≤ 3 * e) (hCclose : ∀ t ∈ Set.Icc 0 T, ∀ (j : Fin 3), |C t 0 j - EulerPacketRay.idealUnprojectedEntry 0 j| ≤ 5 * e ∧ |C t 1 j - EulerPacketRay.idealUnprojectedEntry 1 j| ≤ 5 * e) (hZ : ∀ t ∈ Set.Icc 0 T, HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ t ∈ Set.Icc 0 T, HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) (hrayInitial : EulerPacketRay.norm3 (P 0) (Q 0) (N 0 - 1) ≤ e) (hvelocityInitial : |V 0 - 1| + |U 0 + lam| ≤ e) (hZ0 : Z 0 = 1) (hZ₁0 : Z₁ 0 = lam) (t : ℝ) : t ∈ Set.Icc 0 T → |V t - Z t| + |U t + Z₁ t| ≤ 400000000 * e * Θ ^ 29 * (1 + lam) * F t

noncomputable def EulerPacketMovingFrame.neighborStabilityConstant : ℝ

Neighbor stability constant, given by 1000000000*exp 6.

Equations

• EulerPacketMovingFrame.neighborStabilityConstant = 1000000000 * Real.exp 6

theorem EulerPacketMovingFrame.neighborStabilityConstant_ge : 1000000000 ≤ neighborStabilityConstant

theorem EulerPacketMovingFrame.controlled_neighbor_stage_references_within {σ Θ T e ε lam : ℝ} {U V P Q N : ℝ → ℝ} {R A C : ℝ → Fin 3 → Fin 3 → ℝ} (hσ : 0 < σ) (hσsmall : σ ≤ 1 / 4) (hΘ : 1 ≤ Θ) (hT0 : 0 < T) (hT : T ≤ Θ) (he : 0 ≤ e) (hε : 0 ≤ ε) (hεe : ε ≤ e) (hlam : 0 ≤ lam) (hsmall : 1000000 * neighborStabilityConstant * e * Θ ^ 40 ≤ 1) (hRc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => R t i j) (Set.Icc 0 T)) (hAc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => A t i j) (Set.Icc 0 T)) (hCc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => C t i j) (Set.Icc 0 T)) (hP : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt P (R t 0 0 * P t + R t 0 1 * Q t + R t 0 2 * N t) (Set.Icc 0 T) t) (hQ : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Q (R t 1 0 * P t + R t 1 1 * Q t + R t 1 2 * N t) (Set.Icc 0 T) t) (hN : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt N (R t 2 0 * P t + R t 2 1 * Q t + R t 2 2 * N t) (Set.Icc 0 T) t) (hU : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt U (EulerPacketRay.velocityFirstRhs (A t) (C t) ε (P t) (Q t) (N t) (U t) (V t)) (Set.Icc 0 T) t) (hV : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt V (EulerPacketRay.velocitySecondRhs (A t) (C t) ε (P t) (Q t) (N t) (U t) (V t)) (Set.Icc 0 T) t) (hRclose : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), |R t i j - EulerPacketRay.idealRayEntry (σ ^ 2) i j| ≤ 4 * e) (hAclose : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), |A t i j - EulerPacketRay.idealVelocityEntry (σ ^ 2) i j| ≤ 3 * e) (hCclose : ∀ t ∈ Set.Icc 0 T, ∀ (j : Fin 3), |C t 0 j - EulerPacketRay.idealUnprojectedEntry 0 j| ≤ 5 * e ∧ |C t 1 j - EulerPacketRay.idealUnprojectedEntry 1 j| ≤ 5 * e) (hrayInitial : EulerPacketRay.norm3 (P 0) (Q 0) (N 0 - 1) ≤ e) (hvelocityInitial : |V 0 - 1| + |U 0 + lam| ≤ e) : ∃ (F : ℝ → ℝ) (F₁ : ℝ → ℝ) (Z : ℝ → ℝ) (Z₁ : ℝ → ℝ), F 0 = 1 ∧ F₁ 0 = 0 ∧ Z 0 = 1 ∧ Z₁ 0 = lam ∧ (∀ (t : ℝ), HasDerivAt F (F₁ t) t) ∧ (∀ (t : ℝ), HasDerivAt Z (Z₁ t) t) ∧ (∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * F₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * F t) t) ∧ (∀ (t : ℝ), HasDerivAt (fun (s : ℝ) => (1 + (σ ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - σ ^ 2 * (σ ^ 2 * t ^ 2)) * Z t) t) ∧ (∀ t ∈ Set.Icc 0 T, |V t - Z t| + |U t + Z₁ t| ≤ 400000000 * e * Θ ^ 29 * (1 + lam) * F t) ∧ ∀ t ∈ Set.Icc 1 T, 0 < V t ∧ |V t / Z t - 1| ≤ neighborStabilityConstant * e * Θ ^ 29 ∧ |U t / V t + Z₁ t / Z t| ≤ 10 * (neighborStabilityConstant * e * Θ ^ 29)