differentiableAt_Gamma_nat_add_one

English

Gamma is differentiable at every point n+1 with respect to ℂ; i.e., DifferentiableAt_ℂ Γ (n+1).

Русский

Гамма-функция дифференцируема в точке n+1 по комплексному числу.

LaTeX

$$DifferentiableAt_\mathbb{C}}(\Gamma)(n+1)$$

Lean4

theorem differentiableAt_Gamma_nat_add_one (n : ℕ) : DifferentiableAt ℂ Gamma (n + 1) :=
  by
  refine differentiableAt_Gamma _ (fun m ↦ ?_)
  simp only [Ne, ← ofReal_natCast, ← ofReal_one, ← ofReal_add, ← ofReal_neg, ofReal_inj, eq_neg_iff_add_eq_zero]
  positivity

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