English
For a continuous linear map f, the operator norm is zero if and only if f is the zero map.
Русский
Для непрерывно линейного отображения f операторная норма равна нулю тогда и только тогда, когда f тождественно ноль.
LaTeX
$$$\\|f\\| = 0 \\quad\\Leftrightarrow\\quad f = 0.$$$
Lean4
/-- `LinearMap.bound_of_ball_bound'` is a version of this lemma over a field satisfying `RCLike`
that produces a concrete bound.
-/
theorem bound_of_ball_bound {r : ℝ} (r_pos : 0 < r) (c : ℝ) (f : E →ₗ[𝕜] Fₗ)
(h : ∀ z ∈ Metric.ball (0 : E) r, ‖f z‖ ≤ c) : ∃ C, ∀ z : E, ‖f z‖ ≤ C * ‖z‖ :=
by
obtain ⟨k, hk⟩ := @NontriviallyNormedField.non_trivial 𝕜 _
use c * (‖k‖ / r)
intro z
refine bound_of_shell _ r_pos hk (fun x hko hxo => ?_) _
calc
‖f x‖ ≤ c := h _ (mem_ball_zero_iff.mpr hxo)
_ ≤ c * (‖x‖ * ‖k‖ / r) := (le_mul_of_one_le_right ?_ ?_)
_ = _ := by ring
· exact le_trans (norm_nonneg _) (h 0 (by simp [r_pos]))
· rw [div_le_iff₀ (zero_lt_one.trans hk)] at hko
exact (one_le_div r_pos).mpr hko
