[Merged by Bors] - feat(Probability/Independence): add conditional independence

[RemyDegenne]

Define conditional independence of sigma-algebras, sets and functions. This is a special case of independence with respect to a kernel and a measure. Conditional independence is obtained by using the conditional expectation kernel condexpKernel.

---

The PR is huge, but most of it is a copy of Independence/Kernel.lean with a particular choice of kernel, and most lemmas are proved in one line.

The main new part is the section DefinitionsLemmas, which relates the kernel definition and the more usual definition of conditional independence with conditional expectations.

[sgouezel]

I seem to remember from an old discussion (on Zulip?) that this refactor may require at some point that the spaces should be standard Lebesgue spaces (which I am not really enthusiastic about if this can be avoided). Can you comment on that?

[RemyDegenne]

I opened a WIP PR for mathlib3 a while ago where I raised that question. I guess that's where you remember it from.

For unconditional independence this changes nothing. The constant kernel always exists and formulating the definition using it does not change the generality.

For conditional independence, using this definition means that we need the space to be Polish Borel, since that is what is needed for condexpKernel to be defined. We could use the explicit property μ⟦t1 ∩ t2 | m'⟧ =ᵐ[μ] μ⟦t1 | m'⟧ * μ⟦t2 | m'⟧ to define conditional independence more generally, but then most interesting properties would need the Polish Borel assumption (and for example as far as I can tell Kallenberg talks about conditional independence in this case only).

We could also have the more general property as the definition, and then have a lemma stating that it is equivalent to the kernel definition. But since I am unsure whether conditional independence is useful outside of the Polish Borel setting, I thought I might as well define it in the way that gave the most API directly.

[RemyDegenne]

In summary, this refactor can be cut into three steps:
A1) introduce the definition of independence with respect to a kernel and a measure #6106
A2) rephrase unconditional independence as a special case of (A1).
A3) introduce conditional independence, defined as a special case of (A1). This restricts conditional independence to Polish Borel spaces.

An alternative step (A3') would be to define conditional independence more generally using the conditional expectation, then add a lemma stating that in Polish Borel spaces it is a special case of (A1), and prove conditional independence properties in one generality or the other depending on the lemma.

Another way to proceed (B) would be to not define the generalized independence, not change anything to unconditional independence, and to simply add conditional independence with all its properties proved separately. That would be a lot of code duplication (or almost duplication).

(A) avoids code duplication entirely at the cost of some generality for conditional independence. (A') with step (A3') keeps the generality, as does (B). The relative merits of (A') and (B) depend on the proportion of properties that hold without the Polish Borel assumption. The prevalence of that assumption in references makes me think that (A)/(A') and in particular (A1) are a good idea (it looks like conditional independence has nice properties only when the conditional kernel exists), but I need to investigate more to be sure. Non-Polish spaces are not my usual use case :)

[sgouezel]

Let's get this in. Thanks! I haven't looked at everything in detail, since it is modelled on the other files, but it makes perfect sense.
bors d+

[sgouezel]

le sounds weird here, as it's just a subset. Since the same terminology is used in the other independence files, let's keep it like that and maybe fix it some other day.

[mathlib-bors]

✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[RemyDegenne]

Thanks for the review!
bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Check all files imported
• Build