OAI/NumberTheory/Jacobsthal/Estimates/CandidateExceptionMass.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.MultiplicitySuffixRank.lowerIndices line 15
2. def OAI.Erdos970.NumberTheoryLean.MultiplicitySuffixRank.suffixRank line 16
3. theorem OAI.Erdos970.NumberTheoryLean.MultiplicitySuffixRank.below_total_rank line 18
4. theorem OAI.Erdos970.NumberTheoryLean.MultiplicitySuffixRank.suffixRank_pos line 22
5. theorem OAI.Erdos970.NumberTheoryLean.MultiplicitySuffixRank.suffixRank_strict line 26
6. theorem OAI.Erdos970.NumberTheoryLean.MultiplicitySuffixRank.suffixRank_injective_singletons line 40
7. theorem OAI.Erdos970.NumberTheoryLean.MultiplicitySuffixRank.singleton_card_le_rank line 50
8. theorem OAI.Erdos970.NumberTheoryLean.BoundedEdgeSuffixRank.list_length_le_exponents line 73
9. theorem OAI.Erdos970.NumberTheoryLean.BoundedEdgeSuffixRank.bounded_edge_rank_le line 83
10. def OAI.Erdos970.NumberTheoryLean.BoundedCandidateCount.candidateBins line 126
11. theorem OAI.Erdos970.NumberTheoryLean.BoundedCandidateCount.candidate_bins_card_le line 129
12. theorem OAI.Erdos970.NumberTheoryLean.RecentReferenceSegment.recent_reference_segment line 154
13. def OAI.Erdos970.NumberTheoryLean.CandidateExceptionMass.someWitnessMass line 235
14. theorem OAI.Erdos970.NumberTheoryLean.CandidateExceptionMass.some_witness_mass_le_sum line 240
15. theorem OAI.Erdos970.NumberTheoryLean.CandidateExceptionMass.some_witness_mass_bound line 257
16. theorem OAI.Erdos970.NumberTheoryLean.CandidateExceptionMass.some_witness_mass_card_bound line 264