mathlib

5ebb7d87 - feat(analysis/convex/gauge): unit ball of the gauge seminorm (#16413)