English
Let x ∈ tsze R M and hx be as above. If e is the sum of the exponential series on the first component, i.e., HasSum (fun n => expSeries 𝕜 R n fun _ => x.fst) e, then the snd-component HasSum for the full extension satisfies HasSum (fun n => snd (expSeries 𝕜 (tsze R M) n fun _ => x)) (e • x.snd).
Русский
Пусть x ∈ tsze R M и hx как выше. Если e является суммой экспоненциального ряда по первой компоненте, то HasSum для snd-части полного расширения равносилен: HasSum (fun n => snd (expSeries 𝕜 (tsze R M) n fun _ => x)) (e • x.snd).
LaTeX
$$$$ HasSum\\big(\\lambda n,\\ snd(\\expSeries 𝕜 (tsze R M) n (\\_ => x))\\big)\\; (e \\cdot x.snd) $$$$
Lean4
/-- If `NormedSpace.exp R x.fst` converges to `e`
then `(NormedSpace.exp R x).snd` converges to `e • x.snd`. -/
theorem hasSum_snd_expSeries_of_smul_comm (x : tsze R M) (hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd) {e : R}
(h : HasSum (fun n => expSeries 𝕜 R n fun _ => x.fst) e) :
HasSum (fun n => snd (expSeries 𝕜 (tsze R M) n fun _ => x)) (e • x.snd) :=
by
rw [← hasSum_nat_add_iff' 1]
simp_rw [snd_expSeries_of_smul_comm _ _ hx]
simp_rw [expSeries_apply_eq] at *
rw [Finset.range_one, Finset.sum_singleton, Nat.factorial_zero, Nat.cast_one, pow_zero, inv_one, one_smul, snd_one,
sub_zero]
exact h.smul_const _
