Uniform-time spatial word bounds imply the genuine Bochner word bounds.

theorem EulerMeanTimeContinuousTranslation.pathLpOperator_norm_sqrt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) : ‖EulerTimeLp.pathLpOperator T hT‖ ≤ √T

theorem EulerMeanTimeContinuousTranslation.timeTranslation_pathLp (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) : (EulerMeanTimeTranslation.timeTranslation T a) (EulerTimeLp.pathLp T hT p) = EulerTimeLp.pathLp T hT ((pathTranslation T a) p)

theorem EulerMeanTimeContinuousTranslation.pathLp_block_le {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (pathTranslation T a) p) (n : ℕ) (x : EulerSmoothLimit.Space) : EulerParameterWordGevrey.block directions q (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) (EulerTimeLp.pathLp T hT p)) n x ≤ √T * EulerParameterWordGevrey.block directions q (fun (a : EulerSmoothLimit.Space) => (pathTranslation T a) p) n x

The genuine Bochner embedding commutes with all external spatial words.