OAI/NumberTheory/Jacobsthal/Estimates/ReferenceIsolatedExclusion.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.SourceLengthExclusion.sourcePrimeSet_eq_between line 18
2. theorem OAI.Erdos970.NumberTheoryLean.SourceLengthExclusion.uniform_source_length_exclusion line 31
3. def OAI.Erdos970.NumberTheoryLean.SourceLengthExclusion.longReferenceWords line 54
4. theorem OAI.Erdos970.NumberTheoryLean.SourceLengthExclusion.literal_reference_length_exclusion line 57
5. theorem OAI.Erdos970.NumberTheoryLean.ReferenceClearanceFailure.admitted_even_endpoint line 79
6. theorem OAI.Erdos970.NumberTheoryLean.ReferenceClearanceFailure.reference_clearance_failure_prefix line 95
7. theorem OAI.Erdos970.NumberTheoryLean.SourceThresholdRate.source_prime_threshold_probability line 133
8. theorem OAI.Erdos970.NumberTheoryLean.WeightedNearThreshold.weighted_near_threshold_prefix_mass line 199
9. theorem OAI.Erdos970.NumberTheoryLean.ReferenceClearanceMass.uniform_reference_clearance_failure_mass line 277
10. theorem OAI.Erdos970.NumberTheoryLean.ReferenceRepeatedExclusion.uniform_reference_repeated_mass line 329
11. theorem OAI.Erdos970.NumberTheoryLean.BasicRegularMass.basic_regular_defect_mass line 372
12. theorem OAI.Erdos970.NumberTheoryLean.ReferenceIsolatedExclusion.uniform_reference_nonisolated_mass line 434