Documentation

LeanPool.NavierStokesAndEuler.Euler.CylinderScalarParity

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) (θ : ) :
classicalPrimitive P f hf hmean (-y, ↑(-θ)) = classicalPrimitive P f hf hmean (y, θ)