OAI/Probability/ThorpCompatibility/HeavyColumns.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThorpCompatibility.remainingValues line 10
2. lemma OAI.ThorpCompatibility.card_remainingValues line 13
3. lemma OAI.ThorpCompatibility.mem_remainingValues line 16
4. lemma OAI.ThorpCompatibility.remainingValues_nonempty line 25
5. lemma OAI.ThorpCompatibility.columnPrediction_unused line 31
6. lemma OAI.ThorpCompatibility.entry_heavy_mass_bound line 43
7. lemma OAI.ThorpCompatibility.mean_entry_heavy_bound line 54
8. lemma OAI.ThorpCompatibility.column_heavy_bound line 65