OAI/Probability/SKBarriers/Locking/NarrowClockAlgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.narrowClockPerturbed line 13
2. theorem OAI.SK.Analytic.narrowClockPerturbed_pair_zero line 18
3. theorem OAI.SK.Analytic.narrowClockPerturbed_square line 24
4. theorem OAI.SK.Analytic.narrowClockPerturbed_common line 31
5. theorem OAI.SK.Analytic.narrowClockPerturbed_singleton line 39
6. theorem OAI.SK.Analytic.narrowClockPerturbed_pair line 47
7. theorem OAI.SK.Analytic.narrowClockPerturbed_common_penalty line 55
8. theorem OAI.SK.Analytic.narrowClockPerturbed_singleton_penalty line 63
9. theorem OAI.SK.Analytic.narrowClockPerturbed_pair_penalty line 71