A canonically normalized actual scalar potential for ordinary mean pressure gradients.

theorem EulerMeanPressure.symmetry_of_coordinates (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hL : ∀ (i j : Fin 3), (L (EuclideanSpace.single i 1)).ofLp j = (L (EuclideanSpace.single j 1)).ofLp i) (a b : EulerSmoothLimit.Space) : inner ℝ (L a) b = inner ℝ (L b) a

theorem EulerMeanPressure.gradientSpace_has_potential (p : ↥EulerMeanSolenoidal.L2) (hp : p ∈ EulerMeanSolenoidal.gradientSpace) (g : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hrep : ↑↑p =ᵐ[MeasureTheory.volume] g) (hg : ContDiff ℝ (↑⊤) g) : ∃ (q : EulerSmoothLimit.Space → ℝ), ContDiff ℝ (↑⊤) q ∧ ∀ (x : EulerSmoothLimit.Space), gradient q x = g x

Smooth representatives of the actual closed gradient space have a genuine scalar potential.

theorem EulerMeanPressure.gradientSpace_radial_potential (p : ↥EulerMeanSolenoidal.L2) (hp : p ∈ EulerMeanSolenoidal.gradientSpace) (g : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hrep : ↑↑p =ᵐ[MeasureTheory.volume] g) (hg : ContDiff ℝ (↑⊤) g) : ContDiff ℝ (↑⊤) (EulerCanonicalGraphPotential.radialPotential g) ∧ EulerCanonicalGraphPotential.radialPotential g 0 = 0 ∧ ∀ (x : EulerLiftedGradientSpace.Vector3), gradient (EulerCanonicalGraphPotential.radialPotential g) x = g x

The concrete radial integral gives a fixed additive normalization, not just an existential pressure.

theorem EulerMeanPressure.weighted_pressure_has_potential (F FT : EulerMeanCoefficients.Field) (hFT : ∀ (x : EulerSmoothLimit.Space), FT x = ContinuousLinearMap.adjoint (F x)) (r : ↥EulerMeanSolenoidal.L2) (hr : (ContinuousLinearMap.adjoint (EulerMeanCoefficients.multiplier F)) r ∈ EulerMeanSolenoidal.gradientSpace) (g : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hrep : ↑↑r =ᵐ[MeasureTheory.volume] g) (hg : ContDiff ℝ ↑⊤ fun (x : EulerSmoothLimit.Space) => (ContinuousLinearMap.adjoint (F x)) (g x)) : ContDiff ℝ (↑⊤) (EulerCanonicalGraphPotential.radialPotential fun (x : EulerLiftedGradientSpace.Vector3) => (ContinuousLinearMap.adjoint (F x)) (g x)) ∧ EulerCanonicalGraphPotential.radialPotential (fun (x : EulerLiftedGradientSpace.Vector3) => (ContinuousLinearMap.adjoint (F x)) (g x)) 0 = 0 ∧ ∀ (x : EulerLiftedGradientSpace.Vector3), gradient (EulerCanonicalGraphPotential.radialPotential fun (x : EulerLiftedGradientSpace.Vector3) => (ContinuousLinearMap.adjoint (F x)) (g x)) x = (ContinuousLinearMap.adjoint (F x)) (g x)

An F-adjoint pressure residual is the actual pullback of a scalar gradient.