OAI/Probability/GaussianInformation/Dyadic/TranscriptLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RepeatedLocalization.FiniteChannel.coarsen_density_sum line 26
2. lemma OAI.RepeatedLocalization.FiniteChannel.law_coarsen line 44
3. lemma OAI.RepeatedLocalization.FiniteChannel.positive_ae_law line 62
4. lemma OAI.RepeatedLocalization.FiniteChannel.integral_law_snd line 67
5. lemma OAI.RepeatedLocalization.Realization.transcript_meas line 76
6. lemma OAI.RepeatedLocalization.Realization.augmented_eq line 84
7. lemma OAI.RepeatedLocalization.Realization.information_le line 99
8. lemma OAI.RepeatedLocalization.Realization.level_eq line 107