OAI/NumberTheory/DirichletL/Detector/GramIdealSummation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbeGramCommon.gramIdealNorm line 13
2. lemma OAI.SevenEighths.ProbeGramCommon.gramIdealNorm_pos line 15
3. lemma OAI.SevenEighths.ProbeGramCommon.gramIdealNorm_one_le line 19
4. theorem OAI.SevenEighths.ProbeGramCommon.supportedIdeal_rpow_summable line 23
5. theorem OAI.SevenEighths.ProbeGramCommon.supportedIdeal_rpow_finite_bound line 36
6. lemma OAI.SevenEighths.ProbeGramCommon.ideal_sum_min_power_bound line 48
7. lemma OAI.SevenEighths.ProbeGramCommon.gram_ideal_term_bound line 56
8. theorem OAI.SevenEighths.ProbeGramCommon.gram_supported_double_sum line 85
9. theorem OAI.SevenEighths.ProbeGramCommon.gram_supported_exceptional_sum line 111