not_LSeriesSummable_at_one — Mathlib

English

For modulus N > 0, the L-series of a Dirichlet character does not converge absolutely at s = 1.

Русский

Для модуля N > 0 L-ряд Дирихле не сходится абсолютно в s = 1.

LaTeX

$$$\neg L(\uparrow χ)(1)\quad \text{для } N > 0.$$$

Lean4

/-- The L-series of a Dirichlet character mod `N > 0` does not converge absolutely at `s = 1`. -/
theorem not_LSeriesSummable_at_one {N : ℕ} (hN : N ≠ 0) (χ : DirichletCharacter ℂ N) : ¬LSeriesSummable (↗χ) 1 :=
  by
  refine fun h ↦ (Real.not_summable_indicator_one_div_natCast hN 1) ?_
  refine h.norm.of_nonneg_of_le (fun m ↦ Set.indicator_apply_nonneg (fun _ ↦ by positivity)) (fun n ↦ ?_)
  simp only [norm_term_eq, Set.indicator, Set.mem_setOf_eq]
  split_ifs with h₁ h₂
  · simp [h₂]
  · simp [h₁, χ.map_one]
  all_goals positivity

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