English
For any complex z, the series ∑_{n=0}^∞ (z i)^{2n}/(2n)! converges to cos z.
Русский
Для любого комплексного z ряд ∑_{n=0}^∞ (z i)^{2n}/(2n)! сходится и даёт cos z.
LaTeX
$$$\\text{HasSum}\\left(n : \\mathbb{N} \\mapsto \\frac{(z \\cdot \\mathrm{i})^{2n}}{(2n)!}\\right)\\big(\\cos z\\big).$$$
Lean4
theorem hasSum_cos' (z : ℂ) : HasSum (fun n : ℕ => (z * Complex.I) ^ (2 * n) / ↑(2 * n)!) (Complex.cos z) :=
by
rw [Complex.cos, Complex.exp_eq_exp_ℂ]
have := ((expSeries_div_hasSum_exp ℂ (z * Complex.I)).add (expSeries_div_hasSum_exp ℂ (-z * 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, ← two_mul, neg_mul, mul_neg,
neg_div, add_neg_cancel, zero_div, add_zero, mul_div_cancel_left₀ _ (two_ne_zero : (2 : ℂ) ≠ 0)]
