OAI/NumberTheory/DirichletL/Detector/NormalProduct.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbeEuler.factor_ne_zero_of_defect line 12
2. lemma OAI.SevenEighths.ProbeEuler.norm_log_le_defect line 17
3. lemma OAI.SevenEighths.ProbeEuler.log_summable_of_defect line 21
4. lemma OAI.SevenEighths.ProbeEuler.product_eq_exp_log line 29
5. lemma OAI.SevenEighths.ProbeEuler.norm_log_sum_le line 39
6. theorem OAI.SevenEighths.ProbeEuler.product_defect_le line 50
7. theorem OAI.SevenEighths.ProbeEuler.normalProduct_analytic line 58