English
The logarithmic derivative of 1 + sineTerm z i, at x ≡ cotTerm x i when x is in the integer complement.
Русский
Логарифмическая производная 1 + sineTerm z i в точке x равна cotTerm x i, если x не целое.
LaTeX
$$$$\forall x \in \mathbb{C}, \; x \notin \mathbb{Z}, \; \logDeriv\big( z \mapsto 1 + \text{sineTerm}(z,i)\big)\,x = \cotTerm(x,i).$$$$
Lean4
theorem logDeriv_sineTerm_eq_cotTerm (hx : x ∈ ℂ_ℤ) (i : ℕ) :
logDeriv (fun (z : ℂ) ↦ 1 + sineTerm z i) x = cotTerm x i :=
by
have h1 := integerComplement_add_ne_zero hx (i + 1)
have h2 : ((x : ℂ) - (i + 1)) ≠ 0 := by simpa [sub_eq_add_neg] using integerComplement_add_ne_zero hx (-(i + 1))
have h3 : (i + 1) ^ 2 + -x ^ 2 ≠ 0 :=
by
have := (integerComplement_pow_two_ne_pow_two hx ((i + 1) : ℤ))
rw [← sub_eq_add_neg, sub_ne_zero]
aesop
simp only [Int.cast_add, Int.cast_natCast, Int.cast_one, ne_eq, sineTerm, logDeriv_apply, deriv_const_add',
deriv_div_const, deriv.fun_neg', differentiableAt_fun_id, deriv_fun_pow, Nat.cast_ofNat, Nat.add_one_sub_one,
pow_one, deriv_id'', mul_one, cotTerm, one_div] at *
field_simp
ring
