Joint parity carried by the actual profile fields and their true time derivatives.

structure EulerPacketCylinderField.ProfileParity (T : ℝ) (a : EulerPacketProfileRecursion.Profile) : Prop

Profile parity data, collecting high, mean, corrector, pressure, highPressure, meanPressure.

• high : JointOdd T a.high
• mean : JointOdd T a.mean
• corrector : JointOdd T a.corrector
• pressure : JointOdd T (pressureGradient a.highPressure)
• highPressure (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : a.highPressure (↑t, -x, -θ) = a.highPressure (↑t, x, θ)
• meanPressure (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : a.meanPressure (↑t, -x, -θ) = a.meanPressure (↑t, x, θ)

theorem EulerPacketCylinderField.ProfileParity.zero (T : ℝ) : ProfileParity T 0

theorem EulerPacketCylinderField.ProfileParity.prefixOdd {T : ℝ} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (H : ∀ i < p, ProfileParity T (a i)) : PrefixOdd T p a

theorem EulerPacketCylinderField.ProfileParity.changeTime {T T' : ℝ} {a : EulerPacketProfileRecursion.Profile} (H : ProfileParity T a) (h : T = T') : ProfileParity T' a

theorem EulerPacketCylinderField.ProfileParity.highDerivative_odd {P T : ℝ} [Fact (0 < P)] {S : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} (hT : 0 < T) (G : ProfileRegularity P T ⋯ S a) (H : ProfileParity T a) : JointOdd T G.highT

theorem EulerPacketCylinderField.ProfileParity.meanDerivative_odd {P T : ℝ} [Fact (0 < P)] {S : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} (hT : 0 < T) (G : ProfileRegularity P T ⋯ S a) (H : ProfileParity T a) : JointOdd T G.meanT

theorem EulerPacketCylinderField.ProfileParity.correctorDerivative_odd {P T : ℝ} [Fact (0 < P)] {S : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} (hT : 0 < T) (G : ProfileRegularity P T ⋯ S a) (H : ProfileParity T a) : JointOdd T G.correctorT

theorem EulerPacketCylinderField.JointOdd.changeTime {T T' : ℝ} {raw : EulerPacketProfileRecursion.VectorField} (H : JointOdd T raw) (h : T = T') : JointOdd T' raw