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

Sobolev embedding (continuity, alternate form): for n < 2m, every Sobolev space element in SobolevSpace n m admits a continuous representative.

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 (vanishing at infinity, alternate form): for n < 2m, elements of SobolevSpace n m vanish at infinity.

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 (smoothness, alternate form): for k ≤ m and n < 2(m - k), elements of SobolevSpace n m are C^k.

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)

Decay of j-th order derivatives for Sobolev functions: 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.sobolevEmbeddingThm {n m k : ℕ} (hkm : k ≤ m) (hm : n < 2 * (m - k)) (u : SobolevSpace n m) : TestFunctions.ContDiffZeroAtInftyN n k

Sobolev embedding theorem (Theorem 10.1 of Melrose): under k ≤ m and n < 2(m - k), every element of SobolevSpace n m is canonically a ContDiffZeroAtInftyN n k test function, i.e. a C^k function with all derivatives of order ≤ k vanishing at infinity.

@[simp]

theorem SobolevEmbedding.sobolevEmbeddingThm_toFun {n m k : ℕ} (hkm : k ≤ m) (hm : n < 2 * (m - k)) (u : SobolevSpace n m) : ⇑(sobolevEmbeddingThm hkm hm u).toZeroAtInftyContinuousMap = u.toFun

The underlying function of sobolevEmbeddingThm hkm hm u is the same as the underlying function of u.