English
Let z be a complex number. The complex sine function has the Maclaurin series sin z = ∑_{n=0}^∞ (-1)^n z^{2n+1}/(2n+1)!.
Русский
Пусть z — комплексное число. Функция синуса комплексного аргумента имеет степенной ряд около нуля: sin z = ∑_{n=0}^∞ (-1)^n z^{2n+1}/(2n+1)!.
LaTeX
$$$\\sin z = \\sum_{n=0}^{\\infty} (-1)^n \\frac{z^{2n+1}}{(2n+1)!}$$$
Lean4
theorem hasSum_sin' (z : ℂ) :
HasSum (fun n : ℕ => (z * Complex.I) ^ (2 * n + 1) / ↑(2 * n + 1)! / Complex.I) (Complex.sin z) :=
by
rw [Complex.sin, Complex.exp_eq_exp_ℂ]
have :=
(((expSeries_div_hasSum_exp ℂ (-z * Complex.I)).sub (expSeries_div_hasSum_exp ℂ (z * Complex.I))).mul_right
Complex.I).div_const
2
replace := (Nat.divModEquiv 2).symm.hasSum_iff.mpr this
dsimp [Function.comp_def] at this
simp_rw [← mul_comm 2 _] at this
refine this.prod_fiberwise fun k => ?_
dsimp only
convert hasSum_fintype (_ : Fin 2 → ℂ) using 1
rw [Fin.sum_univ_two]
simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ, pow_mul, mul_pow, neg_sq, sub_self, zero_mul, zero_div,
zero_add, neg_mul, mul_neg, neg_div, ← neg_add', ← two_mul, neg_mul, neg_div, mul_assoc,
mul_div_cancel_left₀ _ (two_ne_zero : (2 : ℂ) ≠ 0), Complex.div_I]
