Joint parity of the constructed cylinder history #
Even coefficient fields commute with actual spatial-angular reflection. The genuine coercive inverse therefore preserves odd forcing, including its continuous velocity and acceleration representatives.
theorem
EulerCylinderFieldReflection.reflection_adjoint
(P : ℝ)
[Fact (0 < P)]
{V : Type u_1}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
:
theorem
EulerCylinderDirichlet.Coefficients.continuousVelocity_reflection
(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)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
((velocityPath P D) (EulerTimeLp.pathLp T ⋯ ((EulerCylinderFieldReflection.pathReflection P) f))) t = (EulerCylinderFieldReflection.reflection P) (((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f)) t)
theorem
EulerCylinderDirichlet.Coefficients.accelerationPath_reflection
(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)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
(accelerationPath P D ((EulerCylinderFieldReflection.pathReflection P) f)) t = (EulerCylinderFieldReflection.reflection P) ((accelerationPath P D f) t)
theorem
EulerCylinderDirichlet.Coefficients.accelerationPath_neg
(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)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
theorem
EulerCylinderDirichlet.Coefficients.velocityPath_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)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderFieldReflection.reflection P) (f t) = -f t)
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderFieldReflection.reflection P) (((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f)) t) = -((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f)) t
theorem
EulerCylinderDirichlet.Coefficients.accelerationPath_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)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderFieldReflection.reflection P) (f t) = -f t)
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderFieldReflection.reflection P) ((accelerationPath P D f) t) = -(accelerationPath P D f) t
theorem
EulerCylinderDirichlet.Coefficients.physicalVelocity_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)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderFieldReflection.reflection P) (f t) = -f t)
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderFieldReflection.reflection P) ((physicalVelocity P D f) t) = -(physicalVelocity P D f) t
theorem
EulerCylinderDirichlet.Coefficients.physicalDerivative_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)
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(hf : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderFieldReflection.reflection P) (f t) = -f t)
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderFieldReflection.reflection P) ((physicalDerivative P D f) t) = -(physicalDerivative P D f) t