exp(tsum) = tprod(exp)

Stream: mathlib4

[Michael Stoll]

What would be the right generality for the following statement?

import Mathlib.Analysis.SpecialFunctions.Exp

open BigOperators Complex

lemma HasSum.cexp {ι} {f : ι → ℂ} {a : ℂ} (h : HasSum f a) : HasProd (cexp ∘ f) (cexp a) :=
  Filter.Tendsto.congr (fun s ↦ exp_sum s f) <| Filter.Tendsto.cexp h

(It's a one-line proof, but I think it would make sense to have it as an explicit statement.)

[Floris van Doorn]

LGTM

[Eric Wieser]

Bonus points if you can add it for docs#NormedSpace.exp too

[Michael Stoll]

What can I do with these bonus points? :smile:

[Jireh Loreaux]

spend them when you apply this lemma later on in more generality than ℂ :smile:

[Michael Stoll]

import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Analysis.SpecialFunctions.Exponential

open BigOperators

variable {𝕂 𝔸 : Type*} [RCLike 𝕂]

variable [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] in
open Topology in
lemma Filter.Tendsto.NormedSpace_exp {l : Filter α} {f : α → 𝔸} {a : 𝔸} (hf : Tendsto f l (𝓝 a)) :
    Tendsto (fun x => NormedSpace.exp 𝕂 (f x)) l (𝓝 (NormedSpace.exp 𝕂 a)) :=
  (NormedSpace.exp_continuous.tendsto _).comp hf

variable  [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] in
open Filter in
lemma HasSum.NormedSpace_exp {ι} {f : ι → 𝔸} {a : 𝔸} (h : HasSum f a) :
    HasProd (NormedSpace.exp 𝕂 ∘ f) (NormedSpace.exp 𝕂 a) :=
  Tendsto.congr (fun s ↦ NormedSpace.exp_sum s f) <| Tendsto.NormedSpace_exp h

open Real in
lemma HasSum.rexp {ι} {f : ι → ℝ} {a : ℝ} (h : HasSum f a) : HasProd (rexp ∘ f) (rexp a) :=
  exp_eq_exp_ℝ ▸ h.NormedSpace_exp

open Complex in
lemma HasSum.cexp {ι} {f : ι → ℂ} {a : ℂ} (h : HasSum f a) : HasProd (cexp ∘ f) (cexp a) :=
  exp_eq_exp_ℂ ▸ h.NormedSpace_exp

[Michael Stoll]

I'll make a PR after the snooker session...

[Michael Stoll]

#12635

[Michael Stoll]

... and before the next one starts :billiards: