OAI/NumberTheory/Ostmann/ZeroDensity/OccurrenceCount.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.ZeroDensity.card_occurrences_eq_sum line 15
2. theorem OAI.Ostmann.ZeroDensity.local_occurrences_le_log line 42
3. def OAI.Ostmann.ZeroDensity.localMultiplicityBound line 68
4. theorem OAI.Ostmann.ZeroDensity.localMultiplicityBound_nonneg line 72
5. theorem OAI.Ostmann.ZeroDensity.retainedZeros_local_card_le line 80