OAI/Combinatorics/Progressions/Probability/InactivePrincipalLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.inactivePrincipalPMF line 12
2. theorem OAI.Erdos3.inactivePrincipalPMF_support line 15
3. theorem OAI.Erdos3.inactivePrincipal_scaled_upper line 19
4. theorem OAI.Erdos3.inactivePrincipal_scaled_lower line 35
5. theorem OAI.Erdos3.inactivePrincipal_block_bound line 48
6. def OAI.Erdos3.inactiveDenominator line 61
7. theorem OAI.Erdos3.inactiveDenominator_pos line 63
8. theorem OAI.Erdos3.inactiveDenominator_bound line 66