English
Let E be a normed space. For every nonnegative radius r and every x ∈ E, the gauge of the ball of radius r around the origin evaluated at x is equal to the norm of x divided by r; in the special case r = 0 the value is 0.
Русский
Пусть E — нормированное пространство. Для любого r ≥ 0 и для каждого x ∈ E гейдж(ball(0, r)) в точке x равен ||x||/r; при r = 0 значение равно 0.
LaTeX
$$$$\mathrm{gauge}(\mathrm{ball}(0_E, r))\,x = \begin{cases}0, & r = 0\\[6pt] \dfrac{\|x\|}{r}, & r > 0\end{cases}$$$$
Lean4
theorem gauge_ball (hr : 0 ≤ r) (x : E) : gauge (ball (0 : E) r) x = ‖x‖ / r :=
by
rcases hr.eq_or_lt with rfl | hr
· simp
· rw [← smul_unitBall_of_pos hr, gauge_smul_left, Pi.smul_apply, gauge_unit_ball, smul_eq_mul, abs_of_nonneg hr.le,
div_eq_inv_mul]
simp_rw [mem_ball_zero_iff, norm_neg]
exact fun _ => id
