feat: add HasSum f a → HasProd (exp ∘ f) (exp a) (#12635)

This adds lemmas saying that ` HasSum f a`  implies `HasProd (exp ∘ f) (exp a)` for `exp = rexp, cexp, NormedSpace.exp`.

While the `rexp`  and `cexp`  versions could be deduced from the `NormedSpace.exp` one, we give a direct proof (and so avoid needing to import stuff about `NormedSpace.exp` for these results; the proofs are also a bit faster that way).

Based on the discussion below, this also renames `Filter.Tendsto.exp` to `Filter.Tendsto.rexp` for the version specific to the real exponential function, so that `Filter.Tendsto.exp` can be used for the corresponding statement involving `NormedSpace.exp`.

See [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/exp.28tsum.29.20.3D.20tprod.28exp.29/near/436891747) on Zulip.



Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Mathlib/Analysis/NormedSpace/Exponential.lean

@@ -473,6 +473,12 @@ theorem exp_continuous : Continuous (exp 𝕂 : 𝔸 → 𝔸) := by
   exact continuousOn_exp
 #align exp_continuous NormedSpace.exp_continuous
 
+open Topology in
+lemma _root_.Filter.Tendsto.exp {α : Type*} {l : Filter α} {f : α → 𝔸} {a : 𝔸}
+    (hf : Tendsto f l (𝓝 a)) :
+    Tendsto (fun x => exp 𝕂 (f x)) l (𝓝 (exp 𝕂 a)) :=
+  (exp_continuous.tendsto _).comp hf
+
 theorem exp_analytic (x : 𝔸) : AnalyticAt 𝕂 (exp 𝕂) x :=
   analyticAt_exp_of_mem_ball x ((expSeries_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 #align exp_analytic NormedSpace.exp_analytic

Mathlib/Analysis/SpecialFunctions/Exp.lean

@@ -136,23 +136,24 @@ variable {α : Type*}
 
 open Real
 
-theorem Filter.Tendsto.exp {l : Filter α} {f : α → ℝ} {z : ℝ} (hf : Tendsto f l (𝓝 z)) :
+theorem Filter.Tendsto.rexp {l : Filter α} {f : α → ℝ} {z : ℝ} (hf : Tendsto f l (𝓝 z)) :
     Tendsto (fun x => exp (f x)) l (𝓝 (exp z)) :=
   (continuous_exp.tendsto _).comp hf
-#align filter.tendsto.exp Filter.Tendsto.exp
+#align filter.tendsto.exp Filter.Tendsto.rexp
 
 variable [TopologicalSpace α] {f : α → ℝ} {s : Set α} {x : α}
 
+-- TODO: the two next theorems should be `rexp` as well
 nonrec
 theorem ContinuousWithinAt.exp (h : ContinuousWithinAt f s x) :
     ContinuousWithinAt (fun y => exp (f y)) s x :=
-  h.exp
+  h.rexp
 #align continuous_within_at.exp ContinuousWithinAt.exp
 
 @[fun_prop]
 nonrec
 theorem ContinuousAt.exp (h : ContinuousAt f x) : ContinuousAt (fun y => exp (f y)) x :=
-  h.exp
+  h.rexp
 #align continuous_at.exp ContinuousAt.exp
 
 @[fun_prop]
@@ -442,6 +443,11 @@ lemma summable_pow_mul_exp_neg_nat_mul (k : ℕ) {r : ℝ} (hr : 0 < r) :
 
 end Real
 
+open Real in
+/-- If `f` has sum `a`, then `exp ∘ f` has product `exp a`. -/
+lemma HasSum.rexp {ι} {f : ι → ℝ} {a : ℝ} (h : HasSum f a) : HasProd (rexp ∘ f) (rexp a) :=
+  Tendsto.congr (fun s ↦ exp_sum s f) <| Tendsto.rexp h
+
 namespace Complex
 
 -- Adaptation note: nightly-2024-04-01
@@ -489,3 +495,8 @@ theorem tendsto_exp_comap_re_atBot_nhdsWithin : Tendsto exp (comap re atBot) (
 #align complex.tendsto_exp_comap_re_at_bot_nhds_within Complex.tendsto_exp_comap_re_atBot_nhdsWithin
 
 end Complex
+
+open Complex in
+/-- If `f` has sum `a`, then `exp ∘ f` has product `exp a`. -/
+lemma HasSum.cexp {ι : Type*} {f : ι → ℂ} {a : ℂ} (h : HasSum f a) : HasProd (cexp ∘ f) (cexp a) :=
+  Filter.Tendsto.congr (fun s ↦ exp_sum s f) <| Filter.Tendsto.cexp h

Mathlib/Analysis/SpecialFunctions/Exponential.lean

@@ -421,3 +421,14 @@ theorem hasDerivAt_exp_smul_const' (x : 𝔸) (t : 𝕂) :
 end RCLike
 
 end exp_smul
+
+section tsum_tprod
+
+variable {𝕂 𝔸 : Type*} [RCLike 𝕂] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸]
+
+/-- If `f` has sum `a`, then `exp ∘ f` has product `exp a`. -/
+lemma HasSum.exp {ι : Type*} {f : ι → 𝔸} {a : 𝔸} (h : HasSum f a) :
+    HasProd (exp 𝕂 ∘ f) (exp 𝕂 a) :=
+  Tendsto.congr (fun s ↦ exp_sum s f) <| Tendsto.exp h
+
+end tsum_tprod