Literal slice and scalar-pressure regularity of the actually generated source profiles.

theorem EulerPacketCylinderField.Field.sliceDifferentiable {P T : ℝ} [Fact (0 < P)] {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw_t) (hT : 0 ≤ T) (hd : TimeDerivative hT G H) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerPacketPointJets.SliceDifferentiable (Set.Icc 0 T) raw (↑t, x, θ)

theorem EulerPacketCylinderField.source_high_slice (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (p : ℕ) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerPacketPointJets.SliceDifferentiable (Set.Icc 0 M.T) (sourceProfiles P M D I Iprimary p).high (↑t, x, θ)

theorem EulerPacketCylinderField.source_mean_slice (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (p : ℕ) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerPacketPointJets.SliceDifferentiable (Set.Icc 0 M.T) (sourceProfiles P M D I Iprimary p).mean (↑t, x, θ)

theorem EulerPacketCylinderField.source_corrector_slice (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (p : ℕ) (t : ↑(Set.Icc 0 M.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerPacketPointJets.SliceDifferentiable (Set.Icc 0 M.T) (sourceProfiles P M D I Iprimary p).corrector (↑t, x, θ)

theorem EulerPacketCylinderField.source_highPressure_smooth (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (p : ℕ) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => (sourceProfiles P M D I Iprimary p).highPressure (t, y)

theorem EulerPacketCylinderField.source_meanPressure_smooth (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (p : ℕ) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => (sourceProfiles P M D I Iprimary p).meanPressure (t, y)

theorem EulerPacketCylinderField.source_meanPressure_angle (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (p : ℕ) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.pressureJet (sourceProfiles P M D I Iprimary p).meanPressure (t, x, θ)).2 EulerPacketPointJets.angleDirection = 0

theorem EulerPacketCylinderField.source_high_tangent (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (p : ℕ) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : inner ℝ (D.normalField (t, x, θ)) ((sourceProfiles P M D I Iprimary p).high (t, x, θ)) = 0