Commit 2025-11-17 15:13 647a1018

View on Github →

feat: lemmas on the stopped process and stopped value (#31557)

Estimated changes

Modified Mathlib/Probability/Process/Stopping.lean

modified theorem MeasureTheory.stoppedProcess_eq_of_ge

modified theorem MeasureTheory.stoppedProcess_eq_of_le

modified theorem MeasureTheory.stoppedProcess_eq_stoppedValue

added theorem MeasureTheory.stoppedProcess_eq_stoppedValue_apply

added theorem MeasureTheory.stoppedProcess_indicator_comm'

added theorem MeasureTheory.stoppedProcess_indicator_comm

added theorem MeasureTheory.stoppedProcess_stoppedProcess'

added theorem MeasureTheory.stoppedProcess_stoppedProcess

added theorem MeasureTheory.stoppedProcess_stoppedProcess_of_le_left

added theorem MeasureTheory.stoppedProcess_stoppedProcess_of_le_right

modified theorem MeasureTheory.stoppedValue_stoppedProcess

modified theorem MeasureTheory.stoppedValue_stoppedProcess_ae_eq

added theorem MeasureTheory.stoppedValue_stoppedProcess_apply