The literal initialized packet and its exact residual tail are odd as actual cylinder L² paths, before and after coordinate normalization.
Joint parity of the actual terminal-history primary and its continuation. The compact terminal wave supplies the odd input without an additional assumption on the constructed solution.
theorem
EulerTransversePacketPrimary.profileParity
{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)
(O : EulerPacketProfileRecursion.Operators)
(hcorrector : O.curlCorrector = D.curlCorrector P)
(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)
(hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x)
(hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x)
(hY : (EulerCylinderFieldReflection.reflection P) ↑Y.value = -↑Y.value)
:
EulerPacketCylinderField.ProfileParity D.T
(EulerPacketProfileRecursion.primaryProfile O (vector τ hτ hτT B Y) (scalar τ hτ hτT B Y))
theorem
EulerPacketTerminalDatum.primary_profile_parity
{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)
(O : EulerPacketProfileRecursion.Operators)
(hcorrector : O.curlCorrector = D.curlCorrector period)
(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)
(hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x)
(hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x)
:
EulerPacketCylinderField.ProfileParity D.T
(EulerPacketProfileRecursion.primaryProfile O
(EulerTransversePacketPrimary.vector τ hτ hτT B (initialData D δ hδ ξ hs))
(EulerTransversePacketPrimary.scalar τ hτ hτT B (initialData D δ hδ ξ hs)))
Every initialized profile inherits reflection parity from the actual terminal wave and the prescribed source coefficient symmetries.
theorem
EulerPacketTerminalDatum.initializedProfiles_parity
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(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)
(hBH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x)
(p : ℕ)
:
EulerPacketCylinderField.ProfileParity M.T (initializedProfiles M D τ hτ hτT B δ hδ ξ hs α p)
theorem
EulerPacketTerminalDatum.initializedVelocity_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(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)
(hBH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x)
(N : ℕ)
(κ : ℝ)
:
EulerPacketCylinderField.JointOdd M.T
(EulerPacketPointJets.fieldSum (N + 1) κ
(EulerPacketProfileRecursion.assembledVelocity N (initializedProfiles M D τ hτ hτT B δ hδ ξ hs α)))
theorem
EulerPacketTerminalDatum.initializedPacketField_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(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)
(hBH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x)
(N : ℕ)
(κ : ℝ)
:
(initializedPacketField M D hTime τ hτ hτT B δ hδ ξ hs α N κ).ReflectionOdd
theorem
EulerPacketTerminalDatum.initializedNormalizedField_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(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)
(hBH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x)
(N : ℕ)
(k : ℝ)
:
(initializedNormalizedField M D hTime τ hτ hτT B δ hδ ξ hs α N k).ReflectionOdd
theorem
EulerPacketTerminalDatum.initializedResidualField_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(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)
(hBH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(κ : ℝ)
(hκ : κ ≠ 0)
:
(initializedResidualField M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN κ hκ).ReflectionOdd
theorem
EulerPacketTerminalDatum.initializedNormalizedResidualField_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 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(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)
(hBH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
:
(initializedNormalizedResidualField M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk).ReflectionOdd