Gamma

Mathlib.Analysis.SpecialFunctions.Gamma.Basic

URI: https://scilib.ai/kg/mathlib#Real.Gamma

English

Real.Gamma(s) is the real part of the complex gamma function: Γ_R(s) = Re(Γ(s)).

Русский

Real.Gamma(s) есть действительная часть комплексной гамма-функции: Γ_R(s) = Re(Γ(s)).

LaTeX

$$$$ \mathrm{Real}\Gamma(s) = \operatorname{Re}\big( \Gamma(s) \big). $$$$

Lean4

/-- The `Γ` function (of a real variable `s`). -/
@[pp_nodot]
def Gamma (s : ℝ) : ℝ :=
  (Complex.Gamma s).re

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru