Solved mean fields are actual admissible forcing fields

The genuine continuous L² solution path and its solved spatial translation orbit produce the literal smooth L² slices required by the forcing interface. The same construction applies to its actual time derivative and pressure force.

noncomputable def EulerMeanPacketProvider.Forcing.ofOrbitPath {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (p : C(↑(Set.Icc 0 D.T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T a) p) (heq : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = EulerMeanSmoothRepresentative.representative (p t) ⋯ x) : Forcing D raw

Actual path-orbit regularity is converted into literal spatial derivative data.

Equations

• One or more equations did not get rendered due to their size.

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

The output velocity of the genuine source mean solve can be used as the next forcing input.

Equations

• G.vectorForcing = EulerMeanPacketProvider.Forcing.ofOrbitPath G.velocityPath ⋯ ⋯

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

Its true continuous time derivative has the same literal spatial admissibility.

Equations

• G.vectorDerivativeForcing = EulerMeanPacketProvider.Forcing.ofOrbitPath G.derivativePath ⋯ ⋯

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

Pressure force, defined pointwise by pathRepresentative D.T G.pressureForcePath G.pressureForcePath_orbit (D.clamp z.1) z.2.1.

Equations

• G.pressureForce z = EulerMeanScalarPressure.pathRepresentative D.T G.pressureForcePath ⋯ (D.clamp z.1) z.2.1

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

The physical pressure gradient, rather than the unneeded scalar pressure value, is spatially L².

Equations

• G.pressureForceForcing = EulerMeanPacketProvider.Forcing.ofOrbitPath G.pressureForcePath ⋯ ⋯

theorem EulerMeanPacketProvider.meanSolve_admissible (D : Data) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) : Nonempty (Forcing D (meanSolve D raw).1)