The actual scalar pressure gives a symmetric curvature operator. Symmetry of the source history Hessian is consequently a theorem about the constructed parent data, rather than an independent hypothesis.
theorem
EulerParentPacketFrames.hessian_isSymmetric
(p : EulerSmoothLimit.Space → ℝ)
(hp : ContDiff ℝ 2 p)
(x : EulerSmoothLimit.Space)
:
(↑(fderiv ℝ (gradient p) x)).IsSymmetric
theorem
EulerParentPacketFrames.Parent.curvature_symmetric
(G : Parent)
(p : ↑(Set.Icc 0 G.T) → EulerSmoothLimit.Space → ℝ)
(hp : ∀ (t : ↑(Set.Icc 0 G.T)), ContDiff ℝ (↑⊤) (p t))
(hacceleration :
∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.acceleration.field t) x = -gradient (p t) (G.position t x))
(t : ↑(Set.Icc 0 G.T))
(x : EulerSmoothLimit.Space)
:
(↑((G.curvature.field t) x)).IsSymmetric
theorem
EulerParentPacketFrames.Parent.history_symmetric
(G : Parent)
(p : ↑(Set.Icc 0 G.T) → EulerSmoothLimit.Space → ℝ)
(hp : ∀ (t : ↑(Set.Icc 0 G.T)), ContDiff ℝ (↑⊤) (p t))
(hacceleration :
∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.acceleration.field t) x = -gradient (p t) (G.position t x))
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(H : LowBounds G)
(t : ↑(Set.Icc 0 G.T))
(x : EulerSmoothLimit.Space)
:
(↑(((G.historyData m hm R S hS H).H.field t) x)).IsSymmetric
theorem
EulerParentPacketFrames.Parent.initial_history_symmetric
(G : Parent)
(p : ↑(Set.Icc 0 G.T) → EulerSmoothLimit.Space → ℝ)
(hp : ∀ (t : ↑(Set.Icc 0 G.T)), ContDiff ℝ (↑⊤) (p t))
(hacceleration :
∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.acceleration.field t) x = -gradient (p t) (G.position t x))
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(H : LowBounds G)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ ≤ G.T)
(t : ↑(Set.Icc 0 τ))
(x : EulerSmoothLimit.Space)
:
(↑((((G.historyData m hm R S hS H).initial τ hτ hτT).H.field t) x)).IsSymmetric