The ordinary closed L² gradient space has zero distributional curl. For smooth representatives this gives actual pointwise symmetry of the derivative.

theorem EulerMeanPressure.scalar_test_ibp (f ψ : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hψ : ContDiff ℝ (↑⊤) ψ) (hc : HasCompactSupport ψ) (i : Fin 3) : ∫ (x : EulerSmoothLimit.Space), EulerVectorCalculus.partialDerivative f i x * ψ x = -∫ (x : EulerSmoothLimit.Space), f x * EulerVectorCalculus.partialDerivative ψ i x

noncomputable def EulerMeanPressure.skewTest (i j : Fin 3) (ψ : EulerSmoothLimit.Space → ℝ) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Skew test, given by partialDerivative ψ j x • EuclideanSpace.single i 1 - partialDerivative ψ i x • EuclideanSpace.single j 1.

Equations

• EulerMeanPressure.skewTest i j ψ x = EulerVectorCalculus.partialDerivative ψ j x • EuclideanSpace.single i 1 - EulerVectorCalculus.partialDerivative ψ i x • EuclideanSpace.single j 1

theorem EulerMeanPressure.skewTest_smooth (i j : Fin 3) (ψ : EulerSmoothLimit.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) : ContDiff ℝ (↑⊤) (skewTest i j ψ)

theorem EulerMeanPressure.skewTest_compact (i j : Fin 3) (ψ : EulerSmoothLimit.Space → ℝ) (hc : HasCompactSupport ψ) : HasCompactSupport (skewTest i j ψ)

theorem EulerMeanPressure.skewTest_inner (i j : Fin 3) (ψ : EulerSmoothLimit.Space → ℝ) (x v : EulerSmoothLimit.Space) : inner ℝ v (skewTest i j ψ x) = v.ofLp i * EulerVectorCalculus.partialDerivative ψ j x - v.ofLp j * EulerVectorCalculus.partialDerivative ψ i x

theorem EulerMeanPressure.gradient_coordinate (φ : EulerSmoothLimit.Space → ℝ) (x : EulerSmoothLimit.Space) (i : Fin 3) : (gradient φ x).ofLp i = EulerVectorCalculus.partialDerivative φ i x

theorem EulerMeanPressure.gradient_skewTest_integral (i j : Fin 3) (φ ψ : EulerSmoothLimit.Space → ℝ) (hφ : ContDiff ℝ (↑⊤) φ) (hψ : ContDiff ℝ (↑⊤) ψ) (hc : HasCompactSupport ψ) : ∫ (x : EulerSmoothLimit.Space), inner ℝ (gradient φ x) (skewTest i j ψ x) = 0

noncomputable def EulerMeanPressure.skewTestLp (i j : Fin 3) (ψ : EulerSmoothLimit.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hc : HasCompactSupport ψ) : ↥EulerMeanSolenoidal.L2

Skew test Lᵖ, given by ((skewTest_smooth i j ψ hψ).continuous.memLp_of_hasCompactSupport (skewTest_compact i j ψ hc)).toLp (skewTest i j ψ).

Equations

• EulerMeanPressure.skewTestLp i j ψ hψ hc = MeasureTheory.MemLp.toLp (EulerMeanPressure.skewTest i j ψ) ⋯

theorem EulerMeanPressure.skewTestLp_ae (i j : Fin 3) (ψ : EulerSmoothLimit.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hc : HasCompactSupport ψ) : ↑↑(skewTestLp i j ψ hψ hc) =ᵐ[MeasureTheory.volume] skewTest i j ψ

theorem EulerMeanPressure.skewTestLp_solenoidal (i j : Fin 3) (ψ : EulerSmoothLimit.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hc : HasCompactSupport ψ) : skewTestLp i j ψ hψ hc ∈ EulerMeanSolenoidal.solenoidalSpace

theorem EulerMeanPressure.gradientSpace_weak_curl_zero (p : ↥EulerMeanSolenoidal.L2) (hp : p ∈ EulerMeanSolenoidal.gradientSpace) (i j : Fin 3) (ψ : EulerSmoothLimit.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hc : HasCompactSupport ψ) : ∫ (x : EulerSmoothLimit.Space), (↑↑p x).ofLp i * EulerVectorCalculus.partialDerivative ψ j x - (↑↑p x).ofLp j * EulerVectorCalculus.partialDerivative ψ i x = 0

theorem EulerMeanPressure.gradientSpace_classical_curl_zero (p : ↥EulerMeanSolenoidal.L2) (hp : p ∈ EulerMeanSolenoidal.gradientSpace) (g : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hrep : ↑↑p =ᵐ[MeasureTheory.volume] g) (hg : ContDiff ℝ (↑⊤) g) (x : EulerSmoothLimit.Space) (i j : Fin 3) : ((fderiv ℝ g x) (EuclideanSpace.single i 1)).ofLp j = ((fderiv ℝ g x) (EuclideanSpace.single j 1)).ofLp i

The distributional statement becomes the actual classical closedness identity.