Λ — Mathlib · SciLib

English

Λ is the meromorphic function obtained by subtracting the simple poles 1/s f0 and ε/(k−s) g0 from Λ₀; this aligns Λ with the Mellin transform in the presence of the pole corrections.

Русский

Λ — полуприводимая функция, равная Λ₀ минус простые полюса; т.е. Λ(s) = Λ₀(s) − (1/s) f0 − (ε/(k−s)) g0.

LaTeX

$$Λ(s) := Λ₀(s) − (1 / s) • f₀ − (ε / (k − s)) • g₀$$

Lean4

/-- A meromorphic function which agrees with the Mellin transform of `f - f₀` where defined -/
def Λ (s : ℂ) : E :=
  P.Λ₀ s - (1 / s) • P.f₀ - (P.ε / (P.k - s)) • P.g₀

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