Joint odd parity of the actual transverse velocity, its time derivative, and its corrector.

Reflection parity of the actual Gram-projected source evolution and its physical velocity.

Independence and symmetries of the actual forward solve

The forced solution is independent of the selected homogeneous fundamental representation. Consequently coefficient symmetries pass to the solution without assuming any corresponding symmetry of that representation.

theorem EulerLinearDuhamel.Evolution.solution_independent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {T : ℝ} {hT : 0 ≤ T} {B : C(↑(Set.Icc 0 T), E →L[ℝ] E)} (U V : Evolution T hT B) (f : C(↑(Set.Icc 0 T), E)) (a₀ : E) : U.solution f a₀ = V.solution f a₀

The true forced path is independent of the fundamental evolution chosen to represent it.

theorem EulerLinearDuhamel.Evolution.solution_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {T : ℝ} {hT : 0 ≤ T} {B : C(↑(Set.Icc 0 T), E →L[ℝ] E)} (U : Evolution T hT B) (f : C(↑(Set.Icc 0 T), E)) (a₀ : E) : U.solution (-f) (-a₀) = -U.solution f a₀

Sign reversal of both data reverses the actual solution.

@[simp]

theorem EulerLinearDuhamel.Evolution.solution_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {T : ℝ} {hT : 0 ≤ T} {B : C(↑(Set.Icc 0 T), E →L[ℝ] E)} (U : Evolution T hT B) : U.solution 0 0 = 0

Zero data vanish identically.

theorem EulerLinearDuhamel.solution_odd_under {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : Type u_2} (T : ℝ) (hT : 0 ≤ T) (B : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (U : (x : P) → Evolution T hT (B x)) (σ : P → P) (hB : ∀ (x : P), B (σ x) = B x) (f : P → C(↑(Set.Icc 0 T), E)) (a₀ : P → E) (hf : ∀ (x : P), f (σ x) = -f x) (ha₀ : ∀ (x : P), a₀ (σ x) = -a₀ x) (x : P) : (U (σ x)).solution (f (σ x)) (a₀ (σ x)) = -(U x).solution (f x) (a₀ x)

Reflection or any other parameter symmetry is inherited from coefficients and data; no regularity or symmetry of the chosen propagators is required.

theorem EulerLinearDuhamel.solution_support_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : Type u_2} (T : ℝ) (hT : 0 ≤ T) (B : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (U : (x : P) → Evolution T hT (B x)) (f : P → C(↑(Set.Icc 0 T), E)) (a₀ : P → E) : (Function.support fun (x : P) => (U x).solution (f x) (a₀ x)) ⊆ Function.support f ∪ Function.support a₀

The actual forward solution stays in the union of the supports of its data.

Actual supported forward evolution preserves joint odd parity for even coefficients.

theorem EulerCylinderForwardParity.solution_reflection (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (hB : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (B t) (-x) = (B t) x) (U : EulerLinearDuhamel.Evolution T hT (EulerLpCylinderCoefficients.liftedOperatorPath P S hS T B)) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P V S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P V S hS)) : (EulerCylinderFieldReflection.supportedPathReflection P S hS hSym) (U.solution f a₀) = U.solution ((EulerCylinderFieldReflection.supportedPathReflection P S hS hSym) f) ((EulerCylinderFieldReflection.supportedReflection P S hS hSym) a₀)

theorem EulerCylinderForwardParity.solution_reflection_neg (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (hB : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (B t) (-x) = (B t) x) (U : EulerLinearDuhamel.Evolution T hT (EulerLpCylinderCoefficients.liftedOperatorPath P S hS T B)) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P V S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P V S hS)) (hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderFieldReflection.supportedReflection P S hS hSym) (f t) = -f t) (ha₀ : (EulerCylinderFieldReflection.supportedReflection P S hS hSym) a₀ = -a₀) (t : ↑(Set.Icc 0 T)) : (EulerCylinderFieldReflection.supportedReflection P S hS hSym) ((U.solution f a₀) t) = -(U.solution f a₀) t

theorem EulerCylinderForwardParity.solution_full_reflection_neg (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (hB : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (B t) (-x) = (B t) x) (U : EulerLinearDuhamel.Evolution T hT (EulerLpCylinderCoefficients.liftedOperatorPath P S hS T B)) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P V S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P V S hS)) (hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderFieldReflection.reflection P) ↑(f t) = -↑(f t)) (ha₀ : (EulerCylinderFieldReflection.reflection P) ↑a₀ = -↑a₀) (t : ↑(Set.Icc 0 T)) : (EulerCylinderFieldReflection.reflection P) ↑((U.solution f a₀) t) = -↑((U.solution f a₀) t)

theorem EulerSourceCylinderParity.sourceForcing_even {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (hE : ∀ (t : K) (x : EulerSmoothLimit.Space), (Q.field t) (-x) = (Q.field t) x) (t : K) (x : EulerSmoothLimit.Space) : ((EulerSourceForwardCoefficient.sourceForcing Q c hc hQ) t) (-x) = ((EulerSourceForwardCoefficient.sourceForcing Q c hc hQ) t) x

theorem EulerSourceCylinderParity.sourceGenerator_even {K : Type u_1} {U : Type u_2} {E : Type u_3} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : K) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (hE : ∀ (t : K) (x : EulerSmoothLimit.Space), (Q.field t) (-x) = (Q.field t) x) (hE₁ : ∀ (t : K) (x : EulerSmoothLimit.Space), (Q₁.field t) (-x) = (Q₁.field t) x) (t : K) (x : EulerSmoothLimit.Space) : ((EulerSourceForwardCoefficient.sourceGenerator Q Q₁ c hc hQ) t) (-x) = ((EulerSourceForwardCoefficient.sourceGenerator Q Q₁ c hc hQ) t) x

theorem EulerSourceCylinderParity.projectedForcing_reflection_neg (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (Q : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (hE : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (Q.field t) (-x) = (Q.field t) x) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderFieldReflection.reflection P) ↑(f t) = -↑(f t)) (t : ↑(Set.Icc 0 T)) : (EulerCylinderFieldReflection.reflection P) ↑((EulerSourceCylinderForcing.projectedForcing P S hS Q c hc hQ f) t) = -↑((EulerSourceCylinderForcing.projectedForcing P S hS Q c hc hQ f) t)

theorem EulerSourceCylinderParity.coordinates_reflection_neg (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (hE : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (Q.field t) (-x) = (Q.field t) x) (hE₁ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (Q₁.field t) (-x) = (Q₁.field t) x) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderFieldReflection.reflection P) ↑(f t) = -↑(f t)) (ha₀ : (EulerCylinderFieldReflection.reflection P) ↑a₀ = -↑a₀) (t : ↑(Set.Icc 0 T)) : (EulerCylinderFieldReflection.reflection P) ↑((EulerSourceCylinderEquation.coordinates P S hS T hT Q Q₁ c hc hQ f a₀) t) = -↑((EulerSourceCylinderEquation.coordinates P S hS T hT Q Q₁ c hc hQ f a₀) t)

theorem EulerSourceCylinderParity.velocity_reflection_neg (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (hE : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (Q.field t) (-x) = (Q.field t) x) (hE₁ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (Q₁.field t) (-x) = (Q₁.field t) x) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderFieldReflection.reflection P) ↑(f t) = -↑(f t)) (ha₀ : (EulerCylinderFieldReflection.reflection P) ↑a₀ = -↑a₀) (t : ↑(Set.Icc 0 T)) : (EulerCylinderFieldReflection.reflection P) ↑((EulerSourceCylinderEquation.velocity P S hS T hT Q Q₁ c hc hQ f a₀) t) = -↑((EulerSourceCylinderEquation.velocity P S hS T hT Q Q₁ c hc hQ f a₀) t)

theorem EulerSourceCylinderParity.coordinateDerivative_reflection_neg (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (hE : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (Q.field t) (-x) = (Q.field t) x) (hE₁ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (Q₁.field t) (-x) = (Q₁.field t) x) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderFieldReflection.reflection P) ↑(f t) = -↑(f t)) (ha₀ : (EulerCylinderFieldReflection.reflection P) ↑a₀ = -↑a₀) (t : ↑(Set.Icc 0 T)) : (EulerCylinderFieldReflection.reflection P) ↑((EulerSourceCylinderEquation.coordinateDerivative P S hS T hT Q Q₁ c hc hQ f a₀) t) = -↑((EulerSourceCylinderEquation.coordinateDerivative P S hS T hT Q Q₁ c hc hQ f a₀) t)

theorem EulerSourceCylinderParity.velocityDerivative_reflection_neg (P : ℝ) [Fact (0 < P)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (hE : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (Q.field t) (-x) = (Q.field t) x) (hE₁ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (Q₁.field t) (-x) = (Q₁.field t) x) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderFieldReflection.reflection P) ↑(f t) = -↑(f t)) (ha₀ : (EulerCylinderFieldReflection.reflection P) ↑a₀ = -↑a₀) (t : ↑(Set.Icc 0 T)) : (EulerCylinderFieldReflection.reflection P) ↑((EulerSourceCylinderEquation.velocityDerivative P S hS T hT Q Q₁ c hc hQ f a₀) t) = -↑((EulerSourceCylinderEquation.velocityDerivative P S hS T hT Q Q₁ c hc hQ f a₀) t)

theorem EulerTransversePacketProvider.Data.frame_even {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (D.frame.field t) (-x) = (D.frame.field t) x

theorem EulerTransversePacketProvider.Data.frameDerivative_even {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (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) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (D.frameDerivative.field t) (-x) = (D.frameDerivative.field t) x

theorem EulerTransversePacketProvider.Data.inverse_even {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (D.FInv.field t) (-x) = (D.FInv.field t) x

theorem EulerTransversePacketProvider.Data.normal_even {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (D.normal.field t) (-x) = (D.normal.field t) x

noncomputable def EulerTransversePacketProvider.Forcing.forcingField {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) : EulerPacketCylinderField.Field P D.T raw

Forcing field, bundling path, orbit, raw_eq.

Equations

• G.forcingField = { path := (EulerLpCylinderPaths.includePath P D.support ⋯) G.path, orbit := ⋯, raw_eq := ⋯ }

theorem EulerTransversePacketProvider.Forcing.path_reflection_neg {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (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) ↑(G.path t) = -↑(G.path t)

theorem EulerTransversePacketProvider.Forcing.velocityPath_reflection_neg {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)) : (EulerCylinderFieldReflection.reflection P) ((G.fullVelocityPath I) t) = -(G.fullVelocityPath I) t

theorem EulerTransversePacketProvider.Forcing.derivativePath_reflection_neg {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)) : (EulerCylinderFieldReflection.reflection P) ((G.fullDerivativePath I) t) = -(G.fullDerivativePath I) t

theorem EulerTransversePacketProvider.Forcing.vector_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.vector I (↑t, -x, -θ) = -G.vector I (↑t, x, θ)

theorem EulerTransversePacketProvider.Forcing.vectorDerivative_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.vectorDerivative I (↑t, -x, -θ) = -G.vectorDerivative I (↑t, x, θ)

theorem EulerTransversePacketProvider.Forcing.corrector_odd_of_data {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.corrector I (↑t, -x, -θ) = -G.corrector I (↑t, x, θ)