theorem SobolevRegularity.sobolev_iff_derivatives_in_L2 {n : ℕ} (m : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : SobolevSpace.MemHs n (↑m) u ↔ SobolevSpace.AllDerivMemL2 n m u

For nonnegative integer order m, membership in the Sobolev space Hˢ(ℝⁿ) with s = m is equivalent to all distributional derivatives of order at most m being in L².