Even parity of the actual normalized transverse pressure from the odd solved velocity.

@[reducible, inline]

noncomputable abbrev EulerTransversePacketProvider.Forcing.normalResidualField {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)) (x : EulerLiftedGradientSpace.LiftDomain P) : ℝ

Normal residual field type used in transverse packet pressure parity.

Equations

• G.normalResidualField I = EulerSourceCylinderClassical.normalResidual P D.support ⋯ ⋯ D.T ⋯ D.frame D.frameDerivative D.frameLower ⋯ ⋯ G.path I.value ⋯ ⋯ D.M D.normal

theorem EulerTransversePacketProvider.Forcing.normalResidualField_formula {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)) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.normalResidualField I t (x, ↑θ) = (inner ℝ ((D.normal.field t) x) (raw (↑t, x, θ)) - 2 * inner ℝ ((D.normal.field t) x) (((D.M.field t) x) (G.vector I (↑t, x, θ)))) / ‖(D.normal.field t) x‖ ^ 2

theorem EulerTransversePacketProvider.Forcing.normalResidualField_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) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (hinit : (EulerCylinderFieldReflection.reflection P) ↑I.value = -↑I.value) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.normalResidualField I t (-x, ↑(-θ)) = -G.normalResidualField I t (x, ↑θ)

theorem EulerTransversePacketProvider.Forcing.scalar_even {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) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (hinit : (EulerCylinderFieldReflection.reflection P) ↑I.value = -↑I.value) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.scalar I (↑t, -x, -θ) = G.scalar I (↑t, x, θ)

theorem EulerTransversePacketProvider.highSolve_parity (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : Data U) (I : InitialData P D) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing P D raw)) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (hinit : (EulerCylinderFieldReflection.reflection P) ↑I.value = -↑I.value) : (∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (highSolve P D I raw).1 (↑t, -x, -θ) = -(highSolve P D I raw).1 (↑t, x, θ)) ∧ ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (highSolve P D I raw).2 (↑t, -x, -θ) = (highSolve P D I raw).2 (↑t, x, θ)