Conditional Independence for Not Standard Borel Spaces

Stream: mathlib4

[David Ledvinka]

I noticed that the current definition of conditional independence requires Ω is a standard Borel space. On the one hand I can't think (off the top of my head) any reasonable example of a not standard Borel examples that we care about in practice. On the other hand this is not a common assumption in say the (general state space) Markov chain literature (see for example Meyn and Tweedie) since it is giving up generality unnecessarily (at least in paper math). Was it discussed and decided that we don't care about such generality? Or could we generalize the definition?

[Yaël Dillies]

@Kalle Kytölä and I similarly generalised docs#MeasureTheory.condExp to avoid assuming standard Borel in the theory of Gibbs measures

[Kalle Kytölä]

And indeed our rationale in the case that Yaël Dillies mentions was very similar to what @David Ledvinka said above.

I.e., I cannot think of concrete applications where the spaces would not be standard Borel, but when developing some general theory (whether for Markov processes or Gibbs measures), making this specific assumption about the spaces did not seem natural --- instead just assuming we are given the necessary kernels (whose existence can be guaranteed for example by the standard Borel space assumptions) seemed the natural way to go. Unfortunately this is a while ago, so I don't remember anymore if we landed on a particularly clear design... But at least in principle I agree with David's sentiment.

[Rémy Degenne]

The standard Borel assumption in the Mathlib material could be replaced by the existence of conditional probabilities (standard Borel is there only to be able to use ProbabilityTheory.condExpKernel). And in a book about Markov chains you have them as an assumption, I guess.

[Rémy Degenne]

At the bottom of page 18 of my preprint on the use of Markov kernels in Mathlib, in which I write about their use for conditional independence, I wrote:

Another more minor refactor would be to follow the example of
[For21] and (somewhat artificially) extend our definition to any space by requiring that there
exists a conditional kernel such that the definition applies

[Rémy Degenne]

By the way, I'm really glad that you are being paid to look at our probability theory material and make it better! I made some initial choices in those files but with more eyes on them we will surely improve them a lot.

[David Ledvinka]

Ok I think your discussion on the strength and weaknesses in the preprint is exactly relevant.

While we do assume we have such a Kernel in the case of Markov Chains the weak Markov property itself could be stated without this assumption, even though we cannot guarantee the existence of a transition kernel without the Borel assumption (which is why we do assume existence). I also agree with the fact that manipulating kernels is much easier, which is why I mentioned that the loss generality which is almost free on paper is probably much less free in formalisation. I could definitely work around this (perhaps with the minor refactor idea).

The only reason I am hesitant to not use the classical definition (a la Definition 4.1 in your preprint) is that if someone decides they do need this level of generality it seems like it will be a gargantuan refactor that will only get worse. Maybe thats fine though.

[David Ledvinka]

Doing some "light" research I noticed that @Asgar Jamneshan , who is on this forum, has several papers that consider generalisations of related ideas outside of the standard Borel setting (for example this one). Perhaps you have some insight here?

[Asgar Jamneshan]

The definition of a Markov kernel is valid on all spaces; it just does not, outside the standard Borel setting, represent conditional expectation (since the latter is only defined up to almost-everywhere equality, i.e., as an equivalence class in $L^2$). One way to define conditional independence is to work with conditional expectations instead of kernels, or equivalently in a pointfree framework using measure algebras of probability spaces (see Fremlin’s Measure Theory, Volume 4, §458). Another possibility is to work with Stone models of probability algebras (such models also appear under different names in the literature); see, for example, Section 8 of https://arxiv.org/pdf/2010.00681. Yet another possibility is to use category theory, as in Simpson’s paper: https://www.sciencedirect.com/science/article/pii/S1571066118300318. There is also a more topos-theoretic/sheaf-theoretic approach to measure theory, as developed in my paper cited above, but that might be overkill if the primary purpose is to formalize conditional independence.