OAI/Probability/GaussianInformation/Dyadic/ChannelEntropy.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RepeatedLocalization.integrable_xlog_bounded line 18
2. lemma OAI.RepeatedLocalization.klDiv_withDensity_bounded line 26
3. lemma OAI.RepeatedLocalization.measurable_finite_eval line 56
4. def OAI.RepeatedLocalization.FiniteChannel.law line 71
5. lemma OAI.RepeatedLocalization.FiniteChannel.measurable_density line 74
6. lemma OAI.RepeatedLocalization.FiniteChannel.lintegral_law line 78
7. lemma OAI.RepeatedLocalization.FiniteChannel.lintegral_prob line 87
8. lemma OAI.RepeatedLocalization.FiniteChannel.density_total line 93
9. instance OAI.RepeatedLocalization.FiniteChannel.law_probability line 99
10. lemma OAI.RepeatedLocalization.FiniteChannel.law_fst line 109
11. def OAI.RepeatedLocalization.FiniteChannel.outputLaw line 120
12. lemma OAI.RepeatedLocalization.FiniteChannel.law_snd line 123
13. instance OAI.RepeatedLocalization.FiniteChannel.outputLaw_probability line 136
14. lemma OAI.RepeatedLocalization.FiniteChannel.law_eq_sum line 141
15. def OAI.RepeatedLocalization.FiniteChannel.likelihoodRatio line 152
16. lemma OAI.RepeatedLocalization.FiniteChannel.measurable_likelihoodRatio line 155
17. lemma OAI.RepeatedLocalization.FiniteChannel.likelihoodRatio_nonneg line 160
18. lemma OAI.RepeatedLocalization.FiniteChannel.likelihoodRatio_le line 165
19. lemma OAI.RepeatedLocalization.FiniteChannel.law_eq_reference_density line 173
20. lemma OAI.RepeatedLocalization.FiniteChannel.integral_xlog_ratio line 198
21. lemma OAI.RepeatedLocalization.FiniteChannel.klDiv_law line 218