OAI/NumberTheory/Ostmann/Construction/ActualTestBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.Construction.residueTest_norm_le_prime line 12
2. lemma OAI.Ostmann.Construction.favorableGiantResidueTest_norm_le_prime line 29
3. def OAI.Ostmann.Construction.primeSourceBound line 45
4. lemma OAI.Ostmann.Construction.primeSourceBound_nonneg line 47
5. lemma OAI.Ostmann.Construction.primeSource_le_bound line 50
6. lemma OAI.Ostmann.Construction.residueTest_re_abs_le_source line 53
7. lemma OAI.Ostmann.Construction.favorableGiantResidueTest_re_abs_le_source line 58