Commit 2026-06-05 10:53 bf1fea35

View on Github →

feat: API for stoppedValue and StoppedProcess (#37429)

Estimated changes

Modified Mathlib/Probability/Process/Stopping.lean

added theorem MeasureTheory.stoppedProcess_comp

added theorem MeasureTheory.stoppedProcess_const

added theorem MeasureTheory.stoppedProcess_const_bot

added theorem MeasureTheory.stoppedProcess_const_smul

added theorem MeasureTheory.stoppedProcess_const_top

added theorem MeasureTheory.stoppedProcess_div

added theorem MeasureTheory.stoppedProcess_inv

added theorem MeasureTheory.stoppedProcess_mul

added theorem MeasureTheory.stoppedProcess_norm

added theorem MeasureTheory.stoppedValue_comp

modified theorem MeasureTheory.stoppedValue_const

added theorem MeasureTheory.stoppedValue_const_bot

added theorem MeasureTheory.stoppedValue_const_smul

added theorem MeasureTheory.stoppedValue_div

added theorem MeasureTheory.stoppedValue_inv

added theorem MeasureTheory.stoppedValue_mul

added theorem MeasureTheory.stoppedValue_norm