English
For Complex cosh, logDeriv equals tanh: logDeriv(Complex.cosh) = Complex.tanh.
Русский
Для комплексного cosh логарифмическая производная равна tanh.
LaTeX
$$$\logDeriv(\mathrm{Complex}.\cosh) = \mathrm{Complex}.\tanh$$$
Lean4
/-- Note this also holds for `z = 0`, but we do not need this case for `sin_pi_mul_eq`. -/
theorem integral_cos_mul_cos_pow (hn : 2 ≤ n) (hz : z ≠ 0) :
(((1 : ℂ) - (4 : ℂ) * z ^ 2 / (n : ℂ) ^ 2) * ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ n) =
(n - 1 : ℂ) / n * ∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ (n - 2) :=
by
have nne : (n : ℂ) ≠ 0 := by contrapose! hn; rw [Nat.cast_eq_zero] at hn; rw [hn]; exact zero_lt_two
have := integral_cos_mul_cos_pow_aux hn hz
rw [integral_sin_mul_sin_mul_cos_pow_eq hn hz, sub_eq_neg_add, mul_add, ← sub_eq_iff_eq_add] at this
convert congr_arg (fun u : ℂ => -u * (2 * z) ^ 2 / n ^ 2) this using 1 <;> field_simp; ring
