English
The Gamma integral equals the Mellin transform of exp(−x).
Русский
Интеграл Гамма равен Меллин-трансформе экспоненты.
LaTeX
$$$$ \Gamma\text{Integral} = \mathcal{M}\left(x \mapsto e^{-x}\right). $$$$
Lean4
theorem differentiableAt_GammaAux (s : ℂ) (n : ℕ) (h1 : 1 - s.re < n) (h2 : ∀ m : ℕ, s ≠ -m) :
DifferentiableAt ℂ (GammaAux n) s := by
induction n generalizing s with
| zero =>
refine (hasDerivAt_GammaIntegral ?_).differentiableAt
rw [Nat.cast_zero] at h1; linarith
| succ n hn =>
dsimp only [GammaAux]
specialize hn (s + 1)
have a : 1 - (s + 1).re < ↑n := by rw [Nat.cast_succ] at h1; rw [Complex.add_re, Complex.one_re]; linarith
have b : ∀ m : ℕ, s + 1 ≠ -m := by
intro m; have := h2 (1 + m)
contrapose! this
rw [← eq_sub_iff_add_eq] at this
simpa using this
refine DifferentiableAt.div (DifferentiableAt.comp _ (hn a b) ?_) ?_ ?_
· rw [differentiableAt_add_const_iff (1 : ℂ)]; exact differentiableAt_id
· exact differentiableAt_id
· simpa using h2 0
