The before-target part of the physical primary-size estimate. The input is the actual ray and velocity error already obtained from the physical equations, and the comparison function solves the scalar reference ODE.
Uniform comparison between actual and ideal physical primary sizes.
theorem
EulerPacketMovingFrame.physical_size_comparison_order40
(m v r w : ℝ → EulerSmoothLimit.Space)
{s₀ t₀ a ε τ Θ K e P₀ Q₀ r₀ Z : ℝ}
(hs₀ : 0 < s₀)
(hε : 0 < ε)
(hm : m (physicalTime t₀ a ε τ) ≠ 0)
(hv : v (physicalTime t₀ a ε τ) ≠ 0)
(hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0)
(hrw : inner ℝ (r (physicalTime t₀ a ε τ)) (w (physicalTime t₀ a ε τ)) = 0)
(hΘ : 1 ≤ Θ)
(hK : 1 ≤ K)
(he : 0 ≤ e)
(hεe : ε ≤ e)
(hsmall : 1000000 * K * e * Θ ^ 40 ≤ 1)
(hP₀ : |P₀| ≤ Θ ^ 2)
(hQ₀ : |Q₀| ≤ 2 * Θ ^ 2)
(hr₀ : |r₀| ≤ 4)
(hZ : 0 < Z)
(hP : |scaledRay m v r s₀ t₀ a ε τ 0 - P₀| ≤ 800 * e * Θ ^ 5)
(hQ : |scaledRay m v r s₀ t₀ a ε τ 1 - Q₀| ≤ 800 * e * Θ ^ 5)
(hN : |scaledRay m v r s₀ t₀ a ε τ 2 - 1| ≤ 800 * e * Θ ^ 5)
(hVrel : |scaledVelocity m v w t₀ a ε τ 1 / Z - 1| ≤ K * e * Θ ^ 29)
(hratio : |scaledVelocity m v w t₀ a ε τ 0 / scaledVelocity m v w t₀ a ε τ 1 - r₀| ≤ 10 * (K * e * Θ ^ 29))
:
The actual primary size lies between fixed multiples of its ideal size under the same quantitative ray and relative-state estimates already proved for propagation.
theorem
EulerPacketMovingFrame.physical_ideal_size_comparison_order40
(m v r w : ℝ → EulerSmoothLimit.Space)
{s₀ t₀ a ε τ Θ K e σ : ℝ}
{Z Z₁ : ℝ → ℝ}
(hs₀ : 0 < s₀)
(hε : 0 < ε)
(hσ : 0 < σ)
(hσsmall : σ ≤ 1 / 4)
(hm : m (physicalTime t₀ a ε τ) ≠ 0)
(hv : v (physicalTime t₀ a ε τ) ≠ 0)
(hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0)
(hrw : inner ℝ (r (physicalTime t₀ a ε τ)) (w (physicalTime t₀ a ε τ)) = 0)
(hΘ : 1 ≤ Θ)
(hK : 1 ≤ K)
(he : 0 ≤ e)
(hεe : ε ≤ e)
(hsmall : 1000000 * K * e * Θ ^ 40 ≤ 1)
(hτ : 1 ≤ τ)
(hτΘ : τ ≤ Θ)
(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 ε τ 0 - σ ^ 2 * τ ^ 2| ≤ 800 * e * Θ ^ 5)
(hQ : |scaledRay m v r s₀ t₀ a ε τ 1 - -2 * σ ^ 2 * τ| ≤ 800 * e * Θ ^ 5)
(hN : |scaledRay m v r s₀ t₀ a ε τ 2 - 1| ≤ 800 * e * Θ ^ 5)
(hVrel : |scaledVelocity m v w t₀ a ε τ 1 / Z τ - 1| ≤ K * e * Θ ^ 29)
(hratio : |scaledVelocity m v w t₀ a ε τ 0 / scaledVelocity m v w t₀ a ε τ 1 + Z₁ τ / Z τ| ≤ 10 * (K * e * Θ ^ 29))
:
s₀ * idealPrimarySize σ Z τ / 4 ≤ ‖r (physicalTime t₀ a ε τ)‖ * ‖w (physicalTime t₀ a ε τ)‖ ∧ ‖r (physicalTime t₀ a ε τ)‖ * ‖w (physicalTime t₀ a ε τ)‖ ≤ 8 * s₀ * idealPrimarySize σ Z τ
theorem
EulerPacketMovingFrame.physical_before_target_size_bound
{α : Type u_1}
(center : α)
(m v r w : α → ℝ → EulerSmoothLimit.Space)
{s₀ t₀ a ε T Θ K e σ : ℝ}
{Z Z₁ : ℝ → ℝ}
(hs₀ : 0 < s₀)
(hε : 0 < ε)
(hσ : 0 < σ)
(hσsmall : σ ≤ 1 / 4)
(hT : 1 ≤ T)
(hTΘ : T ≤ Θ)
(hΘ : 1 ≤ Θ)
(hK : 1 ≤ K)
(he : 0 ≤ e)
(hεe : ε ≤ e)
(hsmall : 1000000 * K * e * Θ ^ 40 ≤ 1)
(hm : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 T, m ξ (physicalTime t₀ a ε τ) ≠ 0)
(hv : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 T, v ξ (physicalTime t₀ a ε τ) ≠ 0)
(hmv : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 T, inner ℝ (m ξ (physicalTime t₀ a ε τ)) (v ξ (physicalTime t₀ a ε τ)) = 0)
(hrw : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 T, 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 T, |scaledRay (m ξ) (v ξ) (r ξ) s₀ t₀ a ε τ 0 - σ ^ 2 * τ ^ 2| ≤ 800 * e * Θ ^ 5)
(hQ : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 T, |scaledRay (m ξ) (v ξ) (r ξ) s₀ t₀ a ε τ 1 - -2 * σ ^ 2 * τ| ≤ 800 * e * Θ ^ 5)
(hN : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 T, |scaledRay (m ξ) (v ξ) (r ξ) s₀ t₀ a ε τ 2 - 1| ≤ 800 * e * Θ ^ 5)
(hVrel : ∀ (ξ : α), ∀ τ ∈ Set.Icc 1 T, |scaledVelocity (m ξ) (v ξ) (w ξ) t₀ a ε τ 1 / Z τ - 1| ≤ K * e * Θ ^ 29)
(hratio :
∀ (ξ : α),
∀ τ ∈ Set.Icc 1 T,
|scaledVelocity (m ξ) (v ξ) (w ξ) t₀ a ε τ 0 / scaledVelocity (m ξ) (v ξ) (w ξ) t₀ a ε τ 1 + Z₁ τ / Z τ| ≤ 10 * (K * e * Θ ^ 29))
(ξ : α)
(τ : ℝ)
:
τ ∈ Set.Icc 1 T →
‖r ξ (physicalTime t₀ a ε τ)‖ * ‖w ξ (physicalTime t₀ a ε τ)‖ ≤ 64 * (‖r center (physicalTime t₀ a ε T)‖ * ‖w center (physicalTime t₀ a ε T)‖)
Every controlled neighboring primary before target is bounded by a fixed multiple of the center's actual target size. All comparisons use the same genuine scalar ODE solution, including its initial slope.