The literal corrector preserves joint odd parity under the actual even inverse deformation.

Jointly odd transverse profiles give the actual jointly even vector potential.

theorem EulerPacketAngularPotential.potential_joint_even (P : ℝ) (hP : P ≠ 0) (m : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space) (hm : ∀ (x : EulerSmoothLimit.Space), m (-x) = m x) (hA : ∀ (x : EulerSmoothLimit.Space), Continuous (A x)) (hper : ∀ (x : EulerSmoothLimit.Space), Function.Periodic (A x) P) (hmean : ∀ (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, A x θ = 0) (hodd : ∀ (x : EulerSmoothLimit.Space) (θ : ℝ), A (-x) (-θ) = -A x θ) (x : EulerSmoothLimit.Space) (θ : ℝ) : potential P (m (-x)) (A (-x)) (-θ) = potential P (m x) (A x) θ

theorem EulerTransversePacketProvider.Data.rawPotential_smooth {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (P : ℝ) [Fact (0 < P)] (A : EulerPacketProfileRecursion.VectorField) (t : ℝ) (hA : ContDiff ℝ ↑⊤ fun (y : EulerLiftedGradientSpace.LiftTangent) => A (t, y)) : ContDiff ℝ ↑⊤ fun (y : EulerLiftedGradientSpace.LiftTangent) => D.rawPotential P A (t, y)

theorem EulerTransversePacketProvider.Data.rawPotential_even {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (P : ℝ) [Fact (0 < P)] (A : EulerPacketProfileRecursion.VectorField) (t : ℝ) (hInv : ∀ (x : EulerSmoothLimit.Space), (D.FInv.field (D.clamp t)) (-x) = (D.FInv.field (D.clamp t)) x) (hA : ContDiff ℝ ↑⊤ fun (y : EulerLiftedGradientSpace.LiftTangent) => A (t, y)) (hper : ∀ (x : EulerSmoothLimit.Space), Function.Periodic (fun (θ : ℝ) => A (t, x, θ)) P) (hmean : ∀ (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, A (t, x, θ) = 0) (hodd : ∀ (x : EulerSmoothLimit.Space) (θ : ℝ), A (t, -x, -θ) = -A (t, x, θ)) (x : EulerSmoothLimit.Space) (θ : ℝ) : D.rawPotential P A (t, -x, -θ) = D.rawPotential P A (t, x, θ)

theorem EulerTransversePacketProvider.Data.curlCorrector_odd {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (P : ℝ) [Fact (0 < P)] (A : EulerPacketProfileRecursion.VectorField) (t : ℝ) (hInv : ∀ (x : EulerSmoothLimit.Space), (D.FInv.field (D.clamp t)) (-x) = (D.FInv.field (D.clamp t)) x) (hA : ContDiff ℝ ↑⊤ fun (y : EulerLiftedGradientSpace.LiftTangent) => A (t, y)) (hper : ∀ (x : EulerSmoothLimit.Space), Function.Periodic (fun (θ : ℝ) => A (t, x, θ)) P) (hmean : ∀ (x : EulerSmoothLimit.Space), ∫ (θ : ℝ) in 0..P, A (t, x, θ) = 0) (hodd : ∀ (x : EulerSmoothLimit.Space) (θ : ℝ), A (t, -x, -θ) = -A (t, x, θ)) (x : EulerSmoothLimit.Space) (θ : ℝ) : D.curlCorrector P A (t, -x, -θ) = -D.curlCorrector P A (t, x, θ)

theorem EulerTransversePacketProvider.Forcing.corrector_odd {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) (hInv : ∀ (x : EulerSmoothLimit.Space), (D.FInv.field t) (-x) = (D.FInv.field t) x) (hA : ∀ (x : EulerSmoothLimit.Space) (θ : ℝ), G.vector I (↑t, -x, -θ) = -G.vector I (↑t, x, θ)) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.corrector I (↑t, -x, -θ) = -G.corrector I (↑t, x, θ)