OAI/Combinatorics/Progressions/Polynomial/BinomialMomentAmplification.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.pow_le_choose_block line 11
2. theorem OAI.Erdos3.expect_one_add_pow_eq line 29
3. theorem OAI.Erdos3.expect_one_add_pow_lower line 45
4. theorem OAI.Erdos3.expect_one_add_pow_block_lower line 52