The normalized scalar angular primitive converts joint odd parity to even parity.
theorem
EulerCylinderScalarPrimitive.classicalPrimitive_joint_even
(P : ℝ)
[Fact (0 < P)]
(f : EulerLiftedGradientSpace.LiftDomain P → ℝ)
(hf : Continuous f)
(hmean : ∀ (y : EulerLiftedGradientSpace.Vector3), ∫ (s : ℝ) in 0..P, f (y, ↑s) = 0)
(hodd : ∀ (y : EulerLiftedGradientSpace.Vector3) (θ : ℝ), f (-y, ↑(-θ)) = -f (y, ↑θ))
(y : EulerSmoothLimit.Space)
(θ : ℝ)
: