OAI/Probability/FreeIsing/Martingales/StoppedTimePrimitive.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.StoppedTimePrimitive.stopDensity line 10
2. theorem OAI.Problem367.StoppedTimePrimitive.integral_indicator_min line 14
3. theorem OAI.Problem367.StoppedTimePrimitive.stoppedProcess_primitive line 26
4. theorem OAI.Problem367.StoppedTimePrimitive.continuous_stoppedProcess line 38
5. theorem OAI.Problem367.StoppedTimePrimitive.monotone_stoppedProcess line 47
6. theorem OAI.Problem367.StoppedTimePrimitive.stopTime_eq_iff_le line 56
7. theorem OAI.Problem367.StoppedTimePrimitive.isStronglyProgressive_stopDensity line 62
8. theorem OAI.Problem367.StoppedTimePrimitive.stoppedProcess_weighted_primitive line 74