LFunction_eq_completed_div_gammaFactor

English

For χ and s with s ≠ 0 or N ≠ 1, the L-function equals the completed L-function divided by the gamma factor: L(χ,s) = completedLFunction(χ,s) / gammaFactor(χ,s).

Русский

Для χ и s с s ≠ 0 или N ≠ 1 выполняется отношение L(χ,s) = completedLFunction(χ,s) / gammaFactor(χ,s).

LaTeX

$$$L(\chi,s) = \dfrac{\text{completedLFunction}(\chi,s)}{\gamma\text{Factor}(\chi,s)}$$$

Lean4

/-- Relation between the completed L-function and the usual one. We state it this way around so
it holds at the poles of the gamma factor as well.
-/
theorem LFunction_eq_completed_div_gammaFactor (χ : DirichletCharacter ℂ N) (s : ℂ) (h : s ≠ 0 ∨ N ≠ 1) :
    LFunction χ s = completedLFunction χ s / gammaFactor χ s :=
  by
  rcases χ.even_or_odd with hχ | hχ <;> rw [hχ.gammaFactor_def]
  · exact LFunction_eq_completed_div_gammaFactor_even hχ.to_fun _ (h.imp_right χ.map_zero')
  · apply LFunction_eq_completed_div_gammaFactor_odd hχ.to_fun

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