The primary size remains controlled on the short interval after target. The actual scalar ODE gives the needed uniform logarithmic growth bound; there is no separate post-target growth hypothesis.
theorem
EulerPacketMovingFrame.equation30_short_size_comparison
{σ s t : ℝ}
{Z Z₁ : ℝ → ℝ}
(hσ : 0 < σ)
(hσsmall : σ ≤ 1 / 4)
(hZ : ∀ (x : ℝ), 0 ≤ x → HasDerivAt Z (Z₁ x) x)
(hfluxZ :
∀ (x : ℝ),
0 ≤ x → HasDerivAt (fun (u : ℝ) => (1 + (σ ^ 2 * u ^ 2) ^ 2) * Z₁ u) (2 * (1 - σ ^ 2 * (σ ^ 2 * x ^ 2)) * Z x) x)
(hZ0 : Z 0 = 1)
(hZ₁0 : 0 ≤ Z₁ 0)
(hs : 1 ≤ s)
(hst : s ≤ t)
(hshort : t - s ≤ 1)
:
theorem
EulerPacketMovingFrame.equation30_horizon_size_comparison
{σ T H τ : ℝ}
{Z Z₁ : ℝ → ℝ}
(hσ : 0 < σ)
(hσsmall : σ ≤ 1 / 4)
(hZ : ∀ (x : ℝ), 0 ≤ x → HasDerivAt Z (Z₁ x) x)
(hfluxZ :
∀ (x : ℝ),
0 ≤ x → HasDerivAt (fun (u : ℝ) => (1 + (σ ^ 2 * u ^ 2) ^ 2) * Z₁ u) (2 * (1 - σ ^ 2 * (σ ^ 2 * x ^ 2)) * Z x) x)
(hZ0 : Z 0 = 1)
(hZ₁0 : 0 ≤ Z₁ 0)
(hT : 1 ≤ T)
(hshort : H - T ≤ 1)
(hτ : 0 ≤ τ)
(hτH : τ ≤ H)
:
theorem
EulerPacketMovingFrame.physical_horizon_size_bound
{α : Type u_1}
(center : α)
(m v r w : α → ℝ → EulerSmoothLimit.Space)
{s₀ t₀ a ε T H Θ K e σ : ℝ}
{Z Z₁ : ℝ → ℝ}
(hs₀ : 0 < s₀)
(hε : 0 < ε)
(hσ : 0 < σ)
(hσsmall : σ ≤ 1 / 4)
(hT : 1 ≤ T)
(hTH : T ≤ H)
(hHΘ : H ≤ Θ)
(hshort : H - T ≤ 1)
(hΘ : 1 ≤ Θ)
(hK : 1 ≤ K)
(he : 0 ≤ e)
(hεe : ε ≤ e)
(hsmall : 1000000 * K * e * Θ ^ 40 ≤ 1)
(hm : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 H, m ξ (physicalTime t₀ a ε τ) ≠ 0)
(hv : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 H, v ξ (physicalTime t₀ a ε τ) ≠ 0)
(hmv : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 H, inner ℝ (m ξ (physicalTime t₀ a ε τ)) (v ξ (physicalTime t₀ a ε τ)) = 0)
(hrw : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 H, inner ℝ (r ξ (physicalTime t₀ a ε τ)) (w ξ (physicalTime t₀ a ε τ)) = 0)
(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 : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 H, |scaledRay (m ξ) (v ξ) (r ξ) s₀ t₀ a ε τ 0 - σ ^ 2 * τ ^ 2| ≤ 800 * e * Θ ^ 5)
(hQ : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 H, |scaledRay (m ξ) (v ξ) (r ξ) s₀ t₀ a ε τ 1 - -2 * σ ^ 2 * τ| ≤ 800 * e * Θ ^ 5)
(hN : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 H, |scaledRay (m ξ) (v ξ) (r ξ) s₀ t₀ a ε τ 2 - 1| ≤ 800 * e * Θ ^ 5)
(hVrel : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 H, |scaledVelocity (m ξ) (v ξ) (w ξ) t₀ a ε τ 1 / Z τ - 1| ≤ K * e * Θ ^ 29)
(hratio :
∀ (ξ : α),
∀ τ ∈ Set.Icc 1 H,
|scaledVelocity (m ξ) (v ξ) (w ξ) t₀ a ε τ 0 / scaledVelocity (m ξ) (v ξ) (w ξ) t₀ a ε τ 1 + Z₁ τ / Z τ| ≤ 10 * (K * e * Θ ^ 29))
(ξ : α)
(τ : ℝ)
:
τ ∈ Set.Icc 1 H →
‖r ξ (physicalTime t₀ a ε τ)‖ * ‖w ξ (physicalTime t₀ a ε τ)‖ ≤ 64 * Real.exp 6 * (‖r center (physicalTime t₀ a ε T)‖ * ‖w center (physicalTime t₀ a ε T)‖)