OAI/Probability/ClassicalON/DyadicSums.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClassicalON.dyadic_inverse_square_sum line 9
2. theorem OAI.ClassicalON.sum_dyadic_ratio_lower line 24
3. theorem OAI.ClassicalON.dyadic_min_ratio_sum line 43
4. theorem OAI.ClassicalON.weighted_dyadic_min_pair line 72
5. theorem OAI.ClassicalON.dyadic_min_cost_sum line 77