feat: port Analysis.Convex.Gauge (#3942)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
leanprover-community · May 13, 2023 · b28404d · b28404d
1 parent fb165b6
commit b28404d
Show file tree

Hide file tree

Showing 2 changed files with 491 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -358,6 +358,7 @@ import Mathlib.Analysis.Convex.Exposed
 import Mathlib.Analysis.Convex.Extrema
 import Mathlib.Analysis.Convex.Extreme
 import Mathlib.Analysis.Convex.Function
+import Mathlib.Analysis.Convex.Gauge
 import Mathlib.Analysis.Convex.Hull
 import Mathlib.Analysis.Convex.Independent
 import Mathlib.Analysis.Convex.Jensen