feat: port Analysis.SpecialFunctions.Gaussian (#5370)

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

Hide file tree

Showing 2 changed files with 635 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -722,6 +722,7 @@ import Mathlib.Analysis.SpecialFunctions.Exp
 import Mathlib.Analysis.SpecialFunctions.ExpDeriv
 import Mathlib.Analysis.SpecialFunctions.Exponential
 import Mathlib.Analysis.SpecialFunctions.Gamma.Basic
+import Mathlib.Analysis.SpecialFunctions.Gaussian
 import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
 import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.Analysis.SpecialFunctions.JapaneseBracket