Conditional kernel predicate

Stream: mathlib4

[Rémy Degenne]

Out of curiosity, what is the goal of that refactor?

[Yaël Dillies]

The current issue is that docs#ProbabilityTheory.Kernel.condKernel only works for a standard Borel space, and @Kalle Kytölä claims there are situations where we don't have that, and yet we have a conditional kernel

[Rémy Degenne]

What kind of situations? Do you mean other hypotheses under which you can also get a general construction for a conditional kernel, or do you mean that it might well exist for particular kernels ("by chance") and then if it exists for some kernels, then it exists for others that you can build from them?

[Yaël Dillies]

I was involved in the refactor only recently so I have to ask Kalle (in a few minutes), but it seems that it is the latter

[Yaël Dillies]

Rémy Degenne said:

if it exists for some kernels, then it exists for others that you can build from them

That is particularly true when considering docs#ProbabilityTheory.Kernel.condKernelCountable

[Kalle Kytölä]

General constructions indeed only exists for Borel spaces, but isolating the defining property (a characteristic predicate) from the construction seems worthwhile. As you say, kernels might exist "by chance" even in other situations. But maybe more importantly, a user should be able to make hypotheses about the existence of kernels in spaces which are not standard Borel, or which the user at least does not want to prove are standard Borel.

So the main argument is: The construction requires the user to provide a proof of standard Borel space property. The characteristic predicate can be used without that. @Kin Yau James Wong has shown that many of the lemmas about the kernels hold assuming only the characteristic predicate, and he has of course also shown that the construction satisfies the characteristic predicate.

[Yaël Dillies]

What's not super clear to me is how often we care about non-standard Borel spaces

[Rémy Degenne]

That makes sense and looks like a very sensible refactor!

[Kalle Kytölä]

Seldom, indeed (referring to Yaël's question about how often we care about spaces that are not standard Borel spaces). But in my opinion we would often want to free the user from providing the proof of the standard Borel space property.

[Rémy Degenne]

That refactor makes me think of the approach of the paper https://arxiv.org/abs/1908.07021 by Fritz about Markov categories, and in particular of definition 11.5: Fritz defines the property of having conditionals for a Markov category, and then remarks that it is the case for categories of finite probability spaces and for the category of standard Borel spaces.

[Yaël Dillies]

#15105