A common-radius envelope for the literal compact terminal wave.
theorem
EulerPacketTerminalDatum.initialData_word_bound
{ι : Type u_1}
[Fintype ι]
{U : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hd : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(hδ1 : δ ≤ 1)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.translate period a) ↑(initialData D δ hδ ξ hs).value)
n 0 ≤ wordCost ι q δ * ‖ξ‖ * EulerGevrey.majorant (wordRadius ι δ) 0 n
theorem
EulerPacketTerminalDatum.initialData_common_radius
{ι : Type u_1}
[Fintype ι]
{U : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hd : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(hδ1 : δ ≤ 1)
(R : ℝ)
(hR : wordRadius ι δ ≤ R)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.translate period a) ↑(initialData D δ hδ ξ hs).value)
n 0 ≤ wordCost ι q δ * ‖ξ‖ * EulerGevrey.majorant R 0 n