OAI/NumberTheory/GaussianMoat/InformationTelescope.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.GaussianMoat.exists_batch_information line 10
2. lemma OAI.GaussianMoat.finite_entropy_telescope line 79
3. theorem OAI.GaussianMoat.word_entropy_rate_monotone line 93
4. lemma OAI.GaussianMoat.FinLaw.cIf_refinement line 138
5. theorem OAI.GaussianMoat.common_law_information_telescope line 151
6. def OAI.GaussianMoat.TimeLaw.info line 201
7. lemma OAI.GaussianMoat.TimeLaw.advance_info line 205
8. lemma OAI.GaussianMoat.commonSchedule_smooth line 214
9. theorem OAI.GaussianMoat.schedule_information_telescope line 218
10. theorem OAI.GaussianMoat.schedule_batch_information line 240