OAI/Combinatorics/BalancedRyser/Candidates/CandidateAbundanceAssembly.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.CandidateAbundanceAssembly.measureReal_eq_offset line 19
2. def OAI.Balanced.CandidateAbundanceAssembly.slotLinearConstant line 25
3. theorem OAI.Balanced.CandidateAbundanceAssembly.slotLinearConstant_pos line 27
4. theorem OAI.Balanced.CandidateAbundanceAssembly.tendsto_good_of_bad line 35
5. theorem OAI.Balanced.CandidateAbundanceAssembly.tendsto_successful_roots line 46
6. theorem OAI.Balanced.CandidateAbundanceAssembly.tendsto_square_fibers line 54
7. theorem OAI.Balanced.CandidateAbundanceAssembly.tendsto_constituent_losses line 73
8. theorem OAI.Balanced.CandidateAbundanceAssembly.tendsto_candidateSlots_of_witness_tails line 97
9. theorem OAI.Balanced.CandidateAbundanceAssembly.tendsto_candidateSlots_of_external_tail line 143