Actual odd terminal data give odd endpoint histories under even coefficients.
theorem
EulerCylinderDirichlet.Coefficients.endpointForcing_odd
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
(D : Coefficients T U E)
(hQ₁ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.Q₁ t) (-x) = (D.Q₁ t) x)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : (EulerCylinderFieldReflection.reflection P) Y = -Y)
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderFieldReflection.reflection P) (((endpointForcing P D) Y) t) = -((endpointForcing P D) Y) t
theorem
EulerCylinderDirichlet.Coefficients.endpointCoordinate_odd
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.Q t) (-x) = (D.Q t) x)
(hQ₁ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.Q₁ t) (-x) = (D.Q₁ t) x)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.H t) (-x) = (D.H t) x)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : (EulerCylinderFieldReflection.reflection P) Y = -Y)
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderFieldReflection.reflection P) (((endpointCoordinate P D) Y) t) = -((endpointCoordinate P D) Y) t
theorem
EulerCylinderDirichlet.Coefficients.endpointAcceleration_odd
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.Q t) (-x) = (D.Q t) x)
(hQ₁ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.Q₁ t) (-x) = (D.Q₁ t) x)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.H t) (-x) = (D.H t) x)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : (EulerCylinderFieldReflection.reflection P) Y = -Y)
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderFieldReflection.reflection P) (((endpointAcceleration P D) Y) t) = -((endpointAcceleration P D) Y) t
theorem
EulerCylinderDirichlet.Coefficients.endpointVelocity_odd
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.Q t) (-x) = (D.Q t) x)
(hQ₁ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.Q₁ t) (-x) = (D.Q₁ t) x)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.H t) (-x) = (D.H t) x)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : (EulerCylinderFieldReflection.reflection P) Y = -Y)
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderFieldReflection.reflection P) (((endpointVelocity P D) Y) t) = -((endpointVelocity P D) Y) t
theorem
EulerCylinderDirichlet.Coefficients.endpointDerivative_odd
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{E : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(D : Coefficients T U E)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.Q t) (-x) = (D.Q t) x)
(hQ₁ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.Q₁ t) (-x) = (D.Q₁ t) x)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (D.H t) (-x) = (D.H t) x)
(Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U))
(hY : (EulerCylinderFieldReflection.reflection P) Y = -Y)
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderFieldReflection.reflection P) (((endpointDerivative P D) Y) t) = -((endpointDerivative P D) Y) t