OAI/NumberTheory/Jacobsthal/Paths/OutsideExceptionsWitness.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.FilteredBoxWordMass.selectedWordMass line 17
2. theorem OAI.Erdos970.NumberTheoryLean.FilteredBoxWordMass.filtered_word_box_mass line 21
3. theorem OAI.Erdos970.NumberTheoryLean.FilteredBoxWordMass.filtered_box_mass line 43
4. theorem OAI.Erdos970.NumberTheoryLean.FilteredBoxWordMass.unlisted_geometric_box_mass line 64
5. theorem OAI.Erdos970.NumberTheoryLean.SoftWitnessCapture.word_selection_descending line 93
6. theorem OAI.Erdos970.NumberTheoryLean.SoftWitnessCapture.word_multiplicity_descending line 104
7. theorem OAI.Erdos970.NumberTheoryLean.SoftWitnessCapture.soft_full_word_listed line 114
8. theorem OAI.Erdos970.NumberTheoryLean.SoftWitnessCapture.unlisted_has_no_soft_witness line 129
9. def OAI.Erdos970.ErdosVarianceEligible.eligibleWordWitness line 155
10. theorem OAI.Erdos970.ErdosVarianceEligible.eligible_word_witness_of_endpoint line 159
11. theorem OAI.Erdos970.ErdosVarianceEligible.word_error_bad_aligning_prime line 173
12. theorem OAI.Erdos970.NumberTheoryLean.EligibleListWord.listed_word_eligible_iff line 200
13. theorem OAI.Erdos970.NumberTheoryLean.EligibleListWord.listed_selection_eligible_iff line 216
14. theorem OAI.Erdos970.NumberTheoryLean.EligibleListWord.unlisted_compact_selected_data line 228
15. theorem OAI.Erdos970.ErdosVarianceEligible.geometric_selection_recent_witness line 258
16. theorem OAI.Erdos970.ErdosVarianceEligible.outside_exceptions_eligible_word line 298