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, ↑θ)