Exact ordinary derivatives of the raw covering field of a smooth cylinder representative.

theorem EulerCylinderSmoothOrbit.coverField_eq_local (P : ℝ) {V : Type u_1} (f : EulerLiftedGradientSpace.LiftDomain P → V) : (fun (z : EulerLiftedGradientSpace.LiftTangent) => f (z.1, ↑z.2)) = EulerMetricTransport.localFieldLift P f 0

theorem EulerCylinderSmoothOrbit.coverField_fderiv (P : ℝ) {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerLiftedGradientSpace.LiftDomain P → V) (z : EulerLiftedGradientSpace.LiftTangent) : fderiv ℝ (fun (y : EulerLiftedGradientSpace.LiftTangent) => f (y.1, ↑y.2)) z = EulerLiftedWeakDerivative.fieldFDeriv P f (z.1, ↑z.2)

theorem EulerCylinderSmoothOrbit.coverField_contDiff (P : ℝ) {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerLiftedGradientSpace.LiftDomain P → V) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) : ContDiff ℝ ↑⊤ fun (z : EulerLiftedGradientSpace.LiftTangent) => f (z.1, ↑z.2)

theorem EulerCylinderSmoothOrbit.coverField_spatial_fderiv (P : ℝ) {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerLiftedGradientSpace.LiftDomain P → V) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) (x : EulerSmoothLimit.Space) (θ : ℝ) : fderiv ℝ (fun (y : EulerSmoothLimit.Space) => f (y, ↑θ)) x = EulerLiftedWeakDerivative.fieldFDeriv P f (x, ↑θ) ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ

The raw spatial derivative is exactly the spatial restriction of the cylinder derivative.