Classical divergence and pressure identities for the reconstructed mean fields.

theorem EulerMeanClassical.solenoidal_representative_divergence (u : ↥EulerMeanSolenoidal.L2) (hu : u ∈ EulerMeanSolenoidal.solenoidalSpace) (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (hrep : ↑↑u =ᵐ[MeasureTheory.volume] f) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence f x = 0

theorem EulerMeanClassical.representative_divergence (u : ↥EulerMeanSolenoidal.L2) (hu : u ∈ EulerMeanSolenoidal.solenoidalSpace) (hs : EulerMeanSmoothRepresentative.SmoothOrbit u) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence (EulerMeanSmoothRepresentative.representative u hs) x = 0

The actual smooth representative inherits the weak solenoidal constraint pointwise.

theorem EulerMeanClassical.representative_pressure (p : ↥EulerMeanSolenoidal.L2) (hp : p ∈ EulerMeanSolenoidal.gradientSpace) (hs : EulerMeanSmoothRepresentative.SmoothOrbit p) : ContDiff ℝ (↑⊤) (EulerCanonicalGraphPotential.radialPotential (EulerMeanSmoothRepresentative.representative p hs)) ∧ EulerCanonicalGraphPotential.radialPotential (EulerMeanSmoothRepresentative.representative p hs) 0 = 0 ∧ ∀ (x : EulerLiftedGradientSpace.Vector3), gradient (EulerCanonicalGraphPotential.radialPotential (EulerMeanSmoothRepresentative.representative p hs)) x = EulerMeanSmoothRepresentative.representative p hs x

A smooth translation orbit in the genuine gradient space has a normalized classical pressure.