Spatial support and joint parity of the literal pressure-gradient term.

theorem EulerPacketCylinderField.pressureGradient_eq_spatialDual (p : EulerPacketProfileRecursion.ScalarField) (z : EulerPacketPointJets.Domain) : pressureGradient p z = (InnerProductSpace.toDual ℝ EulerSmoothLimit.Space).symm (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p (z.1, y)) z.2 ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ)

theorem EulerPacketCylinderField.pressureGradient_zero_outside (p : EulerPacketProfileRecursion.ScalarField) (t : ℝ) (S : Set EulerSmoothLimit.Space) (hS : IsClosed S) (hp : ∀ x ∉ S, ∀ (θ : ℝ), p (t, x, θ) = 0) (x : EulerSmoothLimit.Space) (hx : x ∉ S) (θ : ℝ) : pressureGradient p (t, x, θ) = 0

theorem EulerPacketCylinderField.pressureGradient_odd (p : EulerPacketProfileRecursion.ScalarField) (t : ℝ) (hp : ContDiff ℝ ↑⊤ fun (y : EulerLiftedGradientSpace.LiftTangent) => p (t, y)) (heven : ∀ (x : EulerSmoothLimit.Space) (θ : ℝ), p (t, -x, -θ) = p (t, x, θ)) (x : EulerSmoothLimit.Space) (θ : ℝ) : pressureGradient p (t, -x, -θ) = -pressureGradient p (t, x, θ)