Packet Frame Renewal

theorem EulerPacketFrameRenewal.sqrt_unit_error {E d : ℝ} (hE : 1 ≤ E) (herror : E - 1 ≤ d) (hd : d ≤ 1) : 1 ≤ √E ∧ √E ≤ 2 ∧ |√E - 1| ≤ d

Square-root normalization preserves an error from the unit value.

theorem EulerPacketFrameRenewal.sqrt_ray_error {D D₀ d : ℝ} (hD : 1 / 4 ≤ D) (hD₀ : 1 ≤ D₀) (herror : |D - D₀| ≤ d) : 1 / 2 ≤ √D ∧ |√D - √D₀| ≤ d

The ray square root is uniformly stable away from zero.

theorem EulerPacketFrameRenewal.expansion_quotient_error {D D₀ E J J₀ dD dE dJ M aerr : ℝ} (hD : 1 / 4 ≤ D) (hD₀ : 1 ≤ D₀) (hE : 1 ≤ E) (hDE : |D - D₀| ≤ dD) (hEE : E - 1 ≤ dE) (hdE : dE ≤ 1) (hJE : |J - J₀| ≤ dJ) (hJ₀ : |J₀| ≤ M) (hroot : √D₀ ≤ M) (hideal : |J₀ / √D₀ - 1| ≤ aerr) : |J / (√D * √E) - 1| ≤ aerr + 4 * dJ + 4 * M * (2 * dD + M * dE)

Stability of the next-frame expansion coefficient under perturbation of the pressure numerator and both normalization factors.

theorem EulerPacketFrameRenewal.quotient_error_half_denominator {a a₀ b b₀ da db M : ℝ} (hb : 1 / 4 ≤ b) (hb₀ : 1 / 2 ≤ b₀) (ha : |a - a₀| ≤ da) (ha₀ : |a₀| ≤ M) (hbb : |b - b₀| ≤ db) : |a / b - a₀ / b₀| ≤ 8 * da + 16 * M * db

Quotient stability when the reference denominator is at least one half.

theorem EulerPacketFrameRenewal.coupling_quotient_error {P₀ E J J₀ S S₀ dE dJ dS berr : ℝ} (hP₀ : 0 < P₀) (hE : 1 ≤ E) (hEE : E - 1 ≤ dE) (hdE : dE ≤ 1) (hJE : |J - J₀| ≤ dJ) (hJEsmall : dJ ≤ P₀ / 4) (hJ₀ : 1 / 2 ≤ J₀ / P₀) (hJ₀upper : J₀ / P₀ ≤ 2) (hSE : |S - S₀| ≤ dS) (hS₀ : |S₀| ≤ 20) (hideal : |S₀ / (J₀ / P₀) - 1| ≤ berr) : |P₀ * S / (J * √E) - 1| ≤ berr + 8 * dS + 640 * (dJ / P₀) + 640 * dE

Stability of the next coupling multiplied by the target scale squared.

theorem EulerPacketFrameRenewal.ideal_frame_absolute_bounds {ε y z : ℝ} (hε : 0 ≤ ε) (hεsmall : ε ≤ 1 / 4) (hy : 0 ≤ y) (hysmall : y ≤ 1 / 2) (hz : 0 ≤ z) (hzupper : z ≤ 4) : EulerPacketGrowth.idealFrameDenominator ε y z ≤ 2 ∧ |EulerPacketGrowth.idealFrameNumerator ε y z| ≤ 20

Absolute bounds for the ideal inversion-coordinate frame quantities.

theorem EulerPacketFrameRenewal.target_sqrt_identity {y : ℝ} (hy : y ≠ 0) : √(1 + y⁻¹ ^ 4) = √(1 + y ^ 4) / y ^ 2

theorem EulerPacketFrameRenewal.equation30_target_ideal_quantities {ε y : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hy : 0 < y) (hysmall : y ≤ 1 / 2) (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) : have t := y⁻¹ / ε; have P₀ := ε ^ 2 * t ^ 2; have Q₀ := -2 * ε ^ 2 * t; have r₀ := -V₁ t / V t; have J₀ := P₀ + ε ^ 2 + Q₀ * r₀; have S₀ := EulerPacketFrameStability.idealCrossNumerator (ε ^ 2) P₀ Q₀ r₀; 1 ≤ P₀ ∧ 1 / 2 ≤ J₀ / P₀ ∧ J₀ / P₀ ≤ 2 ∧ |S₀| ≤ 20 ∧ |J₀ / √(1 + P₀ ^ 2) - 1| ≤ y ^ 4 + ε ^ 2 * y ^ 2 + 8 * ε * y ^ 3 ∧ |S₀ / (J₀ / P₀) - 1| ≤ 1500 * ε

Ideal frame renewal expressed directly in the original scalar solution and the target time, rather than in auxiliary Riccati variables.

theorem EulerPacketFrameRenewal.perturbed_target_compression {β t ε H P Q N ρ : ℝ} (hβ : 0 < β) (ht : 0 < t) (hε : 0 ≤ ε) (hH : 0 ≤ H) (hscale : 1 ≤ β * t ^ 2) (_hρ : 0 ≤ ρ) (hρsmall : ρ ≤ 1 / 2) (hρQ : ρ ≤ β * t) (hP : |P - β * t ^ 2| ≤ ρ) (hQ : |Q + 2 * β * t| ≤ ρ) (hN : |N - 1| ≤ ρ) (hεQ : |ε * Q| ≤ 1 / 2) : H * ε * Q * P / EulerPacketRay.rayDenominator ε P Q N ≤ -(H * ε) / (10 * t)

The perturbed target ray keeps the shear compression strictly negative with the reciprocal target-time magnitude used in equation (35).

def EulerPacketFrameRenewal.quadraticForm3 (B : Fin 3 → Fin 3 → ℝ) (p q n : ℝ) : ℝ

The coordinate quadratic form of a real three-by-three matrix.

Equations

• EulerPacketFrameRenewal.quadraticForm3 B p q n = p * (B 0 0 * p + B 0 1 * q + B 0 2 * n) + q * (B 1 0 * p + B 1 1 * q + B 1 2 * n) + n * (B 2 0 * p + B 2 1 * q + B 2 2 * n)

theorem EulerPacketFrameRenewal.quadratic_form_bound {B : Fin 3 → Fin 3 → ℝ} {G p q n : ℝ} (hB : ∀ (i j : Fin 3), |B i j| ≤ G) : |quadraticForm3 B p q n| ≤ 3 * G * (p ^ 2 + q ^ 2 + n ^ 2)

theorem EulerPacketFrameRenewal.parent_ray_compression {B E : Fin 3 → Fin 3 → ℝ} {H ε P Q N G : ℝ} (hD : 0 < EulerPacketRay.rayDenominator ε P Q N) (hB : ∀ (i j : Fin 3), |B i j + E i j| ≤ G) : quadraticForm3 (EulerPacketRay.parentEntry B E H) P (ε * Q) N / EulerPacketRay.rayDenominator ε P Q N ≤ H * ε * Q * P / EulerPacketRay.rayDenominator ε P Q N + 3 * G

The full normalized compression is the negative shear term plus a controlled contribution from the older gradient and the packet error.

noncomputable def EulerPacketFrameRenewal.idealTargetPressure (ε y : ℝ) (V V₁ : ℝ → ℝ) : ℝ

The ideal pressure-to-velocity ratio at the inverse target scale.

Equations

• EulerPacketFrameRenewal.idealTargetPressure ε y V V₁ = ε ^ 2 * (y⁻¹ / ε) ^ 2 + ε ^ 2 + -2 * ε ^ 2 * (y⁻¹ / ε) * (-V₁ (y⁻¹ / ε) / V (y⁻¹ / ε))

noncomputable def EulerPacketFrameRenewal.idealTargetCross (ε y : ℝ) (V V₁ : ℝ → ℝ) : ℝ

The ideal cross numerator at the inverse target scale.

Equations

• EulerPacketFrameRenewal.idealTargetCross ε y V V₁ = EulerPacketFrameStability.idealCrossNumerator (ε ^ 2) (ε ^ 2 * (y⁻¹ / ε) ^ 2) (-2 * ε ^ 2 * (y⁻¹ / ε)) (-V₁ (y⁻¹ / ε) / V (y⁻¹ / ε))

theorem EulerPacketFrameRenewal.equation30_target_frame_renewal {ε y D E J S dD dE dJ dS : ℝ} {V V₁ : ℝ → ℝ} (hε : 0 < ε) (hεsmall : ε ≤ 1 / 4) (hy : 0 < y) (hysmall : y ≤ 1 / 2) (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) (hD : 1 / 4 ≤ D) (hE : 1 ≤ E) (hDE : |D - (1 + y⁻¹ ^ 4)| ≤ dD) (hEE : E - 1 ≤ dE) (hdE : dE ≤ 1) (hJE : |J - idealTargetPressure ε y V V₁| ≤ dJ) (hJEsmall : dJ ≤ y⁻¹ ^ 2 / 4) (hSE : |S - idealTargetCross ε y V V₁| ≤ dS) : |J / (√D * √E) - 1| ≤ y ^ 4 + ε ^ 2 * y ^ 2 + 8 * ε * y ^ 3 + 4 * dJ + 16 * y⁻¹ ^ 2 * dD + 16 * y⁻¹ ^ 4 * dE ∧ |y⁻¹ ^ 2 * S / (J * √E) - 1| ≤ 1500 * ε + 8 * dS + 640 * (dJ / y⁻¹ ^ 2) + 640 * dE

Actual target-frame renewal, with all ideal quantities obtained from the scalar equation and all perturbation losses displayed explicitly.