OAI/NumberTheory/DirichletL/LatticeSummability.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.LatticeSummability.normForm_nonneg line 10
2. theorem OAI.SevenEighths.LatticeSummability.normForm_eq_zero_iff line 14
3. theorem OAI.SevenEighths.LatticeSummability.normForm_ge_half_norm_sq line 25
4. theorem OAI.SevenEighths.LatticeSummability.summable_pair_norm_rpow line 36
5. theorem OAI.SevenEighths.LatticeSummability.summable_normForm_neg_rpow line 46
6. theorem OAI.SevenEighths.LatticeSummability.summable_one_div_normForm_rpow line 69
7. theorem OAI.SevenEighths.LatticeSummability.summable_weighted_normForm line 74