English
For x not integer, the logarithmic derivative of sin(π t)/(π t) with respect to t at x equals π cot(π x) − 1/x.
Русский
При x ≠ целое, логарифмическая производная sin(π t)/(π t) по t в точке x равна π cot(π x) − 1/x.
LaTeX
$$$$\forall x \in \mathbb{C}, \; x \notin \mathbb{Z}, \; \logDeriv\Big( t \mapsto \frac{\sin(\pi t)}{\pi t} \Big)\,x = \pi \cot(\pi x) - \frac{1}{x}.$$$$
Lean4
theorem logDeriv_sin_div_eq_cot (hz : x ∈ ℂ_ℤ) :
logDeriv (fun t ↦ (Complex.sin (π * t) / (π * t))) x = π * cot (π * x) - 1 / x :=
by
have : (fun t ↦ (Complex.sin (π * t) / (π * t))) = fun z ↦ (Complex.sin ∘ fun t ↦ π * t) z / (π * z) := by simp
rw [this,
logDeriv_div _ (by apply sin_pi_mul_ne_zero hz) ?_
(DifferentiableAt.comp _ (Complex.differentiableAt_sin) (by fun_prop)) (by fun_prop),
logDeriv_comp (Complex.differentiableAt_sin) (by fun_prop), Complex.logDeriv_sin, deriv_const_mul _ (by fun_prop),
deriv_id'', logDeriv_const_mul, logDeriv_id']
· field_simp
· simp
· simp only [ne_eq, mul_eq_zero, ofReal_eq_zero, not_or]
exact ⟨Real.pi_ne_zero, integerComplement.ne_zero hz⟩
