LevelSets

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Vanishing of the gradient on level sets

grad_ae_zero_on_level_set, derived from the positive-part truncation applied to u at c and to −u at −c. Stated on IsOpenBoundedConvexDomain U.

theorem HCPolySupport.grad_ae_zero_on_level_set {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (u : H1Function U) (c : ℝ) : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U, u.toFun x = c → u.grad x = 0

Vanishing of the gradient on level sets. For u ∈ H¹(U) the weak gradient vanishes almost everywhere on the level set {u = c}.

Proof: (u−c)₊ − (c−u)₊ = u − c, so the difference v₁ − v₂ of the two D1 truncations has the same weak gradient as u (constant shift is H¹-trivial), while pointwise on {u = c} both truncation gradients vanish.