Related estimates used together by the same construction modules.
The actual scaled velocity supplies the first two equations and the scalar flux equation used in amplification. Only the first two transport rows are relevant; the auxiliary third row in the scalar estimate is filled explicitly.
theorem
EulerPacketMovingFrame.velocityFirstRhs_firstTwoRows
(A C : Fin 3 → Fin 3 → ℝ)
(ε P Q N U V : ℝ)
:
EulerPacketRay.velocityFirstRhs A (firstTwoRows C) ε P Q N U V = EulerPacketRay.velocityFirstRhs A C ε P Q N U V
theorem
EulerPacketMovingFrame.velocitySecondRhs_firstTwoRows
(A C : Fin 3 → Fin 3 → ℝ)
(ε P Q N U V : ℝ)
:
EulerPacketRay.velocitySecondRhs A (firstTwoRows C) ε P Q N U V = EulerPacketRay.velocitySecondRhs A C ε P Q N U V
theorem
EulerPacketMovingFrame.velocity_rhs_error_firstTwo
{A C : Fin 3 → Fin 3 → ℝ}
{Θ e ε β P Q N P₀ Q₀ U V : ℝ}
(hΘ : 1 ≤ Θ)
(he : 0 ≤ e)
(hε : 0 ≤ ε)
(hεe : ε ≤ e)
(hsmall : 10000 * e * Θ ^ 5 ≤ 1)
(hβ : |β| ≤ 1)
(hA : ∀ (i j : Fin 3), |A i j - EulerPacketRay.idealVelocityEntry β i j| ≤ 3 * e)
(hC :
∀ (j : Fin 3),
|C 0 j - EulerPacketRay.idealUnprojectedEntry 0 j| ≤ 5 * e ∧ |C 1 j - EulerPacketRay.idealUnprojectedEntry 1 j| ≤ 5 * e)
(hP₀ : |P₀| ≤ Θ ^ 2)
(hQ₀ : |Q₀| ≤ 2 * Θ ^ 2)
(hP : |P - P₀| ≤ 800 * e * Θ ^ 5)
(hQ : |Q - Q₀| ≤ 800 * e * Θ ^ 5)
(hN : |N - 1| ≤ 800 * e * Θ ^ 5)
:
The scalar error estimate needs no assumption on the physical third transport row.
theorem
EulerPacketMovingFrame.scaledVelocity_firstTwo_hasDerivWithinAt
(B M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
{m v r w : ℝ → EulerSmoothLimit.Space}
{s₀ t₀ a ε τ : ℝ}
{S U : Set ℝ}
(ha : a ≠ 0)
(hε : ε ≠ 0)
(hs₀ : s₀ ≠ 0)
(hmap : Set.MapsTo (physicalTime t₀ a ε) U S)
(hm : HasDerivWithinAt m (-(ContinuousLinearMap.adjoint B) (m (physicalTime t₀ a ε τ))) S (physicalTime t₀ a ε τ))
(hv :
HasDerivWithinAt v
(-B (v (physicalTime t₀ a ε τ)) + (2 * inner ℝ (m (physicalTime t₀ a ε τ)) (B (v (physicalTime t₀ a ε τ))) / ‖m (physicalTime t₀ a ε τ)‖ ^ 2) • m (physicalTime t₀ a ε τ))
S (physicalTime t₀ a ε τ))
(hw :
HasDerivWithinAt w
(-M (w (physicalTime t₀ a ε τ)) + (2 * inner ℝ (r (physicalTime t₀ a ε τ)) (M (w (physicalTime t₀ a ε τ))) / ‖r (physicalTime t₀ a ε τ)‖ ^ 2) • r (physicalTime t₀ a ε τ))
S (physicalTime t₀ a ε τ))
(hm0 : m (physicalTime t₀ a ε τ) ≠ 0)
(hv0 : v (physicalTime t₀ a ε τ) ≠ 0)
(hmv : inner ℝ (m (physicalTime t₀ a ε τ)) (v (physicalTime t₀ a ε τ)) = 0)
(hr0 : r (physicalTime t₀ a ε τ) ≠ 0)
(hrw : inner ℝ (r (physicalTime t₀ a ε τ)) (w (physicalTime t₀ a ε τ)) = 0)
(hN : scaledRay m v r s₀ t₀ a ε τ 2 ≠ 0)
:
have R := scaledRay m v r s₀ t₀ a ε τ;
have V := scaledVelocity m v w t₀ a ε τ;
have A := scaledAction M m v a ε (physicalTime t₀ a ε τ);
have C := scaledTransport B M m v a ε (physicalTime t₀ a ε τ);
HasDerivWithinAt (fun (σ : ℝ) => scaledVelocity m v w t₀ a ε σ 0)
(EulerPacketRay.velocityFirstRhs A C ε (R 0) (R 1) (R 2) (V 0) (V 1)) U τ ∧ HasDerivWithinAt (fun (σ : ℝ) => scaledVelocity m v w t₀ a ε σ 1)
(EulerPacketRay.velocitySecondRhs A C ε (R 0) (R 1) (R 2) (V 0) (V 1)) U τ
The actual tangency constraint removes the third scaled coordinate.
theorem
EulerPacketMovingFrame.velocity_scalar_flux_within
{β t u₁ v₁ : ℝ}
{U V : ℝ → ℝ}
{S : Set ℝ}
(hU : HasDerivWithinAt U u₁ S t)
(hV : HasDerivWithinAt V v₁ S t)
:
The flux identity is valid with the actual one-sided endpoint derivatives of packet paths, as well as in the interior.
Ray control for the genuine within-interval packet equations.
theorem
EulerPacketMovingFrame.ray_closeness_within
{β Θ T e : ℝ}
{A : ℝ → Fin 3 → Fin 3 → ℝ}
{P Q N : ℝ → ℝ}
(hβ : 0 ≤ β)
(hβupper : β ≤ 1)
(hΘ : 1 ≤ Θ)
(hT0 : 0 < T)
(hT : T ≤ Θ)
(he : 0 ≤ e)
(hsmall : 400 * e * Θ ^ 5 ≤ 1)
(hAc : ∀ (i j : Fin 3), ContinuousOn (fun (t : ℝ) => A t i j) (Set.Icc 0 T))
(hP : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt P (A t 0 0 * P t + A t 0 1 * Q t + A t 0 2 * N t) (Set.Icc 0 T) t)
(hQ : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt Q (A t 1 0 * P t + A t 1 1 * Q t + A t 1 2 * N t) (Set.Icc 0 T) t)
(hN : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt N (A t 2 0 * P t + A t 2 1 * Q t + A t 2 2 * N t) (Set.Icc 0 T) t)
(hclose : ∀ t ∈ Set.Icc 0 T, ∀ (i j : Fin 3), |A t i j - EulerPacketRay.idealRayEntry β i j| ≤ e)
(hinitial : EulerPacketRay.norm3 (P 0) (Q 0) (N 0 - 1) ≤ e)
(t : ℝ)
: