OAI/Combinatorics/BalancedRyser/Candidates/CandidateGeneratorPairTail.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.CandidateGeneratorPair.momentConstant line 15
2. theorem OAI.Balanced.CandidateGeneratorPair.momentConstant_nonneg line 18
3. theorem OAI.Balanced.CandidateGeneratorPair.count_upper_tail line 22
4. theorem OAI.Balanced.CandidateGeneratorPair.any_pair_upper_tail line 42
5. theorem OAI.Balanced.CandidateGeneratorPair.scale_pair_tail line 74
6. theorem OAI.Balanced.CandidateGeneratorPair.any_pair_source_tail line 84
7. theorem OAI.Balanced.CandidateGeneratorPair.squared_denominator_le_linear line 104
8. theorem OAI.Balanced.CandidateGeneratorPair.all_pairs_tendsto_one line 109
9. theorem OAI.Balanced.CandidateGeneratorPair.count_le_ceil_of_source_bound line 154