feat(Probability/Independence): define independence wrt a kernel and …

…a measure (#6106) We introduce a new notion of independence with respect to a kernel and a measure. The plan is to eventually express both independence and conditional independence as particular cases of this new notion (see #6098). Two sigma-algebras `m` and `m'` are said to be independent with respect to a kernel `κ` and a measure `μ` if for all `m`-measurable sets `t₁` and `m'`-measurable sets `t₂`, `∀ᵐ a ∂μ, κ a (t₁ ∩ t₂) = κ a t₁ * κ a t₂`. Independence is the special case where `κ` is a constant kernel. Conditional independence can be defined by using the conditional expectation kernel `condexpKernel`. Co-authored-by: RemyDegenne <[email protected]>
leanprover-community · Aug 2, 2023 · 2fdc335 · 2fdc335
1 parent cf953a9
commit 2fdc335
Show file tree

Hide file tree

Showing 2 changed files with 917 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2663,6 +2663,7 @@ import Mathlib.Probability.ConditionalProbability
 import Mathlib.Probability.Density
 import Mathlib.Probability.IdentDistrib
 import Mathlib.Probability.Independence.Basic
+import Mathlib.Probability.Independence.Kernel
 import Mathlib.Probability.Independence.ZeroOne
 import Mathlib.Probability.Integration
 import Mathlib.Probability.Kernel.Basic