English
For any k ∈ ℤ and a ∈ Fin(2) → ℤ, the function z ↦ (a0 z + a1)^(-k) is differentiable on the set {z ∈ ℂ | Im(z) > 0}, with the case a ≠ 0 giving the usual z^(-k) differentiability and a = 0 giving a constant function.
Русский
Для любого k ∈ ℤ и a ∈ Fin(2) → ℤ функция z ↦ (a0 z + a1)^(-k) дифференцируема на {z ∈ ℂ | Im(z) > 0}; если a ≠ 0 — обычная дифференцируемость z^(-k), если a = 0 — константа.
LaTeX
$$$\text{DifferentiableOn}_{\mathbb{C}}(z \mapsto (a_0 z + a_1)^{-k})\{ z : \Im z > 0\}$ (в случае $a=0$ функция константа).$$
Lean4
/-- Auxiliary lemma showing that for any `k : ℤ` the function `z → 1/(c*z+d)^k` is
differentiable on `{z : ℂ | 0 < z.im}`. -/
theorem div_linear_zpow_differentiableOn (k : ℤ) (a : Fin 2 → ℤ) :
DifferentiableOn ℂ (fun z : ℂ => (a 0 * z + a 1) ^ (-k)) {z : ℂ | 0 < z.im} :=
by
rcases ne_or_eq a 0 with ha | rfl
· apply DifferentiableOn.zpow
· fun_prop
· left
exact fun z hz ↦ linear_ne_zero ⟨z, hz⟩ ((comp_ne_zero_iff _ Int.cast_injective Int.cast_zero).mpr ha)
· simp only [Pi.zero_apply, Int.cast_zero, zero_mul, add_zero]
apply differentiableOn_const
