Odd velocity and even normalized pressure for the actual mean provider.

theorem EulerMeanPacketProvider.representative_odd_of_reflection (u : ↥EulerMeanSolenoidal.L2) (hs : EulerMeanSmoothRepresentative.SmoothOrbit u) (hu : EulerMeanSolenoidal.reflection u = -u) (x : EulerSmoothLimit.Space) : EulerMeanSmoothRepresentative.representative u hs (-x) = -EulerMeanSmoothRepresentative.representative u hs x

Oddness of an actual L² class transfers to its unique smooth representative.

theorem EulerMeanPacketProvider.Forcing.velocityPath_reflection {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (hD : EvenData D) (hodd : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), raw (↑t, -x, 0) = -raw (↑t, x, 0)) (t : ↑(Set.Icc 0 D.T)) : EulerMeanSolenoidal.reflection (G.velocityPath t) = -G.velocityPath t

theorem EulerMeanPacketProvider.Forcing.vector_odd {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (hD : EvenData D) (hodd : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), raw (↑t, -x, 0) = -raw (↑t, x, 0)) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.vector (t, -x, θ) = -G.vector (t, x, θ)

The actual raw velocity is odd at every time; its exterior definition uses the same retraction.

theorem EulerMeanPacketProvider.Forcing.vectorDerivative_odd {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (hD : EvenData D) (hodd : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), raw (↑t, -x, 0) = -raw (↑t, x, 0)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.vectorDerivative (↑t, -x, θ) = -G.vectorDerivative (↑t, x, θ)

Actual within-time derivatives preserve the odd velocity parity at both endpoints.

theorem EulerMeanPacketProvider.Forcing.pressureRepresentative_equation {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.vectorDerivative (↑t, x, θ) + ((D.M.field t) x) (G.vector (↑t, x, θ)) + EulerMeanScalarPressure.pathRepresentative D.T G.pressureForcePath ⋯ t x = raw (↑t, x, θ)

The pressure-force representative satisfies the already constructed physical equation.

theorem EulerMeanPacketProvider.Forcing.pressureRepresentative_odd {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (hD : EvenData D) (hodd : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), raw (↑t, -x, 0) = -raw (↑t, x, 0)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : EulerMeanScalarPressure.pathRepresentative D.T G.pressureForcePath ⋯ t (-x) = -EulerMeanScalarPressure.pathRepresentative D.T G.pressureForcePath ⋯ t x

theorem EulerMeanPacketProvider.Forcing.scalar_even {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (hD : EvenData D) (hodd : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), raw (↑t, -x, 0) = -raw (↑t, x, 0)) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.scalar (t, -x, θ) = G.scalar (t, x, θ)

Canonical radial normalization makes the actual scalar pressure even.

theorem EulerMeanPacketProvider.meanSolve_odd (D : Data) (hD : EvenData D) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) (hodd : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), raw (↑t, -x, 0) = -raw (↑t, x, 0)) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : (meanSolve D raw).1 (t, -x, -θ) = -(meanSolve D raw).1 (t, x, θ)

theorem EulerMeanPacketProvider.meanSolve_even (D : Data) (hD : EvenData D) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) (hodd : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), raw (↑t, -x, 0) = -raw (↑t, x, 0)) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : (meanSolve D raw).2 (t, -x, -θ) = (meanSolve D raw).2 (t, x, θ)