OAI/Probability/ThorpCompatibility/GridDeficits.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThorpCompatibility.jointRowDeficit line 10
2. def OAI.ThorpCompatibility.rowDeficit line 13
3. def OAI.ThorpCompatibility.colDeficit line 16
4. def OAI.ThorpCompatibility.heavyTotal line 19
5. lemma OAI.ThorpCompatibility.rowDeficit_nonneg line 22
6. lemma OAI.ThorpCompatibility.colDeficit_nonneg line 25
7. lemma OAI.ThorpCompatibility.heavyTotal_nonneg line 28
8. lemma OAI.ThorpCompatibility.rowDeficit_le_joint line 36
9. lemma OAI.ThorpCompatibility.clump_deficit_bound line 50
10. lemma OAI.ThorpCompatibility.heavyTotal_log_bound line 72
11. lemma OAI.ThorpCompatibility.absorb_entropy_losses line 83