OAI/NumberTheory/Jacobsthal/Primes/PrimeChoiceCoordinateMass.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.PrimeBinAlignmentMass.mass line 13
2. theorem OAI.Erdos970.NumberTheoryLean.PrimeBinAlignmentMass.mass_nonnegative line 15
3. theorem OAI.Erdos970.NumberTheoryLean.PrimeBinAlignmentMass.subset_mass_bounds line 18
4. theorem OAI.Erdos970.NumberTheoryLean.PrimeBinAlignmentMass.non_nearfull_mass line 34
5. def OAI.Erdos970.NumberTheoryLean.PrimeChoiceBoxMass.choices line 68
6. def OAI.Erdos970.NumberTheoryLean.PrimeChoiceBoxMass.weight line 69
7. def OAI.Erdos970.NumberTheoryLean.PrimeChoiceBoxMass.boxMass line 70
8. theorem OAI.Erdos970.NumberTheoryLean.PrimeChoiceBoxMass.boxMass_factorizes line 72
9. def OAI.Erdos970.NumberTheoryLean.PrimeChoiceBoxMass.alignedChoices line 75
10. theorem OAI.Erdos970.NumberTheoryLean.PrimeChoiceBoxMass.alignedChoices_eq line 79
11. theorem OAI.Erdos970.NumberTheoryLean.PrimeChoiceBoxMass.no_nearfull_box_mass line 100
12. theorem OAI.Erdos970.NumberTheoryLean.PrimeChoiceAlignmentDecay.boxMass_nonnegative line 138
13. theorem OAI.Erdos970.NumberTheoryLean.PrimeChoiceAlignmentDecay.search_power_bound line 142
14. theorem OAI.Erdos970.NumberTheoryLean.PrimeChoiceAlignmentDecay.no_nearfull_power_mass line 158
15. def OAI.Erdos970.NumberTheoryLean.PrimeChoiceCoordinateMass.coordinateEvent line 178
16. def OAI.Erdos970.NumberTheoryLean.PrimeChoiceCoordinateMass.someCoordinateEvent line 180
17. theorem OAI.Erdos970.NumberTheoryLean.PrimeChoiceCoordinateMass.weight_nonnegative line 184
18. theorem OAI.Erdos970.NumberTheoryLean.PrimeChoiceCoordinateMass.coordinate_mass_eq line 187
19. theorem OAI.Erdos970.NumberTheoryLean.PrimeChoiceCoordinateMass.coordinate_mass_bound line 201
20. theorem OAI.Erdos970.NumberTheoryLean.PrimeChoiceCoordinateMass.union_mass_le_sum line 209
21. theorem OAI.Erdos970.NumberTheoryLean.PrimeChoiceCoordinateMass.some_coordinate_mass_bound line 227