Even-order Sobolev membership from iterated Laplacians

Repeated use of the second-order Bessel identity recovers complete integer Sobolev regularity from physical L² Laplacian data.

theorem CKN.Leray.regularised_memSobolev_even_of_iterated_laplacian_L2 (k : ℕ) (D : TemperedDistribution Foundation.Parabolic.L2Vec3 ComplexVec3) (h : ∀ j ≤ k, TemperedDistribution.MemSobolev 0 2 (Laplacian.laplacian^[j] D)) : TemperedDistribution.MemSobolev (↑(2 * k)) 2 D

If all iterated distributional Laplacians through order k are represented by L² fields, then the original distribution lies in H²ᵏ.

theorem CKN.Leray.regularised_bessel_even_lift_of_iterated_laplacian_L2 (k : ℕ) (f : ↥ComplexVectorL2) (h : ∀ j ≤ k, ∃ (g : ↥ComplexVectorL2), Laplacian.laplacian^[j] (MeasureTheory.Lp.toTemperedDistribution f) = MeasureTheory.Lp.toTemperedDistribution g) : ∃ (v : BesselPotentialSpace Foundation.Parabolic.L2Vec3 ComplexVec3 (↑(2 * k)) 2), regularisedBesselSobolevToL2 ↑(2 * k) ⋯ v = f

L² representatives for all iterated Laplacians give an exact complete H²ᵏ lift of the original spatial field.