The actual joined primary, restricted to its history interval, is the literal compact periodic wave times the finite-dimensional endpoint history. In particular its angular derivative at zero has the manuscript's δ⁻¹ factor.

The actual compact-terminal source history is the manuscript's pointwise stationary history multiplied by the literal cutoff and periodic wave.

noncomputable def EulerTransversePacketProvider.Data.coordinateEmbedding {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : U →L[ℝ] EulerSmoothLimit.Space

Coordinate embedding, given by referenceEmbedding D.m₀ D.R.

Equations

• D.coordinateEmbedding = EulerTransverseSourceFrame.referenceEmbedding D.m₀ D.R

noncomputable def EulerTransversePacketProvider.Data.coordinateRetraction {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : EulerSmoothLimit.Space →L[ℝ] U

Coordinate retraction, given by D.R.symm.toContinuousLinearEquiv.toContinuousLinearMap.comp (referencePlane D.m₀).orthogonalProjectionOnto.

Equations

• D.coordinateRetraction = ↑↑D.R.symm ∘SL (EulerTransverseFrameCoordinates.referencePlane D.m₀).orthogonalProjectionOnto

theorem EulerTransversePacketProvider.Data.coordinateRetraction_embedding {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (v : U) : D.coordinateRetraction (D.coordinateEmbedding v) = v

theorem EulerTransversePacketEndpoint.velocityPath_eq_history {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) (Y : EulerTransversePacketProvider.InitialData P D) (f : EulerLiftedGradientSpace.LiftDomain P → U) (hf : Continuous f) (hrep : ↑↑↑Y.value =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) : EulerCylinderSmoothOrbit.pointField P (velocityPath B Y) ⋯ t x = ((B.coefficients.labelVelocity x.1) (f x)) t

theorem EulerPacketTerminalDatum.compact_wave_history {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (B : EulerTransversePacketProvider.HistoryData D) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerCylinderSmoothOrbit.pointField period (EulerTransversePacketEndpoint.velocityPath B (initialData D δ hδ ξ hs)) ⋯ t x = scalarField δ x • ((B.coefficients.labelVelocity x.1) ξ) t

theorem EulerTransversePacketPrimary.vector_eq_history {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (Y : EulerTransversePacketProvider.InitialData P D) (f : EulerLiftedGradientSpace.LiftDomain P → U) (hf : Continuous f) (hrep : ↑↑↑Y.value =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (t : ↑(Set.Icc 0 τ)) (x : EulerSmoothLimit.Space) (θ : ℝ) : vector τ hτ hτT B Y (↑t, x, θ) = ((B.coefficients.labelVelocity x) (f (x, ↑θ))) t

theorem EulerTransversePacketPrimary.vector_compact_wave_history {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (t : ↑(Set.Icc 0 τ)) (x : EulerSmoothLimit.Space) (θ : ℝ) : vector τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ ξ hs) (↑t, x, θ) = (EulerSpatialCutoffs.innerCutoff x * EulerPeriodicProfile.profile δ θ) • ((B.coefficients.labelVelocity x) ξ) t

theorem EulerTransversePacketPrimary.angular_derivative_zero_history {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (t : ↑(Set.Icc 0 τ)) (x : EulerSmoothLimit.Space) : HasDerivAt (fun (θ : ℝ) => vector τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ ξ hs) (↑t, x, θ)) ((EulerSpatialCutoffs.innerCutoff x * δ⁻¹) • ((B.coefficients.labelVelocity x) ξ) t) 0

theorem EulerTransversePacketPrimary.angular_derivative_zero_origin {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (t : ↑(Set.Icc 0 τ)) : deriv (fun (θ : ℝ) => vector τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ ξ hs) (↑t, 0, θ)) 0 = δ⁻¹ • ((B.coefficients.labelVelocity 0) ξ) t

theorem EulerTransversePacketPrimary.angular_derivative_zero_origin_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (t : ↑(Set.Icc 0 τ)) : ‖deriv (fun (θ : ℝ) => vector τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ ξ hs) (↑t, 0, θ)) 0‖ = δ⁻¹ * ‖((B.coefficients.labelVelocity 0) ξ) t‖