Packet Bridge

noncomputable def EulerPacketBridge.idealVelocityFirst (β t U V : ℝ) : ℝ

The first component of the ideal normalized velocity vector field.

Equations

• EulerPacketBridge.idealVelocityFirst β t U V = -2 * V + 2 * (β * t ^ 2) * ((β * t ^ 2 + β) * V + -2 * β * t * U) / (1 + (β * t ^ 2) ^ 2)

theorem EulerPacketBridge.velocity_scalar_flux {β t u₁ v₁ : ℝ} {U V : ℝ → ℝ} (hU : HasDerivAt U u₁ t) (hV : HasDerivAt V v₁ t) : HasDerivAt V (-U t + (v₁ + U t)) t ∧ HasDerivAt (fun (s : ℝ) => (1 + (β * s ^ 2) ^ 2) * -U s) (2 * (1 - β * (β * t ^ 2)) * V t + (1 + (β * t ^ 2) ^ 2) * (-u₁ + idealVelocityFirst β t (U t) (V t))) t

The exact forced scalar flux equation obtained from the two velocity components. The forcing is the actual vector-field discrepancy.

theorem EulerPacketBridge.continuousOn_idealVelocityFirst {β : ℝ} {I : Set ℝ} {U V : ℝ → ℝ} (hU : ContinuousOn U I) (hV : ContinuousOn V I) : ContinuousOn (fun (t : ℝ) => idealVelocityFirst β t (U t) (V t)) I

theorem EulerPacketBridge.velocity_relative_error_order29 {σ Θ T e lam : ℝ} {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) (hlam : 0 ≤ lam) (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) (hU0 : U 0 = -lam) (hV0 : V 0 = 1) (hZ0 : Z 0 = 1) (hZ₁0 : Z₁ 0 = lam) (herror : ∀ t ∈ Set.Icc 0 T, |U₁ t - 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| ≤ 800 * e * Θ ^ 29 * (1 + lam) * F t

Any continuously differentiable velocity solution inherits the precise relative scalar stability estimate once its vector field has been bounded. The preceding matrix and ray theorems provide that bound.

theorem EulerPacketBridge.ray_controlled_velocity_error {β Θ 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, HasDerivAt P (R t 0 0 * P t + R t 0 1 * Q t + R t 0 2 * N t) t) (hQ : ∀ t ∈ Set.Icc 0 T, HasDerivAt Q (R t 1 0 * P t + R t 1 1 * Q t + R t 1 2 * N t) t) (hN : ∀ t ∈ Set.Icc 0 T, HasDerivAt N (R t 2 0 * P t + R t 2 1 * Q t + R t 2 2 * N 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, ∀ (i j : Fin 3), |C t i j - EulerPacketRay.idealUnprojectedEntry i j| ≤ 5 * e) (hinitial : EulerPacketRay.norm3 (P 0) (Q 0) (N 0 - 1) ≤ e) (t : ℝ) : t ∈ Set.Icc 0 T → 1 / 2 ≤ N t ∧ ∀ (U V : ℝ), |EulerPacketRay.velocityFirstRhs (A t) (C t) ε (P t) (Q t) (N t) U V - idealVelocityFirst β t U V| + |EulerPacketRay.velocitySecondRhs (A t) (C t) ε (P t) (Q t) (N t) U V + U| ≤ 200000 * e * Θ ^ 12 * (|U| + |V|)

Ray coefficient bounds imply the velocity vector-field discrepancy. The ray error and the nonvanishing third coordinate are conclusions of the actual ray ODE, not premises.

theorem EulerPacketBridge.continuousOn_velocity_rhs {ε : ℝ} {I : Set ℝ} {A C : ℝ → Fin 3 → Fin 3 → ℝ} {P Q N U V : ℝ → ℝ} (hAc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => A t i j) I) (hCc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => C t i j) I) (hP : ContinuousOn P I) (hQ : ContinuousOn Q I) (hN : ContinuousOn N I) (hU : ContinuousOn U I) (hV : ContinuousOn V I) (hNne : ∀ t ∈ I, N t ≠ 0) : ContinuousOn (fun (t : ℝ) => EulerPacketRay.velocityFirstRhs (A t) (C t) ε (P t) (Q t) (N t) (U t) (V t)) I ∧ ContinuousOn (fun (t : ℝ) => EulerPacketRay.velocitySecondRhs (A t) (C t) ε (P t) (Q t) (N t) (U t) (V t)) I

theorem EulerPacketBridge.controlled_velocity_relative_error {σ Θ 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, HasDerivAt P (R t 0 0 * P t + R t 0 1 * Q t + R t 0 2 * N t) t) (hQ : ∀ t ∈ Set.Icc 0 T, HasDerivAt Q (R t 1 0 * P t + R t 1 1 * Q t + R t 1 2 * N t) t) (hN : ∀ t ∈ Set.Icc 0 T, HasDerivAt N (R t 2 0 * P t + R t 2 1 * Q t + R t 2 2 * N t) t) (hU : ∀ t ∈ Set.Icc 0 T, HasDerivAt U (EulerPacketRay.velocityFirstRhs (A t) (C t) ε (P t) (Q t) (N t) (U t) (V t)) t) (hV : ∀ t ∈ Set.Icc 0 T, HasDerivAt V (EulerPacketRay.velocitySecondRhs (A t) (C t) ε (P t) (Q t) (N t) (U t) (V 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, ∀ (i j : Fin 3), |C t i j - EulerPacketRay.idealUnprojectedEntry i 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) (hU0 : U 0 = -lam) (hV0 : V 0 = 1) (hZ0 : Z 0 = 1) (hZ₁0 : Z₁ 0 = lam) (t : ℝ) : t ∈ Set.Icc 0 T → |V t - Z t| + |U t + Z₁ t| ≤ 160000000 * e * Θ ^ 29 * (1 + lam) * F t

The complete finite-dimensional stability bridge: actual ray and velocity equations with controlled matrix coefficients imply the relative Θ^29 error. All denominator and Duhamel bounds are derived above.