Liouville theorem for a curl-free L^3 field

This file proves lem:liouville-L3 from the weak harmonic Liouville estimate.

theorem ESS.liouvilleL3 {v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hv : MeasureTheory.MemLp v (ENNReal.ofReal 3) MeasureTheory.volume) (hdiv : CKN.DistributionalDivergenceFree v) (hcurl : ∀ (i j : Fin 3) (φ : CKN.Foundation.Parabolic.Vec3 → ℝ), CKN.SmoothCompactTest φ → ∫ (x : CKN.Foundation.Parabolic.Vec3), v x i * CKN.spatialDeriv φ j x - v x j * CKN.spatialDeriv φ i x = 0) : v =ᵐ[MeasureTheory.volume] 0

A distributionally divergence-free and curl-free L^3 vector field on all of space vanishes almost everywhere, as in lem:liouville-L3.