Actual Euclidean norm estimates for the scaled moving coordinates.
theorem
EulerPacketMovingFrame.norm_le_frame_norm3
(p q x : EulerSmoothLimit.Space)
(hp : inner ℝ p p = 1)
(hq : inner ℝ q q = 1)
(hpq : inner ℝ p q = 0)
:
‖x‖ ≤ EulerPacketRay.norm3 (frameCoordinates p q x 0) (frameCoordinates p q x 1) (frameCoordinates p q x 2)
theorem
EulerPacketMovingFrame.scaledRay_norm_le_norm3
(m v r : ℝ → EulerSmoothLimit.Space)
{s₀ t₀ a ε τ : ℝ}
(hs₀ : 0 < s₀)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(hm : m (physicalTime t₀ a ε τ) ≠ 0)
(hv : v (physicalTime t₀ a ε τ) ≠ 0)
(hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0)
:
‖r (physicalTime t₀ a ε τ)‖ ≤ s₀ * EulerPacketRay.norm3 (scaledRay m v r s₀ t₀ a ε τ 0) (scaledRay m v r s₀ t₀ a ε τ 1) (scaledRay m v r s₀ t₀ a ε τ 2)
theorem
EulerPacketMovingFrame.scaledVelocity_norm_le_norm3
(m v w : ℝ → EulerSmoothLimit.Space)
{t₀ a ε τ : ℝ}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(hm : m (physicalTime t₀ a ε τ) ≠ 0)
(hv : v (physicalTime t₀ a ε τ) ≠ 0)
(hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0)
:
‖w (physicalTime t₀ a ε τ)‖ ≤ EulerPacketRay.norm3 (scaledVelocity m v w t₀ a ε τ 0) (scaledVelocity m v w t₀ a ε τ 1)
(scaledVelocity m v w t₀ a ε τ 2)
theorem
EulerPacketMovingFrame.physical_size_ge_second
(m v r w : ℝ → EulerSmoothLimit.Space)
{s₀ t₀ a ε τ : ℝ}
(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)
(hN : 1 / 2 ≤ scaledRay m v r s₀ t₀ a ε τ 2)
(hV : 0 ≤ scaledVelocity m v w t₀ a ε τ 1)
:
s₀ * scaledVelocity m v w t₀ a ε τ 1 / 2 ≤ ‖r (physicalTime t₀ a ε τ)‖ * ‖w (physicalTime t₀ a ε τ)‖
theorem
EulerPacketMovingFrame.physical_size_le_scaled_state
(m v r w : ℝ → EulerSmoothLimit.Space)
{s₀ t₀ a ε τ Θ ρ P₀ Q₀ : ℝ}
(hs₀ : 0 < s₀)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(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 ≤ Θ)
(hρ0 : 0 ≤ ρ)
(hρ : ρ ≤ 1 / 2)
(hP₀ : |P₀| ≤ Θ ^ 2)
(hQ₀ : |Q₀| ≤ 2 * Θ ^ 2)
(hP : |scaledRay m v r s₀ t₀ a ε τ 0 - P₀| ≤ ρ)
(hQ : |scaledRay m v r s₀ t₀ a ε τ 1 - Q₀| ≤ ρ)
(hN : |scaledRay m v r s₀ t₀ a ε τ 2 - 1| ≤ ρ)
:
‖r (physicalTime t₀ a ε τ)‖ * ‖w (physicalTime t₀ a ε τ)‖ ≤ 49 * s₀ * Θ ^ 4 * (|scaledVelocity m v w t₀ a ε τ 0| + |scaledVelocity m v w t₀ a ε τ 1|)