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 <Remydegenne@gmail.com>

Author: RemyDegenne

Mathlib.lean

@@ -2661,6 +2661,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