LSeriesSummable_mul — Mathlib

English

Same as above: χ convolved with χ·μ equals δ.

Русский

То же самое: свертка χ с χ·μ дают δ.

LaTeX

$$$(\chi \cdot) * (\chi \cdot \mu) = \delta.$$$

Lean4

/-- The L-series of the twist of `f` by a Dirichlet character converges at `s` if the L-series
of `f` does. -/
theorem LSeriesSummable_mul {N : ℕ} (χ : DirichletCharacter ℂ N) {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) :
    LSeriesSummable (↗χ * f) s :=
  by
  refine .of_norm <| h.norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) fun n ↦ norm_term_le s ?_
  simpa using mul_le_of_le_one_left (norm_nonneg <| f n) <| χ.norm_le_one n

Похожие утверждения