Actual mixed translation orbits are smooth everywhere as soon as they are smooth at zero.

@[simp]

theorem EulerLpCylinderTranslation.pathTranslate_zero (period : ℝ) [Fact (0 < period)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [TopologicalSpace K] (f : C(K, ↥(CylinderL2 period V))) : (pathTranslate period 0) f = f

theorem EulerLpCylinderTranslation.pathTranslate_add (period : ℝ) [Fact (0 < period)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [TopologicalSpace K] (a b : EulerLiftedGradientSpace.LiftTangent) (f : C(K, ↥(CylinderL2 period V))) : (pathTranslate period a) ((pathTranslate period b) f) = (pathTranslate period (a + b)) f

The true uniform-time mixed translations obey the group law.

theorem EulerLpCylinderTranslation.pathOrbit_contDiff_of_zero (period : ℝ) [Fact (0 < period)] {V : Type u_1} {K : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [TopologicalSpace K] [CompactSpace K] (f : C(K, ↥(CylinderL2 period V))) (hzero : ContDiffAt ℝ (↑⊤) (fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate period a) f) 0) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (pathTranslate period a) f

Local smoothness at zero propagates to the whole genuine mixed translation orbit.