The actual mean step and literal high-force expression preserve joint odd parity.

Literal angular averaging preserves the joint odd parity of a genuine periodic field.

theorem EulerPacketCylinderField.Field.angleMean_odd {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hodd : JointOdd T raw) : JointOdd T (EulerPacketProfileRecursion.angleMean P raw)

structure EulerPacketCylinderField.CoefficientEven (T : ℝ) (O : EulerPacketProfileRecursion.Operators) : Prop

Coefficient even data, collecting inverse, strain, normal.

• inverse (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : O.inverseFrame (↑t, -x, -θ) = O.inverseFrame (↑t, x, θ)
• strain (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : O.strain (↑t, -x, -θ) = O.strain (↑t, x, θ)
• normal (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : O.normal (↑t, -x, -θ) = O.normal (↑t, x, θ)

theorem EulerPacketCylinderField.PrefixFields.meanForce_odd {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (H : PrefixOdd T p a) (C : CoefficientData P T O) (E : CoefficientEven T O) (hp : 1 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P T (pressureGradient (a (p - 1)).highPressure)) (hpressure : JointOdd T (pressureGradient (a (p - 1)).highPressure)) : JointOdd T (EulerPacketProfileRecursion.meanForce O p a)

theorem EulerPacketCylinderField.PrefixFields.highForce_odd {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (H : PrefixOdd T p a) (C : CoefficientData P T O) (E : CoefficientEven T O) (hp : 2 ≤ p) (hT : 0 < T) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P T (pressureGradient (a (p - 1)).highPressure)) (hpressure : JointOdd T (pressureGradient (a (p - 1)).highPressure)) (hnewMean : JointOdd T (EulerPacketProfileRecursion.meanResult O p a).1) : JointOdd T (EulerPacketProfileRecursion.highForce O p a)

theorem EulerPacketCylinderField.PrefixFields.actualMean_odd {P : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (M : EulerMeanPacketProvider.Data) (F : PrefixFields P M.T p a) (H : PrefixOdd M.T p a) (C : CoefficientData P M.T O) (E : CoefficientEven M.T O) (hM : EulerMeanPacketProvider.EvenData M) (hp : 1 ≤ p) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P M.T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P M.T (pressureGradient (a (p - 1)).highPressure)) (hpressure : JointOdd M.T (pressureGradient (a (p - 1)).highPressure)) (hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M) : JointOdd M.T (EulerPacketProfileRecursion.meanResult O p a).1

theorem EulerPacketCylinderField.PrefixFields.actualHighForce_odd {P : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (M : EulerMeanPacketProvider.Data) (F : PrefixFields P M.T p a) (H : PrefixOdd M.T p a) (C : CoefficientData P M.T O) (E : CoefficientEven M.T O) (hM : EulerMeanPacketProvider.EvenData M) (hp : 2 ≤ p) {correctorT : EulerPacketProfileRecursion.VectorField} (Ct : Field P M.T correctorT) (hCt : TimeDerivative ⋯ (F.corrector (p - 1) ⋯) Ct) (pressure : Field P M.T (pressureGradient (a (p - 1)).highPressure)) (hpressure : JointOdd M.T (pressureGradient (a (p - 1)).highPressure)) (hmean : O.meanSolve = EulerMeanPacketProvider.meanSolve M) : JointOdd M.T (EulerPacketProfileRecursion.highForce O p a)