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

Estimated changes