OAI/Probability/DirectionalWalk/Information.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.informationOf line 12
  2. def OAI.DirectionalZeroOne.entropyOf line 15
  3. def OAI.DirectionalZeroOne.conditionedInformation line 18
  4. def OAI.DirectionalZeroOne.conditionedEntropy line 22
  5. lemma OAI.DirectionalZeroOne.informationOf_fiber line 33
  6. lemma OAI.DirectionalZeroOne.informationOf_pair_comm line 40
  7. lemma OAI.DirectionalZeroOne.informationOf_pair_assoc line 49
  8. lemma OAI.DirectionalZeroOne.informationOf_function line 58
  9. lemma OAI.DirectionalZeroOne.entropyOf_eq_discreteEntropy line 66
  10. lemma OAI.DirectionalZeroOne.integrable_informationOf_iff line 71
  11. lemma OAI.DirectionalZeroOne.conditionedInformation_eq line 76
  12. lemma OAI.DirectionalZeroOne.conditionedInformation_nonneg line 88
  13. lemma OAI.DirectionalZeroOne.integrable_conditionedInformation line 94
  14. lemma OAI.DirectionalZeroOne.conditionedEntropy_le_entropyOf line 114
  15. lemma OAI.DirectionalZeroOne.conditionedInformation_chain line 134
  16. lemma OAI.DirectionalZeroOne.conditionedEntropy_chain line 142
  17. lemma OAI.DirectionalZeroOne.informationOf_pair_chain line 152
  18. lemma OAI.DirectionalZeroOne.integrable_informationOf_pair line 158
  19. lemma OAI.DirectionalZeroOne.entropyOf_pair_chain line 167