Exact coordinate words and tensor norm bounds for the real periodic cover of a smooth cylinder field.

theorem EulerCylinderSmoothOrbit.coverField_eq_euclidean (P : ℝ) {V : Type u_1} (f : EulerLiftedGradientSpace.LiftDomain P → V) : (fun (x : EulerLiftedGradientSpace.LiftTangent) => f (EulerLiftedGradientSpace.coveringMap P x)) = EulerCylinderSobolev.euclideanLift P f 0 ∘ ⇑↑EulerCylinderCoordinates.coordinateEquiv.symm

theorem EulerCylinderSmoothOrbit.coverField_word (P : ℝ) {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} (w : Fin n → Fin 4) (f : EulerLiftedGradientSpace.LiftDomain P → V) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) (x : EulerLiftedGradientSpace.LiftTangent) : EulerCylinderSobolev.iteratedFieldDerivative P w f (EulerLiftedGradientSpace.coveringMap P x) = (iteratedFDeriv ℝ n (fun (y : EulerLiftedGradientSpace.LiftTangent) => f (EulerLiftedGradientSpace.coveringMap P y)) x) fun (i : Fin n) => EulerCylinderSobolev.standardDirection (w i)

theorem EulerCylinderSmoothOrbit.coverField_tensor_norm_le (P : ℝ) {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain P → V) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) (x : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (fun (y : EulerLiftedGradientSpace.LiftTangent) => f (EulerLiftedGradientSpace.coveringMap P y)) x‖ ≤ ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ ^ n * ∑ w : Fin n → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative P w f (EulerLiftedGradientSpace.coveringMap P x)‖