Support and joint odd parity of the actual high-pressure gradient used in the recursion.

theorem EulerTransversePacketProvider.Forcing.scalarGradient_zero_outside {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ℝ) (x : EulerSmoothLimit.Space) (hx : x ∉ D.support) (θ : ℝ) : EulerPacketCylinderField.pressureGradient (G.scalar I) (t, x, θ) = 0

theorem EulerTransversePacketProvider.Forcing.scalarGradientField_supported {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (t : ↑(Set.Icc 0 D.T)) : (G.scalarGradientField I).path t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯

theorem EulerTransversePacketProvider.Forcing.scalarGradient_odd {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : Data U} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing P D raw) (I : InitialData P D) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ D.support ↔ x ∈ D.support) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) (-x) = (D.F.field t) x) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.M.field t) (-x) = (D.M.field t) x) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, -x, -θ) = -raw (↑t, x, θ)) (hinit : (EulerCylinderFieldReflection.reflection P) ↑I.value = -↑I.value) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerPacketCylinderField.pressureGradient (G.scalar I) (↑t, -x, -θ) = -EulerPacketCylinderField.pressureGradient (G.scalar I) (↑t, x, θ)

theorem EulerTransversePacketProvider.highSolvePressureGradientField_supported (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : Data U) (I : InitialData P D) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing P D raw)) (t : ↑(Set.Icc 0 D.T)) : (highSolvePressureGradientField P D I raw h).path t ∈ EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space D.support ⋯