Sobolev functions vanishing continuously on the boundary

Let Ω be a bounded open set and 1 ≤ p < ∞. A function u ∈ W^{1,p}(Ω) that agrees almost everywhere on Ω with a function g continuous on the closure of Ω and zero on its frontier lies in W^{1,p}_0(Ω). So for a function continuous up to the boundary, the classical boundary condition u = 0 on ∂Ω implies the Sobolev one, with no regularity of ∂Ω assumed.

The proof truncates. For k > 0 the truncation (u - k)⁺ vanishes outside the compact set {x ∈ closure Ω | g x ≥ k}, which lies inside Ω because g vanishes on the frontier, so it belongs to W^{1,p}_0(Ω). As k → 0 it tends to u⁺ in W^{1,p}(Ω): on a domain of finite measure (u - k)⁺ is the positive part of u - k, and taking positive parts is continuous on W^{1,p}(Ω) (TauCeti.W1p.continuous_posPart). The same argument applied to -u handles u⁻.

Main declarations

• TauCeti.exists_isCompact_inter_preimage_Ici_subset_subset: the superlevel sets {x ∈ Ω | k ≤ g x}, k > 0, of a function vanishing on the frontier lie in a compact subset of Ω.
• TauCeti.W1p.mem_w1p0Submodule_of_continuousOn_closure: a Sobolev function on a bounded domain that agrees with a function continuous on the closure and vanishing on the frontier lies in W^{1,p}_0(Ω).

References

• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Section 7.4 (truncations of Sobolev functions) and Section 7.5 (the spaces W^{k,p}_0).

theorem TauCeti.exists_isCompact_inter_preimage_Ici_subset_subset {X : Type u_2} [MetricSpace X] [ProperSpace X] {U : Set X} (hb : Bornology.IsBounded U) {g : X → ℝ} (hg : ContinuousOn g (closure U)) (hg0 : ∀ x ∈ frontier U, g x = 0) {k : ℝ} (hk : 0 < k) : ∃ (K : Set X), IsCompact K ∧ U ∩ g ⁻¹' Set.Ici k ⊆ K ∧ K ⊆ U

Superlevel sets stay away from the boundary. Let g be continuous on the closure of a bounded set U of a proper metric space and zero on its frontier. For every k > 0 the points of U where k ≤ g lie in a compact subset of U, namely closure U ∩ g ⁻¹' Ici k.

theorem TauCeti.W1p.mem_w1p0Submodule_of_continuousOn_closure {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (hb : Bornology.IsBounded ↑Omega) {g : E → ℝ} (hg : ContinuousOn g (closure ↑Omega)) (hg0 : ∀ x ∈ frontier ↑Omega, g x = 0) {u : ↥(W1p mu Omega p)} (hu : ↑↑(value u) =ᵐ[mu.restrict ↑Omega] g) : u ∈ w1p0Submodule mu Omega p

A Sobolev function vanishing continuously on the boundary lies in W^{1,p}_0(Ω). Let Ω be bounded and 1 ≤ p < ∞. If u ∈ W^{1,p}(Ω) agrees almost everywhere on Ω with a function g that is continuous on closure Ω and zero on frontier Ω, then u ∈ W^{1,p}_0(Ω). No regularity of the boundary is assumed.