Interior Sobolev embedding into Cʲ(Ω)

Let Ω be an open subset of a finite-dimensional real inner product space E of dimension n. If 2k > n, every u ∈ W^{k+j,2}(Ω) agrees almost everywhere on Ω with a function that is Cʲ on Ω. In particular, a function lying in W^{m,2}(Ω) for every m agrees almost everywhere on Ω with a function smooth on Ω. No boundedness or boundary regularity of Ω is assumed: the statements are interior ones, and the representative need not be bounded or extend continuously to the boundary.

Localization

Continuity is local. Near a point of Ω, multiply u by a smooth bump ζ equal to one near the point and supported in Ω; then ζ u ∈ W^{k,2}_0(Ω) (TauCeti.Wkp.exists_mem_wkp0Submodule_value_ae_eq_mul), its extension by zero lies in W^{k,2}(E), and the whole-space embedding W^{k,2}(E) → C₀(E) for 2k > n (TauCeti.Wkp.toZeroAtInfty) gives a continuous function equal to u almost everywhere near the point. The local continuous representatives glue to one on Ω (TauCeti.exists_contDiffOn_ae_eq_of_locally).

Derivatives

For u ∈ W^{k+j+1,2}(Ω), the weak derivatives ∂ᵢu along an orthonormal basis lie in W^{k+j,2}(Ω) (TauCeti.Wkp.exists_hasWeakLineDerivOn_value), so by induction they have Cʲ representatives. Assembled into a Cʲ field of linear maps, they form a weak derivative of the continuous representative of u, which is therefore Cʲ⁺¹ (TauCeti.HasWeakFDerivOn.contDiffOn_succ).

The statements are for Lebesgue measure volume, the measure of the whole-space embedding.

Main results

• TauCeti.Wkp.exists_continuousOn_ae_eq: W^{k,2}(Ω) ⊆ C(Ω) for 2k > n.
• TauCeti.Wkp.exists_contDiffOn_ae_eq: W^{k+j,2}(Ω) ⊆ Cʲ(Ω) for 2k > n.
• TauCeti.exists_contDiffOn_ae_eq_of_forall_wkp: a function in W^{m,2}(Ω) for every m has a representative smooth on Ω.

References

• L. C. Evans, Partial Differential Equations, 2nd ed., §5.6.3, Theorem 6, and its use in §6.3.1, Theorem 3 (infinite differentiability in the interior).
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Corollary 7.11.

theorem TauCeti.Wkp.exists_continuousOn_ae_eq {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {Omega : TopologicalSpace.Opens E} {k : ℕ} (hk : Module.finrank ℝ E < 2 * k) (u : Wkp MeasureTheory.volume Omega 2 k) : ∃ (g : E → ℝ), ContinuousOn g ↑Omega ∧ ↑↑(value k u) =ᵐ[MeasureTheory.volume.restrict ↑Omega] g

Interior Sobolev embedding into C(Ω). If 2k > dim E, every u ∈ W^{k,2}(Ω) agrees almost everywhere on Ω with a function continuous on Ω.

theorem TauCeti.Wkp.exists_contDiffOn_ae_eq {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {Omega : TopologicalSpace.Opens E} {k : ℕ} (hk : Module.finrank ℝ E < 2 * k) (j : ℕ) (u : Wkp MeasureTheory.volume Omega 2 (k + j)) : ∃ (g : E → ℝ), ContDiffOn ℝ (↑j) g ↑Omega ∧ ↑↑(value (k + j) u) =ᵐ[MeasureTheory.volume.restrict ↑Omega] g

Interior Sobolev embedding into Cʲ(Ω). If 2k > dim E, every u ∈ W^{k+j,2}(Ω) agrees almost everywhere on Ω with a function that is Cʲ on Ω.

theorem TauCeti.exists_contDiffOn_ae_eq_of_forall_wkp {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {Omega : TopologicalSpace.Opens E} {u : E → ℝ} (h : ∀ (m : ℕ), ∃ (w : Wkp MeasureTheory.volume Omega 2 m), ↑↑(Wkp.value m w) =ᵐ[MeasureTheory.volume.restrict ↑Omega] u) : ∃ (g : E → ℝ), ContDiffOn ℝ (↑⊤) g ↑Omega ∧ u =ᵐ[MeasureTheory.volume.restrict ↑Omega] g

Smoothness from all Sobolev orders. A function that agrees almost everywhere on Ω with an element of W^{m,2}(Ω) for every m agrees almost everywhere on Ω with a function smooth on Ω.