Continuity of positive truncation

For 1 ≤ p < ∞ and 0 ≤ k, the truncation u ↦ (u - k)⁺ is continuous in W^{1,p}(Ω) and preserves W^{1,p}_0(Ω). Neither assertion requires boundedness or boundary regularity of Ω.

Positive parts of functions with zero boundary values are therefore admissible Sobolev test functions. In particular, this applies to the difference of two functions with the same Dirichlet boundary data, as needed in weak comparison arguments.

• TauCeti.W1p.continuous_posPartAbove: continuity in the full Sobolev norm.
• TauCeti.W1p.posPartAbove_mem_w1p0Submodule: preservation of the homogeneous Dirichlet condition.

The corresponding positive-part results are the special case k = 0.

theorem TauCeti.W1p.continuous_posPartAbove {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) {k : ℝ} (hk : 0 ≤ k) : Continuous (posPartAbove hp hk)

Truncation above a nonnegative level is continuous in the Sobolev norm for finite exponents.

theorem TauCeti.W1p.continuous_posPart {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) : Continuous (posPart hp)

Taking the positive part is continuous in the Sobolev norm for finite exponents.

theorem TauCeti.W1p.posPartAbove_mem_w1p0Submodule {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) {k : ℝ} (hk : 0 ≤ k) {u : ↥(W1p mu Omega p)} (hu : u ∈ w1p0Submodule mu Omega p) : posPartAbove hp hk u ∈ w1p0Submodule mu Omega p

Truncation above a nonnegative level preserves the homogeneous Dirichlet boundary condition.

theorem TauCeti.W1p.posPart_mem_w1p0Submodule {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) {u : ↥(W1p mu Omega p)} (hu : u ∈ w1p0Submodule mu Omega p) : posPart hp u ∈ w1p0Submodule mu Omega p

Positive truncation preserves the homogeneous Dirichlet boundary condition.