OAI/Dynamics/ConditionalShuffle/ScheduledInstrument.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Revealed.Scheduled.Symbol line 11
2. def OAI.Revealed.Scheduled.stepInstrument line 13
3. lemma OAI.Revealed.Scheduled.base_clock line 19
4. lemma OAI.Revealed.Scheduled.base_outside line 31
5. lemma OAI.Revealed.Scheduled.observed_outside line 42
6. lemma OAI.Revealed.Scheduled.observed_public line 57
7. lemma OAI.Revealed.Scheduled.group_eq line 72
8. lemma OAI.Revealed.Scheduled.kernel_dichotomy line 83
9. def OAI.Revealed.Scheduled.interval line 115
10. lemma OAI.Revealed.Scheduled.interval_kernel line 121
11. lemma OAI.Revealed.Scheduled.interval_probability line 126
12. lemma OAI.Revealed.Scheduled.interval_dichotomy line 131
13. def OAI.Revealed.Scheduled.decode line 136
14. lemma OAI.Revealed.Scheduled.decode_injective line 140
15. lemma OAI.Revealed.Scheduled.decode_observed line 148
16. lemma OAI.Revealed.Scheduled.interval_weighted_cost line 155