The source target-compression estimate for the actual next ray.
Packet Target Compression #
theorem
EulerPacketTargetCompression.target_compression_order40
{β t Θ K e ε H P Q N : ℝ}
(hβ : 0 < β)
(hβupper : β ≤ 1)
(ht : 0 < t)
(htΘ : t ≤ Θ)
(hΘ : 1 ≤ Θ)
(hK : 1 ≤ K)
(he : 0 ≤ e)
(hε : 0 ≤ ε)
(hεe : ε ≤ e)
(hH : 0 ≤ H)
(hsmall : 1000000 * K * e * Θ ^ 40 ≤ 1)
(hscale : 1 ≤ β * t ^ 2)
(hP : |P - β * t ^ 2| ≤ 800 * e * Θ ^ 5)
(hQ : |Q + 2 * β * t| ≤ 800 * e * Θ ^ 5)
(hN : |N - 1| ≤ 800 * e * Θ ^ 5)
:
The common Θ^40 smallness regime guarantees every sign and
denominator condition used in the perturbed target compression estimate.
theorem
EulerPacketTargetCompression.full_target_compression_negative
{B E : Fin 3 → Fin 3 → ℝ}
{H ε P Q N G t : ℝ}
(ht : 0 < t)
(hD : 0 < EulerPacketRay.rayDenominator ε P Q N)
(hB : ∀ (i j : Fin 3), |B i j + E i j| ≤ G)
(hShear : H * ε * Q * P / EulerPacketRay.rayDenominator ε P Q N ≤ -(H * ε) / (10 * t))
(hdominates : 30 * G * t < H * ε)
:
EulerPacketFrameRenewal.quadraticForm3 (EulerPacketRay.parentEntry B E H) P (ε * Q) N / EulerPacketRay.rayDenominator ε P Q N < 0
The full parent matrix has strictly negative target-ray compression once its shear contribution dominates the older-gradient error.
theorem
EulerPacketMovingFrame.normalizedCompression_eq
(M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(m v r : ℝ → EulerSmoothLimit.Space)
{s₀ t₀ a ε τ : ℝ}
(hs₀ : s₀ ≠ 0)
(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)
(hD :
0 < EulerPacketRay.rayDenominator ε (scaledRay m v r s₀ t₀ a ε τ 0) (scaledRay m v r s₀ t₀ a ε τ 1)
(scaledRay m v r s₀ t₀ a ε τ 2))
:
have R := scaledRay m v r s₀ t₀ a ε τ;
normalizedCoupling M (r (physicalTime t₀ a ε τ)) (r (physicalTime t₀ a ε τ)) = EulerPacketFrameRenewal.quadraticForm3
(frameMatrix M (EulerPacketNormalizedPrimary.unit (m (physicalTime t₀ a ε τ)))
(EulerPacketNormalizedPrimary.unit (v (physicalTime t₀ a ε τ))))
(R 0) (ε * R 1) (R 2) / EulerPacketRay.rayDenominator ε (R 0) (R 1) (R 2)
theorem
EulerPacketMovingFrame.physical_parent_compression
(B M E : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(h : ℝ)
(m v r : ℝ → EulerSmoothLimit.Space)
{s₀ t₀ a ε τ : ℝ}
(hs₀ : s₀ ≠ 0)
(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)
(hD :
0 < EulerPacketRay.rayDenominator ε (scaledRay m v r s₀ t₀ a ε τ 0) (scaledRay m v r s₀ t₀ a ε τ 1)
(scaledRay m v r s₀ t₀ a ε τ 2))
(hparent :
M = B + h • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit (v (physicalTime t₀ a ε τ))))
(EulerPacketNormalizedPrimary.unit (m (physicalTime t₀ a ε τ))) + E)
:
have R := scaledRay m v r s₀ t₀ a ε τ;
normalizedCoupling M (r (physicalTime t₀ a ε τ)) (r (physicalTime t₀ a ε τ)) ≤ h * ε * R 1 * R 0 / EulerPacketRay.rayDenominator ε (R 0) (R 1) (R 2) + 3 * (‖B‖ + ‖E‖)
theorem
EulerPacketMovingFrame.physical_target_compression
(B M E : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(h : ℝ)
(m v r : ℝ → EulerSmoothLimit.Space)
{s₀ t₀ a ε τ β Θ K e : ℝ}
(hs₀ : s₀ ≠ 0)
(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)
(hparent :
M = B + h • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit (v (physicalTime t₀ a ε τ))))
(EulerPacketNormalizedPrimary.unit (m (physicalTime t₀ a ε τ))) + E)
(hβ : 0 < β)
(hβupper : β ≤ 1)
(hτ : 0 < τ)
(hτΘ : τ ≤ Θ)
(hΘ : 1 ≤ Θ)
(hK : 1 ≤ K)
(he : 0 ≤ e)
(hεe : ε ≤ e)
(hh : 0 ≤ h)
(hsmall : 1000000 * K * e * Θ ^ 40 ≤ 1)
(hscale : 1 ≤ β * τ ^ 2)
(hP : |scaledRay m v r s₀ t₀ a ε τ 0 - β * τ ^ 2| ≤ 800 * e * Θ ^ 5)
(hQ : |scaledRay m v r s₀ t₀ a ε τ 1 + 2 * β * τ| ≤ 800 * e * Θ ^ 5)
(hN : |scaledRay m v r s₀ t₀ a ε τ 2 - 1| ≤ 800 * e * Θ ^ 5)
:
normalizedCoupling M (r (physicalTime t₀ a ε τ)) (r (physicalTime t₀ a ε τ)) ≤ -(h * ε) / (10 * τ) + 3 * (‖B‖ + ‖E‖) ∧ (30 * (‖B‖ + ‖E‖) * τ < h * ε → normalizedCoupling M (r (physicalTime t₀ a ε τ)) (r (physicalTime t₀ a ε τ)) < 0)