The constructed forward transverse provider in the literal packet jet equation.

theorem EulerPacketPointJets.pressureJet_angle_derivative (p : EulerPacketProfileRecursion.ScalarField) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) (hp : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p (t, y)) (x, θ)) : (pressureJet p (t, x, θ)).2 angleDirection = deriv (fun (s : ℝ) => p (t, x, s)) θ

theorem EulerPacketPointJets.fastPressure_pressureJet (m : EulerSmoothLimit.Space) (p : EulerPacketProfileRecursion.ScalarField) (t : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) (hp : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => p (t, y)) (x, θ)) : (fastPressure m) (pressureJet p (t, x, θ)) = deriv (fun (s : ℝ) => p (t, x, s)) θ • m

theorem EulerTransversePacketProvider.Forcing.slicedJet_time {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)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) (G.vector I) (↑t, x, θ)).2 EulerPacketPointJets.timeDirection = G.vectorDerivative I (↑t, x, θ)

theorem EulerTransversePacketProvider.Forcing.jet_equation {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)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.linearPart (D.strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) (G.vector I) (↑t, x, θ)) + (EulerPacketPointJets.fastPressure (D.normalField (↑t, x, θ))) (EulerPacketPointJets.pressureJet (G.scalar I) (↑t, x, θ)) = raw (↑t, x, θ)

This exact high-frequency equation is the interface used in the grade recursion.

theorem EulerTransversePacketProvider.highSolve_jet_equation {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)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (EulerPacketPointJets.linearPart (D.strain (↑t, x, θ))) (EulerPacketPointJets.slicedJet (Set.Icc 0 D.T) (highSolve P D I raw).1 (↑t, x, θ)) + (EulerPacketPointJets.fastPressure (D.normalField (↑t, x, θ))) (EulerPacketPointJets.pressureJet (highSolve P D I raw).2 (↑t, x, θ)) = raw (↑t, x, θ)