feat: port Probability.Kernel.CondDistrib (#5293)

leanprover-community · Jun 21, 2023 · b8eff30 · b8eff30
1 parent 712f6d7
commit b8eff30
Show file tree

Hide file tree

Showing 2 changed files with 323 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2454,6 +2454,7 @@ import Mathlib.Probability.Integration
 import Mathlib.Probability.Kernel.Basic
 import Mathlib.Probability.Kernel.Composition
 import Mathlib.Probability.Kernel.CondCdf
+import Mathlib.Probability.Kernel.CondDistrib
 import Mathlib.Probability.Kernel.Disintegration
 import Mathlib.Probability.Kernel.IntegralCompProd
 import Mathlib.Probability.Kernel.Invariance