OAI/Probability/ThorpCompatibility/EntropyChain.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpCompatibility.Law.entropy_eq_of_fibers line 12
2. lemma OAI.ThorpCompatibility.Law.condEntropy_chain line 23
3. lemma OAI.ThorpCompatibility.Law.condEntropy_le_entropy line 32
4. lemma OAI.ThorpCompatibility.Law.entropy_pair_le line 38
5. def OAI.ThorpCompatibility.Law.history line 44
6. lemma OAI.ThorpCompatibility.Law.history_eq_iff line 48
7. lemma OAI.ThorpCompatibility.Law.history_step_fibers line 61
8. lemma OAI.ThorpCompatibility.Law.sum_fin_telescope line 77
9. lemma OAI.ThorpCompatibility.Law.entropy_chain_history line 87
10. lemma OAI.ThorpCompatibility.Law.entropy_chain line 117
11. lemma OAI.ThorpCompatibility.Law.entropy_tuple_le line 133