Uniqueness of the force pressure

An L⁶ function on ℝ³ with zero weak gradient vanishes almost everywhere: its mollifications are constant, a constant in L⁶(ℝ³) is zero, and the mollifications converge in L⁶. Hence two L⁶ functions with the same weak gradient agree almost everywhere, which is the uniqueness statement of lem:force-pressure.

theorem CKN.Leray.ae_eq_zero_of_memLp_six_of_hasWeakGradientOn_zero {q : Foundation.Parabolic.Vec3 → ℝ} (hq : MeasureTheory.MemLp q 6 MeasureTheory.volume) (hgrad : HasWeakGradientOn Set.univ q fun (x : Vec 3) => 0) : q =ᵐ[MeasureTheory.volume] 0

An L⁶ function on ℝ³ whose weak gradient vanishes is zero almost everywhere.

theorem CKN.Leray.ae_eq_of_memLp_six_of_hasWeakGradientOn {p₁ p₂ : Foundation.Parabolic.Vec3 → ℝ} {G : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (h₁ : MeasureTheory.MemLp p₁ 6 MeasureTheory.volume) (h₂ : MeasureTheory.MemLp p₂ 6 MeasureTheory.volume) (hG₁ : HasWeakGradientOn Set.univ p₁ G) (hG₂ : HasWeakGradientOn Set.univ p₂ G) : p₁ =ᵐ[MeasureTheory.volume] p₂

The uniqueness statement of lem:force-pressure: two L⁶ functions on ℝ³ with the same weak gradient agree almost everywhere.