Pressure-gradient bounds after literal time-profile division, with no profile extrema or time derivative.

theorem EulerPacketCylinderField.scalarWeightedOrbit {P : ℝ} [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (g : C(K, ℝ)) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.weight g) p)

theorem EulerPacketCylinderField.scalarGradientPath_weight {P : ℝ} [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (g : C(K, ℝ)) : scalarGradientPath ((EulerContinuousTimeWeight.weight g) p) = (EulerContinuousTimeWeight.weight g) (scalarGradientPath p)

theorem EulerPacketCylinderField.scalarGradientPath_normalize {P : ℝ} [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (g : C(K, ℝ)) (hg : ∀ (t : K), 0 < g t) : scalarGradientPath ((EulerContinuousTimeWeight.normalize g hg) p) = (EulerContinuousTimeWeight.normalize g hg) (scalarGradientPath p)

theorem EulerPacketCylinderField.scalarGradientPath_normalized_majorant {P : ℝ} [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (g : C(K, ℝ)) (hg : ∀ (t : K), 0 < g t) (q : ℕ) (R A : ℝ) (d : ℕ) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) p)) n 0 ≤ A * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (scalarGradientPath p))) n 0 ≤ 3 * A * EulerGevrey.majorant R (d + 1) n