Classical lifted divergence zero implies membership in the actual closed L² constraint space.

theorem EulerCylinderClassicalSolenoidal.mem_of_test_integral (P : ℝ) [Fact (0 < P)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) (h : ∀ (φ : EulerLiftedGradientSpace.LiftDomain P → ℝ), (HasCompactSupport φ ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerLiftedGradientSpace.localLift P φ x)) → ∫ (x : EulerLiftedGradientSpace.LiftDomain P), inner ℝ (EulerLiftedGradientSpace.liftedGradient P κ m φ x) (↑↑u x) ∂EulerLiftedGradientSpace.liftMeasure P = 0) : u ∈ EulerLiftedGradientSpace.divergenceFreeSpace P κ m

theorem EulerCylinderClassicalSolenoidal.mem_of_classical (P : ℝ) [Fact (0 < P)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerLiftedGradientSpace.LiftL2 P)) (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hrep : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) (hdiv : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ∑ i : Fin 3, (EulerTransportDerivatives.fieldDerivative P (EulerMetricTransport.coordinateDirection κ m i) f x).ofLp i = 0) : u ∈ EulerLiftedGradientSpace.divergenceFreeSpace P κ m