OAI/Probability/GaussianInformation/Dyadic/ChannelProducts.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RepeatedLocalization.scorePosterior_assoc line 18
2. lemma OAI.RepeatedLocalization.scoreMass_indicator_one line 33
3. lemma OAI.RepeatedLocalization.scorePosterior_indicator_one line 39
4. lemma OAI.RepeatedLocalization.scorePosterior_congr_ae line 51
5. lemma OAI.RepeatedLocalization.scorePosterior_null_iff line 60
6. lemma OAI.RepeatedLocalization.infoContribution_support_lower line 76
7. lemma OAI.RepeatedLocalization.scorePosterior_of_mass_zero line 118
8. lemma OAI.RepeatedLocalization.scoreMass_mul_le line 122
9. lemma OAI.RepeatedLocalization.scoreMass_mul_eq line 136
10. def OAI.RepeatedLocalization.FiniteChannel.dbind line 150
11. lemma OAI.RepeatedLocalization.FiniteChannel.information_dbind line 159
12. lemma OAI.RepeatedLocalization.FiniteChannel.mass_dbind line 181
13. lemma OAI.RepeatedLocalization.FiniteChannel.mass_bind line 188
14. lemma OAI.RepeatedLocalization.FiniteChannel.coarsen_dbind_fst line 195
15. lemma OAI.RepeatedLocalization.FiniteChannel.coarsen_comp line 204