OAI/Probability/DirectionalWalk/EntropyBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalZeroOne.geometric_comparison_sum line 12
2. lemma OAI.DirectionalZeroOne.geometric_comparison_cost line 19
3. lemma OAI.DirectionalZeroOne.entropy_nat_moment line 24
4. lemma OAI.DirectionalZeroOne.entropy_finite line 66
5. lemma OAI.DirectionalZeroOne.entropyOf_pair_le line 85
6. lemma OAI.DirectionalZeroOne.entropyOf_nat_moment line 94
7. lemma OAI.DirectionalZeroOne.entropyOf_finite line 108
8. lemma OAI.DirectionalZeroOne.entropyOf_int_moment line 116
9. lemma OAI.DirectionalZeroOne.entropyOf_lattice_moment line 146