A normalized defining function for a regular superlevel set

Let u be a smooth compactly supported real function on a real inner product space and let t > 0 be a regular value of u. Then w = (u - t) / √(‖∇u‖² + (u - t)²) is a smooth defining function of the superlevel set {u > t}: it is positive exactly on {u > t}, equal to -1 off the support of u (so {w ≥ -1/2} is compact), and its derivative has norm one on its zero level {u = t} (ContDiff.exists_contDiff_setOf_pos_eq_setOf_lt).

Such a normalization lets estimates near the boundary of {u > t} be stated uniformly in terms of ‖Dw‖, which is close to one in a neighbourhood of the zero level.

theorem ContDiff.exists_contDiff_setOf_pos_eq_setOf_lt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {u : E → ℝ} (hu : ContDiff ℝ (↑⊤) u) (huc : HasCompactSupport u) {t : ℝ} (ht : 0 < t) (hreg : ∀ (x : E), u x = t → fderiv ℝ u x ≠ 0) : ∃ (w : E → ℝ), ContDiff ℝ (↑⊤) w ∧ IsCompact {x : E | -(1 / 2) ≤ w x} ∧ (∀ (x : E), w x = 0 → ‖fderiv ℝ w x‖ = 1) ∧ {x : E | 0 < w x} = {x : E | t < u x}

A normalized defining function for a regular superlevel set. Let u be smooth and compactly supported, and let t > 0 be a regular value of u. Then w = (u - t) / √(‖∇u‖² + (u - t)²) is smooth, positive exactly on {u > t}, equal to -1 off the support of u, and its derivative has norm one on its zero level {u = t}.