OAI/Combinatorics/SharpRamsey/Entropy/TestSecondMomentBase.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLogRamsey.SecondMoment.abs_pairMean_self_le line 15
2. theorem OAI.SharpLogRamsey.SecondMoment.second_moment_finite line 34
3. theorem OAI.SharpLogRamsey.SecondMoment.second_moment_dyadic line 89
4. lemma OAI.SharpLogRamsey.SecondMoment.second_moment_exponent line 142
5. lemma OAI.SharpLogRamsey.SecondMoment.numerical_budgets line 188
6. theorem OAI.SharpLogRamsey.SecondMoment.prepared_pencil_second_moment line 241