Full space-angle derivative tensors are bounded by the actual packet word budgets. This includes the scalar pressure via its norm-one embedding.

theorem EulerPacketCylinderField.Field.raw_eq_euclidean {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) : (fun (z : EulerLiftedGradientSpace.LiftTangent) => raw (↑t, z)) = EulerCylinderSobolev.euclideanLift P (G.toFieldTower.pointField t) 0 ∘ ⇑↑EulerCylinderCoordinates.coordinateEquiv.symm

theorem EulerPacketCylinderField.Field.WordBound.raw_tensor_le {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (hq : 3 ≤ q) (t : ↑(Set.Icc 0 T)) (n : ℕ) (z : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (fun (y : EulerLiftedGradientSpace.LiftTangent) => raw (↑t, y)) z‖ ≤ ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ ^ n * (EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * A * EulerGevrey.majorant R d n)

theorem EulerPacketCylinderField.Field.WordBound.raw_fderiv_le {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (hq : 3 ≤ q) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent) : ‖fderiv ℝ (fun (y : EulerLiftedGradientSpace.LiftTangent) => raw (↑t, y)) z‖ ≤ ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * (EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * A * EulerGevrey.majorant R d 1)