differentiable_Gammaℝ_inv — Mathlib

English

The reciprocal map s ↦ Γℝ(s)^{-1} is complex-differentiable.

Русский

Обратная к функции Γℝ по комплексной переменной дифференцируема.

LaTeX

$$$$ s \mapsto \Gamma_{\mathbb{R}}(s)^{-1} \text{ is differentiable on } \mathbb{C}. $$$$

Lean4

theorem differentiable_Gammaℝ_inv : Differentiable ℂ (fun s ↦ (Gammaℝ s)⁻¹) :=
  by
  conv => enter [2, s]; rw [Gammaℝ, mul_inv]
  refine Differentiable.mul (fun s ↦ .inv ?_ (by simp [pi_ne_zero])) ?_
  · refine ((differentiableAt_id.neg.div_const (2 : ℂ)).const_cpow ?_)
    exact Or.inl (ofReal_ne_zero.mpr pi_ne_zero)
  · exact differentiable_one_div_Gamma.comp (differentiable_id.div_const _)

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