English
For each natural n, the map s ↦ GammaAux(n)(s) is differentiable provided 1 − Re(s) < n and s is not a negative integer.
Русский
Для каждого натурального n отображение s ↦ GammaAux(n)(s) дифференцируемо при условии 1 − Re(s) < n и s ≠ −m.
LaTeX
$$$$ \text{Differentiable}_{\mathbb{C}}\big( s \mapsto \Gamma_{\mathrm{Aux}}(n)(s) \big) \quad \text{if } 1 - \mathrm{Re}(s) < n \text{ and } s \neq -m. $$$$
Lean4
@[fun_prop]
theorem differentiableAt_Gamma (s : ℂ) (hs : ∀ m : ℕ, s ≠ -m) : DifferentiableAt ℂ Gamma s :=
by
let n := ⌊1 - s.re⌋₊ + 1
have hn : 1 - s.re < n := mod_cast Nat.lt_floor_add_one (1 - s.re)
apply (differentiableAt_GammaAux s n hn hs).congr_of_eventuallyEq
let S := {t : ℂ | 1 - t.re < n}
have : S ∈ 𝓝 s := by
rw [mem_nhds_iff]; use S
refine ⟨Subset.rfl, ?_, hn⟩
have : S = re ⁻¹' Ioi (1 - n : ℝ) := by ext; rw [preimage, Ioi, mem_setOf_eq, mem_setOf_eq, mem_setOf_eq];
exact sub_lt_comm
rw [this]
exact Continuous.isOpen_preimage continuous_re _ isOpen_Ioi
apply eventuallyEq_of_mem this
intro t ht; rw [mem_setOf_eq] at ht
apply Gamma_eq_GammaAux; linarith
