Weak gradients on level sets

For 1 ≤ p < ∞, the weak gradient of a Sobolev function vanishes almost everywhere on each of its level sets. Consequently, the weak gradients of two Sobolev functions agree almost everywhere on the set where their values agree.

The level may be any real number, including on domains of infinite measure. These locality statements apply to measurable level sets, which need not contain any open set. They remove the ambiguity of truncation gradients at a threshold and support continuity of positive truncation in the Sobolev norm.

theorem TauCeti.W1p.gradient_ae_eq_zero_on_level_set {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 ≠ ⊤) (u : ↥(W1p mu Omega p)) (k : ℝ) : ∀ᵐ (x : E) ∂mu.restrict ↑Omega, ↑↑(value u) x = k → ↑↑(gradient u) x = 0

The weak gradient vanishes almost everywhere on every level set, for 1 ≤ p < ∞. The level may be any real number, even when Ω has infinite measure.

theorem TauCeti.W1p.gradient_ae_eq_on_eq {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 ≠ ⊤) (u v : ↥(W1p mu Omega p)) : ∀ᵐ (x : E) ∂mu.restrict ↑Omega, ↑↑(value u) x = ↑↑(value v) x → ↑↑(gradient u) x = ↑↑(gradient v) x

Weak gradients agree almost everywhere wherever the values agree, even if their coincidence set has empty interior.