English
If s has Re(s) > 1 and χ is a Dirichlet character modulo N, then the Dirichlet summand is norm-summable: ∑_{n≥1} ||dirichletSummandHom χ(ne_zero_of_one_lt_re hs) n|| < ∞.
Русский
При Re(s) > 1 и χ — Дирихлетов символ по модулю N, сумма Дирихлетовых слагаемых сходится по норме: ∑ ||dirichletSummandHom χ(ne_zero_of_one_lt_re hs) n|| < ∞.
LaTeX
$$$\forall N, \forall χ, \forall hs: 1 < \Re(s), \; \sum_{n=1}^{\infty} \big\|\operatorname{dirichletSummandHom}(χ)(ne_zero_of_one_lt_re hs)(n)\big\| < \infty.$$$
Lean4
/-- If `f : α → ℂ` is summable, then so is `n ↦ log (1 - f n)`. -/
theorem clog_one_sub {α : Type*} {f : α → ℂ} (hsum : Summable f) : Summable fun n ↦ log (1 - f n) :=
by
have hg : DifferentiableAt ℂ (fun z ↦ log (1 - z)) 0 :=
by
have : 1 - 0 ∈ slitPlane := (sub_zero (1 : ℂ)).symm ▸ one_mem_slitPlane
fun_prop (disch := assumption)
have : (fun z ↦ log (1 - z)) =O[𝓝 0] id := by simpa only [sub_zero, log_one] using hg.isBigO_sub
exact this.comp_summable hsum
