refactor(Probability/Process): rework predictable and progressive processes#38254

Open

jvanwinden wants to merge 14 commits intoleanprover-community:masterfrom

jvanwinden:strongly_progressive_predictable

Commits on Apr 19, 2026

rename IsPredictable to IsStronglyPredictable
Joris van Winden
committed
rename lemmas relating to IsStronglyPredictable
Joris van Winden
committed
remove typeclasses from predictability lemmas with discrete filtration
Joris van Winden
committed
golf proof
Joris van Winden
committed
remove outdated comments
Joris van Winden
committed

Commits on Apr 20, 2026

clean up proof using letI
Joris van Winden
committed
reorganize, partially remove typeclasses from ispredictable_of_measurable_add_one
Joris van Winden
committed
remove more typeclasses and sorrys
Joris van Winden
committed
small change
Joris van Winden
committed
rename progMeasurable to isStronglyProgressive
Joris van Winden
committed
deprecate old theorem
Joris van Winden
committed
change 'progressively measurable' to 'strongly progressive' in comments
Joris van Winden
committed
clean up proof
Joris van Winden
committed
remove usage of deprecated lemma
Joris van Winden
committed