The manuscript's literal compact wave is an admissible terminal coordinate field.

The literal terminal datum belongs to the actual supported, mean-zero cylinder space.

theorem EulerPacketTerminalDatum.terminal_map {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] (δ : ℝ) (hδ : 0 < δ) (ξ : U) (L : U →L[ℝ] V) : terminal δ hδ (L ξ) = (EulerCylinderConstantMap.map period L) (terminal δ hδ ξ)

theorem EulerPacketTerminalDatum.terminal_average_zero {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] [CompleteSpace U] (δ : ℝ) (hδ : 0 < δ) (ξ : U) : (EulerCylinderAngleAverage.average period) (terminal δ hδ ξ) = 0

theorem EulerPacketTerminalDatum.terminal_supported {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (δ : ℝ) (hδ : 0 < δ) (ξ : U) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ S) : terminal δ hδ ξ ∈ EulerLpCylinderPaths.Supported period U S hS

theorem EulerPacketTerminalDatum.terminal_reflection {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (hδ : 0 < δ) (ξ : U) : (EulerCylinderFieldReflection.reflection period) (terminal δ hδ ξ) = -terminal δ hδ ξ

noncomputable def EulerPacketTerminalDatum.initialData {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) : EulerTransversePacketProvider.InitialData period D

Initial data, bundling value, orbit, mean_zero.

Equations

• EulerPacketTerminalDatum.initialData D δ hδ ξ hs = { value := ⟨EulerPacketTerminalDatum.terminal δ hδ ξ, ⋯⟩, orbit := ⋯, mean_zero := ⋯ }

theorem EulerPacketTerminalDatum.initialData_value {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) : ↑(initialData D δ hδ ξ hs).value = terminal δ hδ ξ

theorem EulerPacketTerminalDatum.initialData_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) {ι : Type u_2} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (hδ1 : δ ≤ 1) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period b) ↑(initialData D δ hδ ξ hs).value) n 0 ≤ EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q (jetRadius δ) (scalarJetCost δ * ‖ξ‖ * terminalMass) * EulerGevrey.majorant (wordRadius ι δ) 0 n