OAI/Probability/DirectionalWalk/EntropyTransforms.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalZeroOne.atom_le_map line 12
  2. lemma OAI.DirectionalZeroOne.conditionalInfo_eq_kernel line 18
  3. lemma OAI.DirectionalZeroOne.ac_conditioning_projection line 28
  4. lemma OAI.DirectionalZeroOne.conditionedEntropy_monotone_projection line 47
  5. lemma OAI.DirectionalZeroOne.conditionedEntropy_eq_conditionalEntropy line 69
  6. lemma OAI.DirectionalZeroOne.conditionedEntropy_le_conditionedEntropy line 78
  7. lemma OAI.DirectionalZeroOne.informationOf_nonneg line 105
  8. lemma OAI.DirectionalZeroOne.informationOf_comp_le line 111
  9. lemma OAI.DirectionalZeroOne.integrable_informationOf_comp line 124
  10. lemma OAI.DirectionalZeroOne.entropyOf_comp_le line 132
  11. lemma OAI.DirectionalZeroOne.conditionedInformation_fiberwise_injective line 138
  12. lemma OAI.DirectionalZeroOne.informationOf_pair_indep line 158
  13. lemma OAI.DirectionalZeroOne.conditionedInformation_indep line 172
  14. lemma OAI.DirectionalZeroOne.conditionedEntropy_indep line 178
  15. lemma OAI.DirectionalZeroOne.conditionedInformation_indep_pair line 182
  16. lemma OAI.DirectionalZeroOne.conditionedEntropy_indep_pair line 199