OAI/NumberTheory/Ostmann/ZeroDensity/Target.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.ZeroDensity.PrimitiveFamily line 14
2. instance OAI.Ostmann.ZeroDensity.(instance at line 17) line 17
3. instance OAI.Ostmann.ZeroDensity.(instance at line 22) line 22
4. theorem OAI.Ostmann.ZeroDensity.card_primitiveFamily_le line 24
5. def OAI.Ostmann.ZeroDensity.smoothError line 46
6. def OAI.Ostmann.ZeroDensity.totalPrimitiveError line 51
7. theorem OAI.Ostmann.ZeroDensity.totalPrimitiveError_nonneg line 57
8. theorem OAI.Ostmann.ZeroDensity.totalPrimitiveError_none line 63
9. theorem OAI.Ostmann.ZeroDensity.totalPrimitiveError_some line 69