gauge_closedBall — Mathlib

English

For r ≥ 0 and x ∈ E, the gauge of the closed ball of radius r around the origin at x equals ||x||/r; in particular the r = 0 case yields 0.

Русский

Пусть r ≥ 0 и x ∈ E. Гейдж закрытого шара радиуса r в точке x равен ||x||/r; в случае r = 0 значение равно 0.

LaTeX

$$$$ gauge(\mathrm{closedBall}(0_E, r))\,x = \begin{cases}0, & r = 0\\[6pt] \dfrac{\|x\|}{r}, & r > 0\end{cases} $$$$

Lean4

@[simp]
theorem gauge_closedBall (hr : 0 ≤ r) (x : E) : gauge (closedBall (0 : E) r) x = ‖x‖ / r :=
  by
  rcases hr.eq_or_lt with rfl | hr'
  · rw [div_zero, closedBall_zero', singleton_zero, gauge_closure_zero]; rfl
  · apply le_antisymm
    · rw [← gauge_ball hr]
      exact gauge_mono (absorbent_ball_zero hr') ball_subset_closedBall x
    · suffices ∀ᶠ R in 𝓝[>] r, ‖x‖ / R ≤ gauge (closedBall 0 r) x
        by
        refine le_of_tendsto ?_ this
        exact tendsto_const_nhds.div inf_le_left hr'.ne'
      filter_upwards [self_mem_nhdsWithin] with R hR
      rw [← gauge_ball (hr.trans hR.out.le)]
      refine gauge_mono ?_ (closedBall_subset_ball hR) _
      exact (absorbent_ball_zero hr').mono ball_subset_closedBall

Похожие утверждения