Joint parity of the complete constructed high inverse, pressure and actual corrector.

Joint parity of the actual source history inverse and its normalized pressure.

theorem EulerTransversePacketProvider.HistoryData.coordinatePath_reflection_neg {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} (B : HistoryData D) {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (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) (hH : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 D.T)) : (EulerCylinderFieldReflection.reflection P) ((B.coordinatePath G) t) = -(B.coordinatePath G) t

theorem EulerTransversePacketProvider.HistoryData.velocityPath_reflection_neg {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} (B : HistoryData D) {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (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) (hH : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 D.T)) : (EulerCylinderFieldReflection.reflection P) ((B.velocityPath G) t) = -(B.velocityPath G) t

theorem EulerTransversePacketProvider.HistoryData.derivativePath_reflection_neg {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} (B : HistoryData D) {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (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) (hH : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 D.T)) : (EulerCylinderFieldReflection.reflection P) ((B.derivativePath G) t) = -(B.derivativePath G) t

theorem EulerTransversePacketProvider.HistoryData.field_odd {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} (B : HistoryData D) {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (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) (hH : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : B.field G t (-x, ↑(-θ)) = -B.field G t (x, ↑θ)

theorem EulerTransversePacketProvider.HistoryData.normalResidual_odd {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} (B : HistoryData D) {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (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) (hH : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : B.normalResidual G t (-x, ↑(-θ)) = -B.normalResidual G t (x, ↑θ)

theorem EulerTransversePacketProvider.HistoryData.pressureField_even {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} (B : HistoryData D) {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (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) (hH : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : B.pressureField G t (-x, ↑(-θ)) = B.pressureField G t (x, ↑θ)

theorem EulerTransversePacketJoin.forwardInitial_reflection_neg {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.Forcing P D raw) (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) (hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) : (EulerCylinderFieldReflection.reflection P) ↑(forwardInitial τ hτ hτT B G).value = -↑(forwardInitial τ hτ hτT B G).value

theorem EulerTransversePacketJoin.futureVelocity_reflection_neg {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.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) (hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 (D.T - τ))) : (EulerCylinderFieldReflection.reflection P) ((futureVelocity τ hτ hτT B G) t) = -(futureVelocity τ hτ hτT B G) t

theorem EulerTransversePacketJoin.velocityPath_reflection_neg {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.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) (hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 D.T)) : (EulerCylinderFieldReflection.reflection P) ((velocityPath τ hτ hτT B G) t) = -(velocityPath τ hτ hτT B G) t

theorem EulerTransversePacketJoin.vector_odd {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.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) (hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : vector τ hτ hτT B G (↑t, -x, -θ) = -vector τ hτ hτT B G (↑t, x, θ)

theorem EulerTransversePacketJoin.vectorDerivative_odd {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.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) (hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : vectorDerivative τ hτ hτT B G (↑t, -x, -θ) = -vectorDerivative τ hτ hτT B G (↑t, x, θ)

theorem EulerTransversePacketJoin.scalar_even {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.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) (hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : scalar τ hτ hτT B G (↑t, -x, -θ) = scalar τ hτ hτT B G (↑t, x, θ)

theorem EulerTransversePacketJoin.curlCorrector_odd {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.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) (hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : D.curlCorrector P (vector τ hτ hτT B G) (↑t, -x, -θ) = -D.curlCorrector P (vector τ hτ hτT B G) (↑t, x, θ)

theorem EulerTransversePacketJoin.correctorDerivative_odd {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerTransversePacketProvider.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) (hH : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)) (x : EulerSmoothLimit.Space), (B.H.field t) (-x) = (B.H.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : correctorDerivative τ hτ hτT B G (↑t, -x, -θ) = -correctorDerivative τ hτ hτT B G (↑t, x, θ)