English
If HasSum (fun n => expSeries 𝕜 R n fun _ => x.fst) e holds, then the HasSum of the full extension equals the sum of the left component and the right component, specifically HasSum (fun n => expSeries 𝕜 (tsze R M) n fun _ => x) (inl e + inr (e • x.snd)).
Русский
Если имеет место HasSum (fun n => expSeries 𝕜 R n fun _ => x.fst) e, то HasSum для полного расширения равен сумме левой и правой компонент: HasSum (fun n => expSeries 𝕜 (tsze R M) n fun _ => x) (inl e + inr (e • x.snd)).
LaTeX
$$$$ HasSum\\big(\\lambda n,\\ expSeries 𝕜 (tsze R M) n (\\_ => x)\\big) = inl e + inr (e \\cdot x.snd) $$$$
Lean4
/-- If `NormedSpace.exp R x.fst` converges to `e`
then `NormedSpace.exp R x` converges to `inl e + inr (e • x.snd)`. -/
theorem hasSum_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 => expSeries 𝕜 (tsze R M) n fun _ => x) (inl e + inr (e • x.snd)) :=
by
have : HasSum (fun n => fst (expSeries 𝕜 (tsze R M) n fun _ => x)) e := by simpa [fst_expSeries] using h
simpa only [inl_fst_add_inr_snd_eq] using
(hasSum_inl _ <| this).add (hasSum_inr _ <| hasSum_snd_expSeries_of_smul_comm 𝕜 x hx h)
