TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.CompletedZeta.complexPlaceGammaFactor (s : ℂ) : ℂ

A complex place gamma factor used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.CompletedZeta.complexPlaceGammaFactor s = s.Gammaℂ / 2

theorem NumberField.Odlyzko.complexPlaceGammaFactor_eq (s : ℂ) : CompletedZeta.complexPlaceGammaFactor s = (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s

theorem NumberField.Odlyzko.complexPlaceGammaFactor_ne_zero_of_re_pos {s : ℂ} (hs : 0 < s.re) : CompletedZeta.complexPlaceGammaFactor s ≠ 0

theorem NumberField.Odlyzko.differentiableAt_complexPlaceGammaFactor_of_re_pos {s : ℂ} (hs : 0 < s.re) : DifferentiableAt ℂ CompletedZeta.complexPlaceGammaFactor s

theorem NumberField.Odlyzko.logDeriv_const_cpow_neg {c : ℂ} (hc : c ≠ 0) (s : ℂ) : logDeriv (fun (z : ℂ) => c ^ (-z)) s = -Complex.log c

theorem NumberField.Odlyzko.logDeriv_complexPlaceGammaFactor_of_re_pos {s : ℂ} (hs : 0 < s.re) : logDeriv CompletedZeta.complexPlaceGammaFactor s = s.digamma - Complex.log (2 * ↑Real.pi)