Commit 2024-10-20 13:19 e7b15d2c

feat(Analysis/Complex/Positivity): new file (#17862) This adds results of the kind "if f is an entire function with all iterated derivatives at a point c nonnegative real, then f z is nonnegative real for z = c + r with r nonnegative real". From EulerProducts. This will be needed for the proof that $L(\chi, 1) \ne 0$ for nontrivial quadratic Dirichlet characters $\chi$ (which in turn is necessary for Dirichlet's Theorem on primes in arithmetic progressions; see PNT+).