Commit 2026-04-28 09:12 e3d43da4

refactor(Probability/Process): rework predictable and progressive processes (#38254) The purpose of this PR is to rework IsProgressive and ProgMeasurable to have a weak (i.e., Measurable) and strong (i.e., StronglyMeasurable) variant, so that they are more in line with Adapted/StronglyAdapted. As a side effect, some lemmas can have certain typeclasses removed (which were previously needed to go back and forth between Measurable and StronglyMeasurable). Zulip discussion at #Brownian motion > Adapted Filtrations for Markov Chains and Markov Processes