Packet Frame Stability

theorem EulerPacketFrameStability.inverted_logarithmic_identity {ε y : ℝ} {V V₁ : ℝ → ℝ} (hε : ε ≠ 0) (hy : y ≠ 0) (hV : V (y⁻¹ / ε) ≠ 0) : y ^ 2 * (-ε * EulerPacketGrowth.invertedScalarDeriv ε V V₁ y / EulerPacketGrowth.invertedScalar ε V y) - ε * y = V₁ (y⁻¹ / ε) / V (y⁻¹ / ε)

Exact relation between the original and inverted logarithmic slopes.

theorem EulerPacketFrameStability.equation30_primary_logderivative_bound {ε : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hflux : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) (t : ℝ) : 1 ≤ t → |V₁ t / V t| ≤ 4

The logarithmic slope is bounded uniformly in the initial nonnegative slope after time one.

theorem EulerPacketFrameStability.equation30_ideal_numerator_positive {ε : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hV : ∀ (t : ℝ), 0 ≤ t → HasDerivAt V (V₁ t) t) (hflux : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * V₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * V t) t) (hV0 : V 0 = 1) (hV₁0 : 0 ≤ V₁ 0) (t : ℝ) : 0 ≤ t → ε ^ 2 * V t ≤ (ε ^ 2 * t ^ 2 + ε ^ 2) * V t + 2 * ε ^ 2 * t * V₁ t

The ideal pressure numerator has the sign required for the next-frame construction, throughout the forward evolution.

theorem EulerPacketFrameStability.relative_state_error_consequences {U V Z Z₁ η : ℝ} (hZ : 0 < Z) (hη : 0 ≤ η) (hηsmall : η ≤ 1 / 2) (herror : |V - Z| + |U + Z₁| ≤ η * Z) (hslope : |Z₁ / Z| ≤ 4) : 0 < V ∧ |V / Z - 1| ≤ η ∧ |U / V + Z₁ / Z| ≤ 10 * η

Relative control of both components gives positivity and control of the logarithmic ratio without dividing by an uncontrolled quantity.

theorem EulerPacketFrameStability.equation30_relative_state_consequences {ε lam δ t U V : ℝ} {F F₁ Z Z₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hlam : 0 ≤ lam) (ht : 1 ≤ t) (hδ : 0 ≤ δ) (hsmall : 4 * Real.exp 6 * δ ≤ 1) (hF : ∀ (t : ℝ), 0 ≤ t → HasDerivAt F (F₁ t) t) (hZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt Z (Z₁ 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) (hfluxZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * Z t) t) (hF0 : F 0 = 1) (hF₁0 : F₁ 0 = 0) (hZ0 : Z 0 = 1) (hZ₁0 : Z₁ 0 = lam) (herror : |V - Z t| + |U + Z₁ t| ≤ δ * (1 + lam) * F t) : 0 < V ∧ |V / Z t - 1| ≤ 2 * Real.exp 6 * δ ∧ |U / V + Z₁ t / Z t| ≤ 20 * Real.exp 6 * δ

Stability relative to the growing primary solution, with constants independent of its nonnegative initial slope.

theorem EulerPacketFrameStability.pressure_ratio_error {Θ η j P₀ Q₀ β U V r₀ J : ℝ} (hΘ : 1 ≤ Θ) (_hη : 0 ≤ η) (hηsmall : η ≤ 1 / 2) (hj : 0 ≤ j) (hV : 0 < V) (hQ₀ : |Q₀| ≤ 2 * Θ ^ 2) (hr₀ : |r₀| ≤ 4) (hr : |U / V - r₀| ≤ 10 * η) (hJ : |J - ((P₀ + β) * V + Q₀ * U)| ≤ j * (|U| + |V|)) : |J / V - (P₀ + β + Q₀ * r₀)| ≤ 10 * j + 20 * Θ ^ 2 * η

Division of the pressure-numerator error is safe once positivity and the logarithmic-ratio bounds have been derived.

theorem EulerPacketFrameStability.equation30_pressure_sign_stable {ε Θ t η j U V J : ℝ} {Z Z₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hΘ : 1 ≤ Θ) (ht : 1 ≤ t) (htΘ : t ≤ Θ) (hη : 0 ≤ η) (hηsmall : η ≤ 1 / 2) (hj : 0 ≤ j) (hsmall : 10 * j + 20 * Θ ^ 2 * η ≤ ε ^ 2 / 2) (hZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt Z (Z₁ t) t) (hfluxZ : ∀ (t : ℝ), 0 ≤ t → HasDerivAt (fun (s : ℝ) => (1 + (ε ^ 2 * s ^ 2) ^ 2) * Z₁ s) (2 * (1 - ε ^ 2 * (ε ^ 2 * t ^ 2)) * Z t) t) (hZ0 : Z 0 = 1) (hZ₁0 : 0 ≤ Z₁ 0) (herror : |V - Z t| + |U + Z₁ t| ≤ η * Z t) (hJ : |J - ((ε ^ 2 * t ^ 2 + ε ^ 2) * V + -2 * ε ^ 2 * t * U)| ≤ j * (|U| + |V|)) : 0 < V ∧ ε ^ 2 / 2 ≤ J / V ∧ 0 < J

The actual pressure numerator preserves the required positive sign under the quantitatively derived relative state error.

theorem EulerPacketFrameStability.third_ratio_error {Θ ρ η P Q N P₀ Q₀ r r₀ : ℝ} (hΘ : 1 ≤ Θ) (hρ : 0 ≤ ρ) (hρsmall : ρ ≤ 1 / 2) (hη : 0 ≤ η) (hηsmall : η ≤ 1 / 2) (hP₀ : |P₀| ≤ Θ ^ 2) (hQ₀ : |Q₀| ≤ 2 * Θ ^ 2) (hP : |P - P₀| ≤ ρ) (hQ : |Q - Q₀| ≤ ρ) (hN : |N - 1| ≤ ρ) (hr₀ : |r₀| ≤ 4) (hr : |r - r₀| ≤ 10 * η) : |r| ≤ 9 ∧ |(-(P₀ * r₀ + Q₀))| ≤ 6 * Θ ^ 2 ∧ |EulerPacketRay.velocityThird P Q N r 1| ≤ 60 * Θ ^ 2 ∧ |EulerPacketRay.velocityThird P Q N r 1 - -(P₀ * r₀ + Q₀)| ≤ (32 * ρ + 20 * η) * Θ ^ 2

The third normalized velocity ratio follows from orthogonality and the already controlled ray and first velocity ratio.

def EulerPacketFrameStability.rowAction (A : Fin 3 → Fin 3 → ℝ) (i : Fin 3) (r w : ℝ) : ℝ

A normalized parent-gradient row applied to the velocity ratios.

Equations

• EulerPacketFrameStability.rowAction A i r w = A i 0 * r + A i 1 + A i 2 * w

theorem EulerPacketFrameStability.normalized_action_error {Θ e β r w : ℝ} {A : Fin 3 → Fin 3 → ℝ} (hΘ : 1 ≤ Θ) (he : 0 ≤ e) (hr : |r| ≤ 9) (hw : |w| ≤ 60 * Θ ^ 2) (hA : ∀ (i j : Fin 3), |A i j - EulerPacketRay.idealVelocityEntry β i j| ≤ e) : |rowAction A 0 r w - 1| ≤ 70 * e * Θ ^ 2 ∧ |rowAction A 1 r w - r| ≤ 70 * e * Θ ^ 2 ∧ |rowAction A 2 r w - β| ≤ 70 * e * Θ ^ 2

Rowwise control of the normalized parent action on the new velocity.

def EulerPacketFrameStability.frameCrossNumerator (ε P Q N r w Tp Tq Tn : ℝ) : ℝ

The cross-product numerator for the next normalized coupling. The middle argument Tq denotes ε times the physical middle component.

Equations

• EulerPacketFrameStability.frameCrossNumerator ε P Q N r w Tp Tq Tn = (-N + ε ^ 2 * Q * w) * Tp + (N * r - P * w) * Tq + (P - ε ^ 2 * Q * r) * Tn

def EulerPacketFrameStability.idealCrossNumerator (β P Q r : ℝ) : ℝ

The ideal next-frame cross numerator in original scalar coordinates.

Equations

• EulerPacketFrameStability.idealCrossNumerator β P Q r = -1 + β * P + (1 + P ^ 2) * r ^ 2 + P * Q * r

theorem EulerPacketFrameStability.frame_cross_numerator_error {Θ ρ η σ ε β P Q N P₀ Q₀ r r₀ w Tp Tq Tn : ℝ} (hΘ : 1 ≤ Θ) (hρ : 0 ≤ ρ) (hη : 0 ≤ η) (hσ : 0 ≤ σ) (hP₀ : |P₀| ≤ Θ ^ 2) (hP : |P - P₀| ≤ ρ) (hQ : |Q| ≤ 3 * Θ ^ 2) (hN : |N - 1| ≤ ρ) (hr₀ : |r₀| ≤ 4) (hrabs : |r| ≤ 9) (hr : |r - r₀| ≤ 10 * η) (hwabs : |w| ≤ 60 * Θ ^ 2) (hw₀ : |(-(P₀ * r₀ + Q₀))| ≤ 6 * Θ ^ 2) (hw : |w - -(P₀ * r₀ + Q₀)| ≤ (32 * ρ + 20 * η) * Θ ^ 2) (hTp : |Tp - 1| ≤ σ) (hTq : |Tq - r₀| ≤ σ + 10 * η) (hTn : |Tn - β| ≤ σ) (hTpabs : |Tp| ≤ 2) (hTqabs : |Tq| ≤ 10) (hTnabs : |Tn| ≤ 2) : |frameCrossNumerator ε P Q N r w Tp Tq Tn - idealCrossNumerator β P₀ Q₀ r₀| ≤ (1100 * ρ + 400 * η + 12 * σ + 500 * ε ^ 2) * Θ ^ 4

Quantitative stability of the exact cross-product numerator.

theorem EulerPacketFrameStability.frame_cross_error_from_matrix {Θ ρ η e ε β P Q N P₀ Q₀ r r₀ : ℝ} {A : Fin 3 → Fin 3 → ℝ} (hΘ : 1 ≤ Θ) (hρ : 0 ≤ ρ) (hρsmall : ρ ≤ 1 / 2) (hη : 0 ≤ η) (hηsmall : η ≤ 1 / 2) (he : 0 ≤ e) (hsmall : 70 * e * Θ ^ 2 ≤ 1) (hβ : |β| ≤ 1) (hP₀ : |P₀| ≤ Θ ^ 2) (hQ₀ : |Q₀| ≤ 2 * Θ ^ 2) (hP : |P - P₀| ≤ ρ) (hQ : |Q - Q₀| ≤ ρ) (hN : |N - 1| ≤ ρ) (hr₀ : |r₀| ≤ 4) (hr : |r - r₀| ≤ 10 * η) (hA : ∀ (i j : Fin 3), |A i j - EulerPacketRay.idealVelocityEntry β i j| ≤ e) : have w := EulerPacketRay.velocityThird P Q N r 1; |frameCrossNumerator ε P Q N r w (rowAction A 0 r w) (rowAction A 1 r w) (rowAction A 2 r w) - idealCrossNumerator β P₀ Q₀ r₀| ≤ (1100 * ρ + 400 * η + 840 * e * Θ ^ 2 + 500 * ε ^ 2) * Θ ^ 4

The cross numerator bound with every velocity-ratio and parent-action estimate derived from ray, state, and matrix coefficient errors.

def EulerPacketFrameStability.velocityDirectionNormSq (ε r w : ℝ) : ℝ

Squared norm of the normalized velocity direction.

Equations

• EulerPacketFrameStability.velocityDirectionNormSq ε r w = 1 + ε ^ 2 * (r ^ 2 + w ^ 2)

theorem EulerPacketFrameStability.velocity_direction_norm_bound {Θ ε r w : ℝ} (hΘ : 1 ≤ Θ) (hr : |r| ≤ 9) (hw : |w| ≤ 60 * Θ ^ 2) : 1 ≤ velocityDirectionNormSq ε r w ∧ velocityDirectionNormSq ε r w - 1 ≤ 3681 * ε ^ 2 * Θ ^ 4