OAI/NumberTheory/DirichletL/Detector/SelectedPrimeSums.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbeSelectedPrimeSums.finite_ideal_count line 11
2. lemma OAI.SevenEighths.ProbeSelectedPrimeSums.ramified_card_bound line 26
3. def OAI.SevenEighths.ProbeSelectedPrimeSums.annularPower line 37
4. lemma OAI.SevenEighths.ProbeSelectedPrimeSums.annularPower_nonneg line 39
5. lemma OAI.SevenEighths.ProbeSelectedPrimeSums.annular_rpow line 42
6. theorem OAI.SevenEighths.ProbeSelectedPrimeSums.annular_slot_majorant line 55
7. theorem OAI.SevenEighths.ProbeSelectedPrimeSums.weighted_slot_bound line 115