OAI/InformationTheory/Entanglement/SequentialSampling.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SecretKey.sampled_pair_law line 13
2. def OAI.SecretKey.sampledPrefix line 37
3. def OAI.SecretKey.sampledHistory line 40
4. lemma OAI.SecretKey.sampledPrefix_succ line 43
5. lemma OAI.SecretKey.sampledPrefix_eq line 46
6. lemma OAI.SecretKey.measurable_tape_coordinate line 55
7. lemma OAI.SecretKey.sampledPrefix_measurable line 59
8. lemma OAI.SecretKey.sampledPrefix_measurable_global line 75
9. lemma OAI.SecretKey.sampledHistory_measurable line 78
10. theorem OAI.SecretKey.sampled_history_step line 84
11. def OAI.SecretKey.recordPrefix line 100
12. lemma OAI.SecretKey.recordPrefix_measurable line 101
13. lemma OAI.SecretKey.snoc_measurable line 103
14. lemma OAI.SecretKey.recordPrefix_succ line 111
15. theorem OAI.SecretKey.full_history_law_unique line 116
16. theorem OAI.SecretKey.sampled_full_history_law line 132