Local Factor

Supporting definitions and lemmas for the Odlyzko-bound formalization.

noncomputable def NumberField.Odlyzko.inverseNormPower (q : ℕ) (s : ℂ) : ℂ

An inverse norm power used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.inverseNormPower q s = ↑q ^ (-s)

noncomputable def NumberField.Odlyzko.localFactor (q : ℕ) (s : ℂ) : ℂ

A local factor used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.localFactor q s = (1 - NumberField.Odlyzko.inverseNormPower q s)⁻¹

theorem NumberField.Odlyzko.norm_inverseNormPower (q : ℕ) (hq : 0 < q) (s : ℂ) : ‖inverseNormPower q s‖ = ↑q ^ (-s.re)

theorem NumberField.Odlyzko.norm_inverseNormPower_lt_one {q : ℕ} (hq : 1 < q) {s : ℂ} (hs : 0 < s.re) : ‖inverseNormPower q s‖ < 1

theorem NumberField.Odlyzko.hasSum_inverseNormPower_pow {q : ℕ} (hq : 1 < q) {s : ℂ} (hs : 0 < s.re) : HasSum (fun (e : ℕ) => inverseNormPower q s ^ e) (localFactor q s)

theorem NumberField.Odlyzko.one_sub_inverseNormPower_ne_zero {q : ℕ} (hq : 1 < q) {s : ℂ} (hs : 0 < s.re) : 1 - inverseNormPower q s ≠ 0

theorem NumberField.Odlyzko.localFactor_ne_zero {q : ℕ} (hq : 1 < q) {s : ℂ} (hs : 0 < s.re) : localFactor q s ≠ 0

theorem NumberField.Odlyzko.hasDerivAt_inverseNormPower {q : ℕ} (hq : q ≠ 0) (s : ℂ) : HasDerivAt (inverseNormPower q) (inverseNormPower q s * Complex.log ↑q * -1) s