OAI/NumberTheory/Ostmann/SharpSieveSpacing.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.SharpSieve.reduced_nat_fraction_cross_injective line 8
2. theorem OAI.Ostmann.SharpSieve.reduced_nat_fraction_real_injective line 24
3. theorem OAI.Ostmann.SharpSieve.reduced_nat_fraction_rat_injective line 34
4. theorem OAI.Ostmann.SharpSieve.rational_spacing_mod_one line 44
5. theorem OAI.Ostmann.SharpSieve.rational_spacing_circle line 88
6. def OAI.Ostmann.SharpSieve.ReducedFrequency line 100
7. instance OAI.Ostmann.SharpSieve.(instance at line 103) line 103
8. def OAI.Ostmann.SharpSieve.ReducedFrequency.denominator line 117
9. def OAI.Ostmann.SharpSieve.ReducedFrequency.numerator line 119
10. def OAI.Ostmann.SharpSieve.ReducedFrequency.value line 121
11. def OAI.Ostmann.SharpSieve.ReducedFrequency.point line 124
12. theorem OAI.Ostmann.SharpSieve.ReducedFrequency.denominator_pos line 127
13. theorem OAI.Ostmann.SharpSieve.ReducedFrequency.denominator_le line 129
14. theorem OAI.Ostmann.SharpSieve.ReducedFrequency.numerator_lt line 131
15. theorem OAI.Ostmann.SharpSieve.ReducedFrequency.coprime line 134
16. theorem OAI.Ostmann.SharpSieve.ReducedFrequency.value_nonneg line 137
17. theorem OAI.Ostmann.SharpSieve.ReducedFrequency.value_lt_one line 140
18. theorem OAI.Ostmann.SharpSieve.ReducedFrequency.value_injective line 144
19. theorem OAI.Ostmann.SharpSieve.ReducedFrequency.mod_one_spacing line 151
20. theorem OAI.Ostmann.SharpSieve.ReducedFrequency.dist_spacing line 157
21. theorem OAI.Ostmann.SharpSieve.ReducedFrequency.point_injective line 163
22. theorem OAI.Ostmann.SharpSieve.ReducedFrequency.pairwise_dist line 172