OAI/Probability/Localization/History.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.RepeatedLocalization.FiniteEntropy.letterMeasurableSpace line 12
2. lemma OAI.RepeatedLocalization.FiniteEntropy.state_nil line 14
3. lemma OAI.RepeatedLocalization.FiniteEntropy.state_append line 17
4. lemma OAI.RepeatedLocalization.FiniteEntropy.attemptLetter_none_iff line 21
5. lemma OAI.RepeatedLocalization.FiniteEntropy.attemptLetter_some_iff line 30
6. lemma OAI.RepeatedLocalization.FiniteEntropy.measurableSet_firstHeavy_union line 45
7. lemma OAI.RepeatedLocalization.FiniteEntropy.measurable_attemptLetter line 49
8. lemma OAI.RepeatedLocalization.FiniteEntropy.state_event_measurable line 75
9. lemma OAI.RepeatedLocalization.FiniteEntropy.state_event_subset_initial line 86
10. lemma OAI.RepeatedLocalization.FiniteEntropy.state_event_subset_cell line 97
11. lemma OAI.RepeatedLocalization.FiniteEntropy.state_descendant_of_mem line 116
12. lemma OAI.RepeatedLocalization.FiniteEntropy.measurable_run line 137
13. lemma OAI.RepeatedLocalization.FiniteEntropy.run_length_le line 153
14. lemma OAI.RepeatedLocalization.FiniteEntropy.run_length_of_active line 163
15. lemma OAI.RepeatedLocalization.FiniteEntropy.run_mem_event line 177
16. lemma OAI.RepeatedLocalization.FiniteEntropy.run_eq_iff_mem line 191
17. lemma OAI.RepeatedLocalization.FiniteEntropy.run_fiber_inter_initial line 244
18. lemma OAI.RepeatedLocalization.FiniteEntropy.run_succ_of_stopped line 255
19. lemma OAI.RepeatedLocalization.FiniteEntropy.run_add_of_stopped line 259
20. lemma OAI.RepeatedLocalization.FiniteEntropy.run_of_stopped_le line 267
21. lemma OAI.RepeatedLocalization.FiniteEntropy.attempts_spec line 273
22. lemma OAI.RepeatedLocalization.FiniteEntropy.attempts_min line 277
23. lemma OAI.RepeatedLocalization.FiniteEntropy.attempts_pos line 284
24. lemma OAI.RepeatedLocalization.FiniteEntropy.terminalLog_length line 291
25. lemma OAI.RepeatedLocalization.FiniteEntropy.terminalLog_of_stopped line 298
26. lemma OAI.RepeatedLocalization.FiniteEntropy.measurableSet_stopped line 306
27. lemma OAI.RepeatedLocalization.FiniteEntropy.measurableSet_terminates line 311
28. lemma OAI.RepeatedLocalization.FiniteEntropy.measurable_attempts line 318
29. lemma OAI.RepeatedLocalization.FiniteEntropy.measurable_terminalLog line 343
30. lemma OAI.RepeatedLocalization.FiniteEntropy.terminates_of_terminal_stopped line 349
31. lemma OAI.RepeatedLocalization.FiniteEntropy.terminalLog_fiber_inter_initial line 353