differentiableAt_Gamma — Mathlib

English

On the real line, the Gamma function is differentiable at every nonnegative pole-excluded point.

Русский

На вещественной оси функция Гамма дифференцируема во всех точках, исключая полюсы.

LaTeX

$$$$ \text{Differentiable}_{\mathbb{R}}( \Gamma ) \text{ on } \mathbb{R} \setminus \{ -m : m \in \mathbb{N} \}. $$$$

Lean4

@[fun_prop]
theorem differentiableAt_Gamma {s : ℝ} (hs : ∀ m : ℕ, s ≠ -m) : DifferentiableAt ℝ Gamma s :=
  by
  refine (Complex.differentiableAt_Gamma _ ?_).hasDerivAt.real_of_complex.differentiableAt
  simp_rw [← Complex.ofReal_natCast, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]
  exact hs

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