OAI/Probability/GaussianInformation/Dyadic/StateInformation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RepeatedLocalization.FiniteChannel.coarsen_equiv line 22
2. lemma OAI.RepeatedLocalization.FiniteChannel.coarsen_bind_map line 33
3. lemma OAI.RepeatedLocalization.FiniteChannel.coarsen_congr_prob line 49
4. lemma OAI.RepeatedLocalization.FiniteChannel.bind_congr_prob line 56
5. lemma OAI.RepeatedLocalization.historyChannel_succ line 64
6. lemma OAI.RepeatedLocalization.FiniteChannel.ext_prob line 73
7. def OAI.RepeatedLocalization.UniformBlockCost line 80
8. lemma OAI.RepeatedLocalization.experimentLaw_eq_law line 85
9. lemma OAI.RepeatedLocalization.experimentLaw_probability line 91
10. lemma OAI.RepeatedLocalization.mutualInformation_experiment line 97
11. lemma OAI.RepeatedLocalization.mutualInformation_map_right line 103
12. lemma OAI.RepeatedLocalization.actual_uniform_blockCost line 120