OAI/NumberTheory/OrdinaryCorrelations/Elliott/PrimeDefect.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.ElliottReductions.primeDefect line 31
2. def OAI.OrdinaryCorrelations.ElliottReductions.normFunction line 34
3. lemma OAI.OrdinaryCorrelations.ElliottReductions.normFunction_oneBounded line 36
4. lemma OAI.OrdinaryCorrelations.ElliottReductions.normFunction_multiplicative line 42
5. lemma OAI.OrdinaryCorrelations.ElliottReductions.primeDefect_nonneg line 47
6. lemma OAI.OrdinaryCorrelations.ElliottReductions.primeDefect_sum_le_distanceSq line 54
7. theorem OAI.OrdinaryCorrelations.ElliottReductions.normFunction_nonpretentious_of_divergent_defect line 86