theorem SobolevEmbedding.sobolevSpace_toFun_continuous {n m : ℕ} (hm : n < 2 * m) (u : SobolevSpace n m) : Continuous u.toFun

Sobolev embedding (continuity): for n < 2m, every element of SobolevSpace n m is represented by a continuous function.

theorem SobolevEmbedding.sobolevSpace_toFun_zeroAtInfty {n m : ℕ} (hm : n < 2 * m) (u : SobolevSpace n m) : Filter.Tendsto u.toFun (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)

Sobolev embedding (decay at infinity): for n < 2m, every element of SobolevSpace n m is represented by a function tending to 0 along the cocompact filter.

theorem SobolevEmbedding.sobolevSpace_contDiff {n m k : ℕ} (hkm : k ≤ m) (hm : n < 2 * (m - k)) (u : SobolevSpace n m) : ContDiff ℝ (↑↑k) u.toFun

Sobolev embedding (higher regularity): for k ≤ m and n < 2(m - k), every element of SobolevSpace n m is C^k smooth.

noncomputable def SobolevEmbedding.SobolevSpace.deriv {n m : ℕ} (u : SobolevSpace n m) (j : ℕ) (hj : j ≤ m) (v : Fin j → EuclideanSpace ℝ (Fin n)) : { w : SobolevSpace n (m - j) // w.toFun = fun (x : EuclideanSpace ℝ (Fin n)) => (iteratedFDeriv ℝ j u.toFun x) v }

The j-th weak derivative of an element of SobolevSpace n m (for j ≤ m) is itself an element of SobolevSpace n (m - j), represented pointwise by the iterated Fréchet derivative of the underlying function.

theorem SobolevEmbedding.sobolevSpace_iteratedFDeriv_norm_tendsto_zero {n m : ℕ} (u : SobolevSpace n m) (j : ℕ) (hj : j ≤ m) (hm : n < 2 * (m - j)) : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ‖iteratedFDeriv ℝ j u.toFun x‖) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)

Sobolev embedding (decay of higher derivatives): for j ≤ m with n < 2(m - j), the norm of the j-th iterated derivative of any element of SobolevSpace n m tends to 0 at infinity.

def SobolevEmbedding.sobolevEmbeddingFix {n m k : ℕ} (hkm : k ≤ m) (hm : n < 2 * (m - k)) (u : SobolevSpace n m) : TestFunctions.ContDiffZeroAtInftyN n k

Combined Sobolev embedding: under k ≤ m and n < 2(m - k), any u ∈ SobolevSpace n m gives rise to an element of TestFunctions.ContDiffZeroAtInftyN n k, that is, a C^k function with all derivatives of order ≤ k vanishing at infinity. This is the concrete embedding asserted by Theorem 10.1 of Melrose.