OAI/Probability/DirectionalWalk/EntropyLaws.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalZeroOne.informationOf_map line 20
2. lemma OAI.DirectionalZeroOne.entropyOf_map line 27
3. lemma OAI.DirectionalZeroOne.conditionedEntropy_map line 35
4. lemma OAI.DirectionalZeroOne.informationOf_same_fibers line 48
5. lemma OAI.DirectionalZeroOne.conditionedInformation_same_conditioner line 57
6. lemma OAI.DirectionalZeroOne.conditionedEntropy_monotone_function line 65
7. lemma OAI.DirectionalZeroOne.entropyOf_prod_fst line 79
8. lemma OAI.DirectionalZeroOne.conditionedEntropy_prod_fst line 84