The actual scalar pressure gradient is an admissible smooth L² field.

noncomputable def EulerMeanPacketProvider.Forcing.scalarGradient {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : EulerPacketProfileRecursion.VectorField

Scalar gradient, defined pointwise by gradient (fun x => G.scalar (z.1,(x,z.2.2))) z.2.1.

Equations

• G.scalarGradient z = gradient (fun (x : EulerSmoothLimit.Space) => G.scalar (z.1, x, z.2.2)) z.2.1

theorem EulerMeanPacketProvider.Forcing.scalarGradient_eq {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.scalarGradient (↑t, x, θ) = (ContinuousLinearMap.adjoint ((D.F.field t) x)) (G.pressureForce (↑t, x, θ))

noncomputable def EulerMeanPacketProvider.Forcing.scalarGradientForcing {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : Forcing D G.scalarGradient

All actual pressure-gradient jets are square-integrable and continuous in time.

Equations

• G.scalarGradientForcing = (G.pressureForceForcing.multiply (EulerMeanCoefficients.SmoothCoefficientPath.map EulerTransverseGramInverse.realAdjoint D.F)).congr ⋯

theorem EulerMeanPacketProvider.Forcing.physicalGradient_eq {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : (ContinuousLinearMap.adjoint (D.inverseFrame (↑t, x, θ))) (G.scalarGradient (↑t, x, θ)) = G.pressureForce (↑t, x, θ)