OAI/Probability/GaussianInformation/Dyadic/PosteriorChannels.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RepeatedLocalization.scorePosterior line 18
  2. lemma OAI.RepeatedLocalization.scorePosterior_probability line 22
  3. lemma OAI.RepeatedLocalization.integral_scorePosterior line 34
  4. lemma OAI.RepeatedLocalization.scorePosterior_apply_le line 44
  5. lemma OAI.RepeatedLocalization.scorePosterior_null_of_score_zero line 54
  6. lemma OAI.RepeatedLocalization.scorePosterior_absolutelyContinuous line 65
  7. lemma OAI.RepeatedLocalization.scoreMass_posterior_mul line 69
  8. lemma OAI.RepeatedLocalization.infoContribution_split line 77
  9. lemma OAI.RepeatedLocalization.infoContribution_split_zero line 117
  10. structure OAI.RepeatedLocalization.FiniteChannel line 136
  11. lemma OAI.RepeatedLocalization.FiniteChannel.le_one line 145
  12. lemma OAI.RepeatedLocalization.FiniteChannel.integrable line 149
  13. lemma OAI.RepeatedLocalization.FiniteChannel.mass_total line 153
  14. lemma OAI.RepeatedLocalization.FiniteChannel.information_nonneg line 159
  15. def OAI.RepeatedLocalization.FiniteChannel.bind line 163
  16. lemma OAI.RepeatedLocalization.FiniteChannel.information_bind line 172
  17. def OAI.RepeatedLocalization.FiniteChannel.deterministic line 195
  18. lemma OAI.RepeatedLocalization.FiniteChannel.deterministic_information line 204
  19. lemma OAI.RepeatedLocalization.infoContribution_sum_le line 218
  20. def OAI.RepeatedLocalization.FiniteChannel.coarsen line 237
  21. lemma OAI.RepeatedLocalization.FiniteChannel.information_coarsen_le line 246