OAI/NumberTheory/Ostmann/ZeroDensity/ActualZeros.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.ZeroDensity.NonprincipalPrimitiveFamily line 12
2. instance OAI.Ostmann.ZeroDensity.(instance at line 15) line 15
3. def OAI.Ostmann.ZeroDensity.ZeroOccurrence line 20
4. instance OAI.Ostmann.ZeroDensity.(instance at line 25) line 25
5. def OAI.Ostmann.ZeroDensity.ZeroOccurrence.point line 33
6. def OAI.Ostmann.ZeroDensity.retainedZeros line 35
7. def OAI.Ostmann.ZeroDensity.totalZeroCount line 40
8. theorem OAI.Ostmann.ZeroDensity.ZeroOccurrence.isNontrivialZero line 43
9. theorem OAI.Ostmann.ZeroDensity.totalZeroCount_le_none line 46
10. theorem OAI.Ostmann.ZeroDensity.totalZeroCount_antitone line 55
11. theorem OAI.Ostmann.ZeroDensity.totalZeroCount_pos_of_zero line 64
12. theorem OAI.Ostmann.ZeroDensity.actual_zero_density_exp_sum_le line 74