Packet Frame Quantitative #
theorem
EulerPacketFrameQuantitative.frame_error_polynomial_bounds
{Θ K e ε P₀ : ℝ}
(hΘ : 1 ≤ Θ)
(hK : 1 ≤ K)
(he : 0 ≤ e)
(hε : 0 ≤ ε)
(hεe : ε ≤ e)
(hsmall : 1000000 * K * e * Θ ^ 40 ≤ 1)
(hP₀ : 1 ≤ P₀)
(hP₀upper : P₀ ≤ Θ ^ 2)
:
have ρ := 800 * e * Θ ^ 5;
have η := K * e * Θ ^ 29;
have dD := 6 * ρ * Θ ^ 2 + 9 * ε ^ 2 * Θ ^ 4;
have dE := 3681 * ε ^ 2 * Θ ^ 4;
have dJ := 1470 * e * Θ ^ 4 + 20 * ρ + 20 * Θ ^ 2 * η;
have dS := (1100 * ρ + 400 * η + 2520 * e * Θ ^ 2 + 500 * ε ^ 2) * Θ ^ 4;
ρ ≤ 1 / 2 ∧ η ≤ 1 / 2 ∧ 210 * e * Θ ^ 2 ≤ 1 ∧ dE ≤ 1 ∧ dJ ≤ P₀ / 4 ∧ 4 * dJ + 16 * P₀ * dD + 16 * P₀ ^ 2 * dE ≤ 30000000 * K * e * Θ ^ 40 ∧ 8 * dS + 640 * (dJ / P₀) + 640 * dE ≤ 30000000 * K * e * Θ ^ 40
Explicit polynomial control of all target-frame perturbation losses.
theorem
EulerPacketFrameQuantitative.frame_renewal_order40
{σ y Θ K e ε P Q N r : ℝ}
{A : Fin 3 → Fin 3 → ℝ}
{Z Z₁ : ℝ → ℝ}
(hσ : 0 < σ)
(hσsmall : σ ≤ 1 / 4)
(hy : 0 < y)
(hysmall : y ≤ 1 / 2)
(hΘ : 1 ≤ Θ)
(hK : 1 ≤ K)
(he : 0 ≤ e)
(hε : 0 ≤ ε)
(hεe : ε ≤ e)
(htΘ : y⁻¹ / σ ≤ Θ)
(hsmall : 1000000 * K * e * Θ ^ 40 ≤ 1)
(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)
(hP : |P - y⁻¹ ^ 2| ≤ 800 * e * Θ ^ 5)
(hQ : |Q + 2 * σ * y⁻¹| ≤ 800 * e * Θ ^ 5)
(hN : |N - 1| ≤ 800 * e * Θ ^ 5)
(hr : |r + Z₁ (y⁻¹ / σ) / Z (y⁻¹ / σ)| ≤ 10 * (K * e * Θ ^ 29))
(hA : ∀ (i j : Fin 3), |A i j - EulerPacketRay.idealVelocityEntry (σ ^ 2) i j| ≤ 3 * e)
:
have w := EulerPacketRay.velocityThird P Q N r 1;
have D := EulerPacketRay.rayDenominator ε P Q N;
have E := EulerPacketFrameStability.velocityDirectionNormSq ε r w;
have J := EulerPacketRay.velocityNumerator A P Q N r 1 w;
have S :=
EulerPacketFrameStability.frameCrossNumerator ε P Q N r w (EulerPacketFrameStability.rowAction A 0 r w)
(EulerPacketFrameStability.rowAction A 1 r w) (EulerPacketFrameStability.rowAction A 2 r w);
|J / (√D * √E) - 1| ≤ y ^ 4 + σ ^ 2 * y ^ 2 + 8 * σ * y ^ 3 + 30000000 * K * e * Θ ^ 40 ∧ |y⁻¹ ^ 2 * S / (J * √E) - 1| ≤ 1500 * σ + 30000000 * K * e * Θ ^ 40
The source's Θ^40 frame-renewal estimate, derived from coefficient,
ray, and relative state errors and the actual scalar initial value problem.