Actual spatial jets outside a closed support and for angle-independent fields.

structure EulerPacketCylinderField.AngleIndependentJet (J : ℝ → EulerPacketPointJets.VectorJet) : Prop

Precisely the spatial parts of the jet that occur in the packet nonlinearities.

• value (θ : ℝ) : (J θ).1 = (J 0).1
• spatial (θ : ℝ) (v : EulerSmoothLimit.Space) : (J θ).2 (EulerPacketPointJets.spatialInjection v) = (J 0).2 (EulerPacketPointJets.spatialInjection v)
• angular (θ : ℝ) : (J θ).2 EulerPacketPointJets.angleDirection = 0

theorem EulerPacketCylinderField.AngleIndependentJet.zero : AngleIndependentJet fun (x : ℝ) => 0

theorem EulerPacketCylinderField.AngleIndependentJet.add {J K : ℝ → EulerPacketPointJets.VectorJet} (hJ : AngleIndependentJet J) (hK : AngleIndependentJet K) : AngleIndependentJet fun (θ : ℝ) => J θ + K θ

theorem EulerPacketCylinderField.raw_fderiv_zero_outside {T : ℝ} {raw : EulerPacketProfileRecursion.VectorField} (S : Set EulerSmoothLimit.Space) (hS : IsClosed S) (h : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∉ S, ∀ (θ : ℝ), raw (↑t, x, θ) = 0) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (hx : x ∉ S) (θ : ℝ) : fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => raw (↑t, y)) (x, θ) = 0

theorem EulerPacketCylinderField.slicedJet_angleIndependent_of_support {T : ℝ} {raw : EulerPacketProfileRecursion.VectorField} (s : Set ℝ) (S : Set EulerSmoothLimit.Space) (hS : IsClosed S) (h : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∉ S, ∀ (θ : ℝ), raw (↑t, x, θ) = 0) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (hx : x ∉ S) : AngleIndependentJet fun (θ : ℝ) => EulerPacketPointJets.slicedJet s raw (↑t, x, θ)

theorem EulerPacketCylinderField.Field.raw_fderiv_of_angleIndependent {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (h : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = raw (↑t, x, 0)) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => raw (↑t, y)) (x, θ) = fderiv ℝ (fun (y : EulerSmoothLimit.Space) => raw (↑t, y, 0)) x ∘SL ContinuousLinearMap.fst ℝ EulerSmoothLimit.Space ℝ

theorem EulerPacketCylinderField.Field.slicedJet_angleIndependent {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (s : Set ℝ) (h : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = raw (↑t, x, 0)) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : AngleIndependentJet fun (θ : ℝ) => EulerPacketPointJets.slicedJet s raw (↑t, x, θ)