English
If the domain is a real normed space, the supremum of the nonnegative norms ‖f x‖₊ over the unit sphere is equal to ‖f‖₊.
Русский
Если область определения — вещественное нормированное пространство, то супремум по ‖f x‖₊ на единичной сфере равен ‖f‖₊.
LaTeX
$$$\\forall f: E \\to SL[σ_{12}] F\\, [NormedAlgebra \\mathbb{R} 𝕜]\\; sSup\\big(\\{\\|f x\\|_+ : x \\in S\\} \\big) = \\|f\\|_+,$ где $S$ — сфера $\\|x\\|=1$.$$
Lean4
/-- When the domain is a real normed space, `ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm` can
be tightened to take the supremum over only the `Metric.sphere`. -/
theorem sSup_sphere_eq_nnnorm [NormedAlgebra ℝ 𝕜] (f : E →SL[σ₁₂] F) :
sSup ((fun x => ‖f x‖₊) '' Metric.sphere 0 1) = ‖f‖₊ :=
by
cases subsingleton_or_nontrivial E
· simp [sphere_eq_empty_of_subsingleton one_ne_zero]
have : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
refine
csSup_eq_of_forall_le_of_forall_lt_exists_gt ((NormedSpace.sphere_nonempty.mpr zero_le_one).image _) ?_
fun ub hub => ?_
· rintro - ⟨x, hx, rfl⟩
simpa only [mul_one] using f.le_opNorm_of_le (mem_sphere_zero_iff_norm.1 hx).le
· obtain ⟨x, hx, hxf⟩ := f.exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm hub
exact ⟨_, ⟨x, by simpa using congrArg NNReal.toReal hx, rfl⟩, hxf⟩
