Commit 2024-11-18 07:41 6d297a41

View on Github →

feat(NumberTheory/LSeries/Nonvanishing): new file (#19043) This is a substantial step on the way to PNT and Dirichlet's Theorem: it adds the fact that the L-function of a Dirichlet character does not vanish on the closed right half-plane Re(s) ≥ 1. From EulerProducts. See here on Zulip.

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/LSeries/Nonvanishing.lean

added theorem DirichletCharacter.LFunctionTrivChar_isBigO_near_one_horizontal

added theorem DirichletCharacter.LFunction_apply_one_ne_zero

added theorem DirichletCharacter.LFunction_isBigO_horizontal

added theorem DirichletCharacter.LFunction_ne_zero_of_one_le_re

added theorem DirichletCharacter.LFunction_ne_zero_of_re_eq_one

added theorem DirichletCharacter.norm_LFunction_product_ge_one

added theorem DirichletCharacter.norm_LSeries_product_ge_one

added theorem DirichletCharacter.summable_neg_log_one_sub_mul_prime_cpow

added theorem riemannZeta_ne_zero_of_one_le_re