Commit 2025-08-05 22:50 2530d06a
View on Github →feat(Analysis/NormedSpace/OperatorNorm): characterize the operator norm via sphere 0 1
(#27912)
Namely that sSup ((fun x => ‖f x‖₊) '' Metric.sphere 0 1) = ‖f‖₊
, which we previously had for ball
and closedBall
.
From lean-matrix-cookbook