OAI/Combinatorics/SquareDifference/ExceptionalBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SquareDifference.exists_exceptional_threshold line 13
2. lemma OAI.SquareDifference.primeProduct_one_le line 35
3. lemma OAI.SquareDifference.tupleEta_le_one_of_fourth line 42
4. lemma OAI.SquareDifference.exceptional_weight_budget line 51
5. lemma OAI.SquareDifference.exceptional_large_tail line 63
6. lemma OAI.SquareDifference.exceptional_small_power_budget line 86