OAI/NumberTheory/OrdinaryCorrelations/HighTrace/TwoTermBinomial.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.SourceCylinder.two_term_binomial line 26
2. lemma OAI.OrdinaryCorrelations.SourceCylinder.double_power_le line 39
3. lemma OAI.OrdinaryCorrelations.SourceCylinder.factorial_power_bound line 48
4. lemma OAI.OrdinaryCorrelations.SourceCylinder.geometric_two_bound line 64
5. lemma OAI.OrdinaryCorrelations.SourceCylinder.choose_factorial_le line 69
6. lemma OAI.OrdinaryCorrelations.SourceCylinder.proper_subset_factorial_sum line 78
7. lemma OAI.OrdinaryCorrelations.SourceCylinder.intersection_support_inj line 108
8. lemma OAI.OrdinaryCorrelations.SourceCylinder.coefficient_crude line 113