GammaIntegral_eq_mellin — Mathlib

English

A reformulated reflection-type relation for 1−s: (Γℝ(1−s))^{-1} = Γℂ(s) cos(π s/2) (Γℝ(s))^{-1}.

Русский

Переформулированная отражательная формула для 1−s: (Γℝ(1−s))^{-1} = Γℂ(s) cos(π s/2) (Γℝ(s))^{-1}.

LaTeX

$$$$ (\Gamma_{\mathbb{R}}(1 - s))^{-1} = \Gamma_{\mathbb{C}}(s) \cos\left(\frac{\pi s}{2}\right) \big( \Gamma_{\mathbb{R}}(s)\big)^{-1}. $$$$

Lean4

/-- Rewrite the Gamma integral as an example of a Mellin transform. -/
theorem GammaIntegral_eq_mellin : GammaIntegral = mellin fun x => ↑(Real.exp (-x)) :=
  funext fun s => by simp only [mellin, GammaIntegral, smul_eq_mul, mul_comm]

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