OAI/InformationTheory/SoftChannel/SoftInformation.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.softJointNat line 12
  2. def OAI.LeanBlast.CourtadeKumar.boolJointNat line 15
  3. def OAI.LeanBlast.CourtadeKumar.mutualInformationNat line 20
  4. lemma OAI.LeanBlast.CourtadeKumar.noiseKernel_nonneg_closed line 23
  5. lemma OAI.LeanBlast.CourtadeKumar.signProbability_nonneg_soft line 29
  6. lemma OAI.LeanBlast.CourtadeKumar.softJointNat_nonneg line 33
  7. lemma OAI.LeanBlast.CourtadeKumar.softJointNat_posterior line 38
  8. lemma OAI.LeanBlast.CourtadeKumar.softJointNat_left line 45
  9. lemma OAI.LeanBlast.CourtadeKumar.softJointNat_right line 52
  10. lemma OAI.LeanBlast.CourtadeKumar.softJointNat_total line 57
  11. lemma OAI.LeanBlast.CourtadeKumar.softJointNat_xlogx_bool line 62
  12. theorem OAI.LeanBlast.CourtadeKumar.soft_information_identity line 70
  13. lemma OAI.LeanBlast.CourtadeKumar.boolJointNat_eq_soft line 89
  14. lemma OAI.LeanBlast.CourtadeKumar.signEncoding_closed line 98
  15. lemma OAI.LeanBlast.CourtadeKumar.information_signEncoding line 102
  16. lemma OAI.LeanBlast.CourtadeKumar.bool_information_identity line 106
  17. lemma OAI.LeanBlast.CourtadeKumar.psi_abs_soft line 112
  18. lemma OAI.LeanBlast.CourtadeKumar.psiInv_psi_abs line 117
  19. lemma OAI.LeanBlast.CourtadeKumar.refined_curve_le line 121
  20. lemma OAI.LeanBlast.CourtadeKumar.refined_curve_strict line 127
  21. theorem OAI.LeanBlast.CourtadeKumar.refined_boolean_bound line 135
  22. lemma OAI.LeanBlast.CourtadeKumar.information_scaled_coordinate line 143
  23. lemma OAI.LeanBlast.CourtadeKumar.information_noise_scaled_coordinate line 150
  24. theorem OAI.LeanBlast.CourtadeKumar.all_soft_coordinate_attainment line 159