English
For a continuous linear map f, the supremum of the nonnegative norms ‖f x‖₊ over the closed unit ball equals the nnreal operator norm ‖f‖₊.
Русский
Пусть f — непрерывно линейное отображение. Тогда супремум по неотрицательным значениям ‖f x‖₊ на замкнутом единичном шаре равен nn-операторной норме ‖f‖₊.
LaTeX
$$$\\forall f: E \\to SL[\\sigma_{12}] F,\\ sSup\\big(\\{\\|f x\\|_+ : \\|x\\|_≤ 1\\}\\big) = \\|f\\|_+.$$$
Lean4
theorem sSup_unitClosedBall_eq_nnnorm (f : E →SL[σ₁₂] F) : sSup ((fun x => ‖f x‖₊) '' closedBall 0 1) = ‖f‖₊ :=
by
have hbdd : ∀ y ∈ (fun x => ‖f x‖₊) '' closedBall 0 1, y ≤ ‖f‖₊ :=
by
rintro - ⟨x, hx, rfl⟩
exact f.unit_le_opNorm x (mem_closedBall_zero_iff.1 hx)
refine le_antisymm (csSup_le ((nonempty_closedBall.mpr zero_le_one).image _) hbdd) ?_
rw [← sSup_unit_ball_eq_nnnorm]
gcongr
exacts [⟨‖f‖₊, hbdd⟩, ball_subset_closedBall]
