deriv_LFunction_eq_deriv_LSeries — Mathlib

English

The derivative of the L-function equals the derivative of the corresponding L-series: d/ds LFunction χ s = d/ds LSeries (χ ·) s, for s with Re(s) > 1.

Русский

Производная L-функции χ равна производной соответствующей L-цифры: d/ds LFunction χ s = d/ds LSeries (χ ·) s, при Re(s) > 1.

LaTeX

$$deriv(LFunction χ) s = deriv(LSeries (χ ·)) s$$

Lean4

theorem deriv_LFunction_eq_deriv_LSeries (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
    deriv (LFunction χ) s = deriv (LSeries (χ ·)) s :=
  by
  refine Filter.EventuallyEq.deriv_eq ?_
  have h : {z | 1 < z.re} ∈ nhds s := (isOpen_lt continuous_const continuous_re).mem_nhds hs
  filter_upwards [h] with z hz
  exact LFunction_eq_LSeries χ hz

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