Lipschitz maps vanishing on a hyperplane

A Lipschitz map that vanishes on the affine hyperplane {f = a} of a real normed space is bounded by a multiple of |f x - a|: moving from x along a vector v with f v = 1 reaches the hyperplane after a displacement of norm |f x - a| ‖v‖. The functional f only needs to be linear, not continuous.

Main results

• LipschitzWith.norm_le_mul_abs_sub_of_eq_zero: if g is K-Lipschitz, vanishes on {f = a}, and f v = 1, then ‖g x‖ ≤ K ‖v‖ |f x - a|.

theorem LipschitzWith.norm_le_mul_abs_sub_of_eq_zero {E : Type u_1} {F : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [SeminormedAddCommGroup F] {K : NNReal} {g : E → F} (hg : LipschitzWith K g) {f : E →ₗ[ℝ] ℝ} {v : E} (hv : f v = 1) {a : ℝ} (hg0 : ∀ (x : E), f x = a → g x = 0) (x : E) : ‖g x‖ ≤ ↑K * ‖v‖ * |f x - a|

A Lipschitz map vanishing on a hyperplane is O (|f x - a|). If g is K-Lipschitz and vanishes on the hyperplane {f = a} of a linear functional f, then ‖g x‖ ≤ K ‖v‖ |f x - a| for every v with f v = 1.