sSup_sphere_eq_norm — Mathlib

English

If the domain is a real normed space, the supremum of the real norms ‖f x‖ over the unit sphere equals the real operator norm ‖f‖.

Русский

Если область определения — вещественное нормированное пространство, то супремум по ‖f x‖ на единичной сфере равен ‖f‖.

LaTeX

$$$\\forall f: E \\to SL[σ_{12}] F\\, [NormedAlgebra \\mathbb{R} 𝕜]\\; sSup\\big(\\{\\|f x\\| : x\\in S\\} \\big) = \\|f\\|.$$$

Lean4

/-- When the domain is a real normed space, `ContinuousLinearMap.sSup_unitClosedBall_eq_norm` can be
tightened to take the supremum over only the `Metric.sphere`. -/
theorem sSup_sphere_eq_norm [NormedAlgebra ℝ 𝕜] (f : E →SL[σ₁₂] F) :
    sSup ((fun x => ‖f x‖) '' Metric.sphere 0 1) = ‖f‖ := by
  simpa only [NNReal.coe_sSup, Set.image_image] using NNReal.coe_inj.2 f.sSup_sphere_eq_nnnorm

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