Every actual classical spatial/angular word differentiates in time on the closed interval.
theorem
EulerCylinderSmoothOrbit.pointField_word_eq_evaluation
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(n : ℕ)
(w : Fin n → Fin 4)
(t : K)
(x : EulerLiftedGradientSpace.LiftDomain P)
:
EulerCylinderSobolev.iteratedFieldDerivative P w (pointField P p hp t) x = (EulerSobolevPointEvaluation.pointEvaluation P x)
((EulerSobolevWordBlocks.wordBlock P 3 n w) ((sobolevPath P (3 + n) p hp) t))
theorem
EulerCylinderSmoothOrbit.pointField_word_joint_continuous
(P : ℝ)
[Fact (0 < P)]
{K : Type u_1}
[TopologicalSpace K]
[CompactSpace K]
(p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(n : ℕ)
(w : Fin n → Fin 4)
:
Continuous fun (z : K × EulerLiftedGradientSpace.LiftDomain P) =>
EulerCylinderSobolev.iteratedFieldDerivative P w (pointField P p hp z.1) z.2
theorem
EulerCylinderSmoothOrbit.pointField_word_hasDerivWithinAt
(P : ℝ)
[Fact (0 < P)]
(T : ℝ)
(hT : 0 ≤ T)
(p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P)))
(hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p)
(hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT p) (f t) (Set.Icc 0 T) ↑t)
(n : ℕ)
(w : Fin n → Fin 4)
(t : ↑(Set.Icc 0 T))
(x : EulerLiftedGradientSpace.LiftDomain P)
:
HasDerivWithinAt
(fun (r : ℝ) => EulerCylinderSobolev.iteratedFieldDerivative P w (pointField P p hp (Set.projIcc 0 T hT r)) x)
(EulerCylinderSobolev.iteratedFieldDerivative P w (pointField P f hf t) x) (Set.Icc 0 T) ↑t
Time differentiation commutes with each actual spatial/angular word, including at endpoints.