OAI/Probability/SwitchChain/BalancedBlockVariance.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem315.BalancedBlockVariance.Balanced line 14
2. theorem OAI.Problem315.BalancedBlockVariance.sum_row_card line 20
3. theorem OAI.Problem315.BalancedBlockVariance.lower_le line 27
4. theorem OAI.Problem315.BalancedBlockVariance.lower_sum_le line 34
5. theorem OAI.Problem315.BalancedBlockVariance.totals line 39
6. def OAI.Problem315.BalancedBlockVariance.countVector line 44
7. def OAI.Problem315.BalancedBlockVariance.forgetCounts line 60
8. def OAI.Problem315.BalancedBlockVariance.familyEquiv line 68
9. theorem OAI.Problem315.BalancedBlockVariance.row_variance_bound line 103
10. theorem OAI.Problem315.BalancedBlockVariance.row_variance_bound_of_rowInvariant line 126