The quantified source frame-renewal bounds concern the actual normalized physical vectors. The third ratio is eliminated using actual tangency, and the scalar estimate is transported through the checked exact formulas.
theorem
EulerPacketMovingFrame.physical_frame_renewal_order40
(M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(m v r w : ℝ → EulerSmoothLimit.Space)
{s₀ t₀ a ε σ y Θ K e : ℝ}
{Z Z₁ : ℝ → ℝ}
(ha : a ≠ 0)
(hs₀ : 0 < s₀)
(hε : 0 < ε)
(hm : m (physicalTime t₀ a ε (y⁻¹ / σ)) ≠ 0)
(hv : v (physicalTime t₀ a ε (y⁻¹ / σ)) ≠ 0)
(hmv : inner ℝ (m (physicalTime t₀ a ε (y⁻¹ / σ))) (v (physicalTime t₀ a ε (y⁻¹ / σ))) = 0)
(hrw : inner ℝ (r (physicalTime t₀ a ε (y⁻¹ / σ))) (w (physicalTime t₀ a ε (y⁻¹ / σ))) = 0)
(hV : 0 < scaledVelocity m v w t₀ a ε (y⁻¹ / σ) 1)
(hσ : 0 < σ)
(hσsmall : σ ≤ 1 / 4)
(hy : 0 < y)
(hysmall : y ≤ 1 / 2)
(hΘ : 1 ≤ Θ)
(hK : 1 ≤ K)
(he : 0 ≤ e)
(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 : |scaledRay m v r s₀ t₀ a ε (y⁻¹ / σ) 0 - y⁻¹ ^ 2| ≤ 800 * e * Θ ^ 5)
(hQ : |scaledRay m v r s₀ t₀ a ε (y⁻¹ / σ) 1 + 2 * σ * y⁻¹| ≤ 800 * e * Θ ^ 5)
(hN : |scaledRay m v r s₀ t₀ a ε (y⁻¹ / σ) 2 - 1| ≤ 800 * e * Θ ^ 5)
(hratio :
|scaledVelocity m v w t₀ a ε (y⁻¹ / σ) 0 / scaledVelocity m v w t₀ a ε (y⁻¹ / σ) 1 + Z₁ (y⁻¹ / σ) / Z (y⁻¹ / σ)| ≤ 10 * (K * e * Θ ^ 29))
(hA :
∀ (i j : Fin 3),
|scaledAction M m v a ε (physicalTime t₀ a ε (y⁻¹ / σ)) i j - EulerPacketRay.idealVelocityEntry (σ ^ 2) i j| ≤ 3 * e)
:
|normalizedCoupling M (r (physicalTime t₀ a ε (y⁻¹ / σ))) (w (physicalTime t₀ a ε (y⁻¹ / σ))) / a - 1| ≤ y ^ 4 + σ ^ 2 * y ^ 2 + 8 * σ * y ^ 3 + 30000000 * K * e * Θ ^ 40 ∧ |y⁻¹ ^ 2 * normalizedTilt M (r (physicalTime t₀ a ε (y⁻¹ / σ))) (w (physicalTime t₀ a ε (y⁻¹ / σ))) - 1| ≤ 1500 * σ + 30000000 * K * e * Θ ^ 40