feat: port Analysis.Convex.Integral (#4718)

Co-authored-by: Komyyy <pol_tta@outlook.jp>
leanprover-community · Jun 6, 2023 · ce2ed4a · ce2ed4a
1 parent a9359cb
commit ce2ed4a
Show file tree

Hide file tree

Showing 2 changed files with 370 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -512,6 +512,7 @@ import Mathlib.Analysis.Convex.Function
 import Mathlib.Analysis.Convex.Gauge
 import Mathlib.Analysis.Convex.Hull
 import Mathlib.Analysis.Convex.Independent
+import Mathlib.Analysis.Convex.Integral
 import Mathlib.Analysis.Convex.Jensen
 import Mathlib.Analysis.Convex.Join
 import Mathlib.Analysis.Convex.KreinMilman