Adapted Filtrations for Markov Chains and Markov Processes

Stream: Brownian motion

[David Ledvinka]

This is not directly related to the Brownian Motion project but I figured this would be the best channel to post this since, a) this channel probably contains most of the people who have answers, b) it may be relevant to the project down the line, c) this may involve refactoring definitions important to the project.

I have started thinking a little bit about formalizing Markov Chains and Markov Processes and I realized the definition of an Adapted filter requires a topology on the state space (and strong measurability). This makes sense for Martingales since you need to take expectations on the state space as part of the definition but is not necessary for Markov chains. Should we have Adapted and StronglyAdapted? Is there a way to do this that avoids duplicating everything?

[Etienne Marion]

I think it would make sense to have StronglyAdapted yes. I came across this a while ago: #mathlib4 > Measurable functions, natural filtration and adapted process

[Rémy Degenne]

Yes, this question has come up several times, and that's evidence we need both definitions.

[David Ledvinka]

#32882