Sobolev promotion through the Laplacian

The second-order Bessel identity promotes a field by two Sobolev orders when both the field and its distributional Laplacian have the lower order.

theorem CKN.Leray.regularised_memSobolev_add_two_of_laplacian (s : ℝ) (D : TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3) (hD : TemperedDistribution.MemSobolev s 2 D) (hΔ : TemperedDistribution.MemSobolev s 2 (Laplacian.laplacian D)) : TemperedDistribution.MemSobolev (s + 2) 2 D

A field and its distributional Laplacian in Hˢ give the field in Hˢ⁺².