Measurable functions, natural filtration and adapted process

Stream: mathlib4

[Etienne Marion]

Hi! I want to generalize docs#MeasureTheory.Filtration.natural to take as input a family of measurable functions instead of strongly measurable functions, so that I can define a filtration on a product of measurable spaces without any topology. While I was doing that I realized that all the library about adapted processes was written in terms of strongly measurable functions, which makes the aforementioned generalization painful. I am wondering wether it would make sense be to generalize all the definitions (e.g. docs#MeasureTheory.Adapted) to measurable functions? I realized that many proofs are using docs#MeasureTheory.StronglyMeasurable.measurable, so it seems to make sense, but maybe we'll lose something here. Maybe define another predicate stronglyAdapted?
Tagging @Kexing Ying and @Rémy Degenne who wrote this part of the library.

[Rémy Degenne]

I can't give you a quick answer right now. I don't recall why StronglyMeasurable was used instead of Measurable. I'll need to look at the library to look for clues. Perhaps your refactor attempt shows some particular places where StronglyMeasurable seems more useful than Measurable?

[Etienne Marion]

I didn't gp far enough to tell you because I wanted to ask before really trying. I'll keep changing defs and see what happens.

[Rémy Degenne]

I guess the definition of a martingale is the key (it's the central object of the work we did): it's about conditional expectations, so it needs strong measurability.

[Etienne Marion]

Yes that makes sense, but on the other hand I did come across lemmas where strong measurability was not needed. This makes me thinks that a second predicate stronglyAdapted might be a solution, because we would have stronglyAdapted => adapted so it would work nicely.