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

leanprover-community · Jun 22, 2023 · 6f4b4c0 · 6f4b4c0
1 parent 1e6d45e
commit 6f4b4c0
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