The actual scalar pressure gradient uses one external word and keeps the same radius.

noncomputable def EulerPacketCylinderField.scalarGradientPath {P : ℝ} [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

Scalar gradient path, given by ∑ i : Fin 3, pathMap P (gradientComponent i) (derivativePath P (pathMap P scalarEmbed p) i.succ).

Equations

• One or more equations did not get rendered due to their size.

theorem EulerPacketCylinderField.scalarGradientPath_orbit {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) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (scalarGradientPath p)

theorem EulerPacketCylinderField.scalarGradientPath_block_bound {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) (q n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) (scalarGradientPath p)) n a ≤ 3 * EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) (n + 1) a

theorem EulerPacketCylinderField.scalarGradientPath_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) (q : ℕ) (R A : ℝ) (d : ℕ) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) n 0 ≤ A * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) (scalarGradientPath p)) n 0 ≤ 3 * A * EulerGevrey.majorant R (d + 1) n

theorem EulerPacketCylinderField.scalarGradientField_path {P : ℝ} [Fact (0 < P)] {T : ℝ} (raw : EulerPacketProfileRecursion.ScalarField) (p : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P p hp t (x, ↑θ)) : (scalarGradientField raw p hp he).path = scalarGradientPath p

theorem EulerPacketCylinderField.scalarGradientField_block_bound {P : ℝ} [Fact (0 < P)] {T : ℝ} (raw : EulerPacketProfileRecursion.ScalarField) (p : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P p hp t (x, ↑θ)) (q n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) (scalarGradientField raw p hp he).path) n a ≤ 3 * EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) (n + 1) a

theorem EulerPacketCylinderField.scalarGradientField_majorant {P : ℝ} [Fact (0 < P)] {T : ℝ} (raw : EulerPacketProfileRecursion.ScalarField) (p : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P p hp t (x, ↑θ)) (q : ℕ) (R A : ℝ) (d : ℕ) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) n 0 ≤ A * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) (scalarGradientField raw p hp he).path) n 0 ≤ 3 * A * EulerGevrey.majorant R (d + 1) n