Joint parity of every profile generated by the literal source operators.
One actual mean/transverse solve preserves every joint profile symmetry.
theorem
EulerPacketCylinderField.ProfileParity.step
{P : ℝ}
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(I : EulerTransversePacketProvider.InitialData P D)
{O : EulerPacketProfileRecursion.Operators}
(C : CoefficientData P M.T O)
(hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M)
(hhigh : O.highSolve = EulerTransversePacketProvider.highSolve P D I)
(hcorrector : O.curlCorrector = D.curlCorrector P)
(E : CoefficientEven M.T O)
(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)
(hI : (EulerCylinderFieldReflection.reflection P) ↑I.value = -↑I.value)
{p : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
(hp : 2 ≤ p)
(G : (i : ℕ) → i < p → ProfileRegularity P M.T ⋯ D.support (a i))
(H : ∀ i < p, ProfileParity M.T (a i))
:
ProfileParity M.T (EulerPacketProfileRecursion.step O p a)
Every profile in the literal recursively generated family has the source parity.
theorem
EulerPacketCylinderField.profiles_parity
{P : ℝ}
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hT : M.T = D.T)
(I : EulerTransversePacketProvider.InitialData P D)
{O : EulerPacketProfileRecursion.Operators}
(C : CoefficientData P M.T O)
(hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M)
(hhigh : O.highSolve = EulerTransversePacketProvider.highSolve P D I)
(hcorrector : O.curlCorrector = D.curlCorrector P)
(E : CoefficientEven M.T O)
(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)
(hI : (EulerCylinderFieldReflection.reflection P) ↑I.value = -↑I.value)
(primary : EulerPacketProfileRecursion.Profile)
(hprimary : ProfileRegularity P M.T ⋯ D.support primary)
(hprimaryParity : ProfileParity M.T primary)
(p : ℕ)
:
ProfileParity M.T (EulerPacketProfileRecursion.profiles O primary p)
theorem
EulerPacketCylinderField.sourceCoefficientEven
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(I : EulerTransversePacketProvider.InitialData P D)
(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)
:
CoefficientEven M.T (sourceOperators P M D I)
theorem
EulerPacketCylinderField.sourceProfiles_parity
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(hT : M.T = D.T)
(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)
(hI : (EulerCylinderFieldReflection.reflection P) ↑I.value = -↑I.value)
(hIprimary : (EulerCylinderFieldReflection.reflection P) ↑Iprimary.value = -↑Iprimary.value)
(p : ℕ)
:
ProfileParity M.T (sourceProfiles P M D I Iprimary p)
theorem
EulerPacketCylinderField.sourceProfiles_time_derivatives_odd
(P : ℝ)
[Fact (0 < P)]
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(I Iprimary : EulerTransversePacketProvider.InitialData P D)
(hT : M.T = D.T)
(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)
(hI : (EulerCylinderFieldReflection.reflection P) ↑I.value = -↑I.value)
(hIprimary : (EulerCylinderFieldReflection.reflection P) ↑Iprimary.value = -↑Iprimary.value)
(p : ℕ)
: