Commit 2026-07-23 09:03 3e810593
View on Github →refactor: change the definition of the stopped sigma-algebra (#42021)
Change the definition of MeasureTheory.IsStoppingTime.measurableSpace to require that it contains only sets that are measurable wrt ⨆ t, f t where f is the filtration. This is what is done for instance in Semimartingale Theory and Stochastic Calculus by He Wang Yan and is needed in the Brownian motion project.