The literal zero-history initialized packet and its exact residual tail are odd as actual cylinder L² paths, before and after coordinate normalization.
theorem
EulerPacketTerminalDatum.forwardInitializedVelocity_odd
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(eM : EulerMeanPacketProvider.EvenData M)
(hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support)
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x)
(hDM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x)
(N : ℕ)
(κ : ℝ)
:
EulerPacketCylinderField.JointOdd M.T
(EulerPacketPointJets.fieldSum (N + 1) κ
(EulerPacketProfileRecursion.assembledVelocity N (forwardInitializedProfiles M D δ hδ ξ hs α)))
theorem
EulerPacketTerminalDatum.forwardInitializedPacketField_odd
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(eM : EulerMeanPacketProvider.EvenData M)
(hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support)
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x)
(hDM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x)
(N : ℕ)
(κ : ℝ)
:
(forwardInitializedPacketField M D hTime δ hδ ξ hs α N κ).ReflectionOdd
theorem
EulerPacketTerminalDatum.forwardInitializedNormalizedField_odd
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(eM : EulerMeanPacketProvider.EvenData M)
(hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support)
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x)
(hDM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x)
(N : ℕ)
(k : ℝ)
:
(forwardInitializedNormalizedField M D hTime δ hδ ξ hs α N k).ReflectionOdd
theorem
EulerPacketTerminalDatum.forwardInitializedResidualField_odd
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(eM : EulerMeanPacketProvider.EvenData M)
(hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support)
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x)
(hDM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(κ : ℝ)
(hκ : κ ≠ 0)
:
(forwardInitializedResidualField M D hTime δ hδ ξ hs α Cagree N hN κ hκ).ReflectionOdd
theorem
EulerPacketTerminalDatum.forwardInitializedNormalizedResidualField_odd
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(eM : EulerMeanPacketProvider.EvenData M)
(hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support)
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x)
(hDM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
:
(forwardInitializedNormalizedResidualField M D hTime δ hδ ξ hs α Cagree N hN k hk).ReflectionOdd