differentiable_Λ — Mathlib

English

If (f, g) is a strong FE-pair, then the completed L-function Λ is differentiable with respect to the complex variable.

Русский

Если (f, g) образуют сильную FE-пару, то Λ является дифференцируемой по комплексной переменной.

LaTeX

$$differentiable_Λ : Differentiable Complex P.Λ$$

Lean4

/-- If `(f, g)` are a strong FE pair, then the Mellin transform of `f` is entire. -/
theorem differentiable_Λ : Differentiable ℂ P.Λ := fun s ↦
  let ⟨_, ht⟩ := exists_gt s.re
  let ⟨_, hu⟩ := exists_lt s.re
  mellin_differentiableAt_of_isBigO_rpow P.hf_int (P.hf_top' _) ht (P.hf_zero' _) hu

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