diff --git a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
index 8e892ed32827bd..cebc5c2a9e7330 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
@@ -448,7 +448,7 @@ protected theorem HasFPowerSeriesAt.deriv (h : HasFPowerSeriesAt f p x) :
   h.hasDerivAt.deriv
 
 /-- If a function is analytic on a set `s` in a complete space, so is its derivative. -/
-protected theorem AnalyticOnNhd.deriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) :
+@[fun_prop] protected theorem AnalyticOnNhd.deriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) :
     AnalyticOnNhd 𝕜 (deriv f) s :=
   (ContinuousLinearMap.apply 𝕜 F (1 : 𝕜)).comp_analyticOnNhd h.fderiv
 
diff --git a/Mathlib/Analysis/Normed/Ring/Basic.lean b/Mathlib/Analysis/Normed/Ring/Basic.lean
index ed5fcd5ae941a9..b04df8fe3865e9 100644
--- a/Mathlib/Analysis/Normed/Ring/Basic.lean
+++ b/Mathlib/Analysis/Normed/Ring/Basic.lean
@@ -786,6 +786,16 @@ theorem norm_prod (s : Finset β) (f : β → α) : ‖∏ b ∈ s, f b‖ = ∏
 theorem nnnorm_prod (s : Finset β) (f : β → α) : ‖∏ b ∈ s, f b‖₊ = ∏ b ∈ s, ‖f b‖₊ :=
   map_prod nnnormHom.toMonoidHom f s
 
+@[simp]
+theorem Multiset.norm_prod_map (s : Multiset β) (f : β → α) :
+    ‖(s.map f).prod‖ = (s.map (‖f ·‖)).prod := by
+  simpa using normHom.toMonoidHom.map_multiset_prod (s.map f)
+
+@[simp]
+theorem Multiset.nnnorm_prod_map (s : Multiset β) (f : β → α) :
+    ‖(s.map f).prod‖₊ = (s.map (‖f ·‖₊)).prod := by
+  simpa using nnnormHom.toMonoidHom.map_multiset_prod (s.map f)
+
 end SeminormedCommRing
 
 section NormedAddCommGroup
diff --git a/Mathlib/Analysis/SpecialFunctions/Bessel.lean b/Mathlib/Analysis/SpecialFunctions/Bessel.lean
index c5eec81ffe903d..1aceb61e8aee56 100644
--- a/Mathlib/Analysis/SpecialFunctions/Bessel.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Bessel.lean
@@ -8,6 +8,9 @@ module
 
 public import Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
 
+import Mathlib.Analysis.Calculus.SmoothSeries
+import Mathlib.Analysis.Complex.LocallyUniformLimit
+import Mathlib.Analysis.Normed.Module.Connected
 import Mathlib.Analysis.SpecialFunctions.Complex.Analytic
 
 /-!
@@ -37,21 +40,20 @@ $J_a(0) = 0$ for all complex $a \ne 0$. For $a = 0$, we have $J_0(0) = 1$.
 
 * Bessel function of the second kind
 * Differential equations
-* Generating functions
 * Bessel's integrals
 
 -/
 
 @[expose] public noncomputable section
 
-open Nat FormalMultilinearSeries
+open Nat FormalMultilinearSeries Topology
 
 namespace Complex
 
 local notation "F₀₁(" a ")" => regularizedHGFun 0 {(a : ℂ)}
 
 /-- Bessel function of the first kind $J_a(x)$. -/
-@[pp_nodot]
+@[pp_nodot, dlmf 10.2.E2]
 noncomputable def besselJ (a x : ℂ) := (x / 2) ^ a * F₀₁(a + 1) (- (x / 2) ^ 2)
 
 local notation "J" => besselJ
@@ -80,6 +82,7 @@ theorem analyticOnNhd_besselJ (a : ℂ) : AnalyticOnNhd ℂ (J a) slitPlane :=
   fun _ hz ↦ analyticAt_besselJ a hz
 
 /-- For integer `a`, `J a` and `J (-a)` are related by a sign. -/
+@[dlmf 10.4.E1]
 theorem besselJ_neg_int (a : ℤ) (x : ℂ) : J (-a) x = (-1) ^ a * J a x := by
   wlog! ha : 0 ≤ a
   · specialize this (-a) x (by simpa using ha.le)
@@ -118,4 +121,195 @@ theorem analyticOnNhd_besselJ_int (a : ℤ) : AnalyticOnNhd ℂ (J a) .univ :=
 theorem besselJ_zero (a : ℂ) : J a 0 = if a = 0 then 1 else 0 := by
   split_ifs with h <;> simp [besselJ, h, regularizedHGFunCoeff]
 
+@[dlmf 10.6.E1]
+theorem two_mul_self_mul_besselJ (a : ℂ) (x : ℂ) :
+    2 * a * J a x = x * J (a - 1) x + x * J (a + 1) x := by
+  by_cases h : x = 0
+  · simp [h, besselJ_zero]
+  have h : x / 2 ≠ 0 := by simp_all
+  unfold besselJ
+  calc
+    _ = 2 * (x / 2) ^ a * (a * F₀₁(a + 1) (-(x / 2) ^ 2)) := by
+      ring
+    _ = 2 * (x / 2) ^ a * F₀₁(a) (-(x / 2) ^ 2) +
+        2 * (x / 2) ^ a * (x / 2) ^ 2 * F₀₁(a + 2) (-(x / 2) ^ 2) := by
+      rw [← sub_eq_iff_eq_add.mpr (regularizedHGFun_zero_singleton_eq_mul_add_mul a (-(x / 2) ^ 2))]
+      ring_nf
+    _ = 2 * ((x / 2) ^ (a - 1) * (x / 2) ^ (1 : ℂ)) * F₀₁(a) (-(x / 2) ^ 2) +
+        2 * (x / 2) ^ (a + 1) * (x / 2) * F₀₁(a + 2) (-(x / 2) ^ 2) := by
+      rw [← cpow_add _ _ h, sub_add_cancel, cpow_add _ _ h, cpow_one]
+      ring
+    _ = _ := by
+      rw [cpow_one]
+      ring_nf
+
+@[dlmf 10.6.E2]
+theorem mul_deriv_besselJ_eq_besselJ_add_one (a : ℂ) {x : ℂ} (h : x ∈ slitPlane) :
+    x * deriv (J a) x = a * J a x - x * J (a + 1) x := by
+  have hx2 : x / 2 ∈ slitPlane := by simpa [slitPlane] using h
+  have hx0 : x / 2 ≠ 0 := fun h ↦ by simp_all
+  unfold besselJ
+  calc
+    _ = x * (deriv (fun x ↦ (x / 2) ^ a) x * F₀₁(a + 1) (-(x / 2) ^ 2) +
+        (x / 2) ^ a * deriv ((fun x ↦ F₀₁(a + 1) x) ∘ fun x ↦ -(x / 2) ^ 2) x) := by
+      rw [deriv_fun_mul (by fun_prop) (by fun_prop)]
+      rfl
+    _ = 2 * (x / 2) * deriv (fun x ↦ (x / 2) ^ a) x * F₀₁(a + 1) (-(x / 2) ^ 2) + x *
+        (x / 2) ^ a * (F₀₁(a + 1 + 1) (-(x / 2) ^ 2) * (-x / 2)) := by
+      rw [deriv_comp _ (by fun_prop) (by fun_prop), deriv_regularizedHGFun (by simp)]
+      simp
+      ring
+    _ = (a * (x / 2) ^ a) * F₀₁(a + 1) (-(x / 2) ^ 2) + x *
+        (x / 2) ^ a * (F₀₁(a + 1 + 1) (-(x / 2) ^ 2) * (-x / 2)) := by
+      congrm ?_ * _ + _
+      rw [_root_.deriv_cpow_const (by fun_prop) (by exact hx2)]
+      trans 2 * a * ((x / 2) ^ (a - 1) * (x / 2) ^ (1 : ℂ) * deriv (· / 2) x)
+      · norm_cast
+        ring
+      rw [← cpow_add _ _ hx0]
+      simp
+      ring
+    _ = _ := by
+      rw [cpow_add _ _ hx0, cpow_one]
+      ring
+
+@[dlmf 10.6.E2]
+theorem mul_deriv_besselJ_eq_besselJ_sub_one (a : ℂ) {x : ℂ} (h : x ∈ slitPlane) :
+    x * deriv (J a) x = x * J (a - 1) x - a * J a x := by
+  linear_combination two_mul_self_mul_besselJ a x + mul_deriv_besselJ_eq_besselJ_add_one a h
+
+@[dlmf 10.6.E1]
+theorem two_mul_deriv_besselJ (a : ℂ) {x : ℂ} (h : x ∈ slitPlane) :
+    2 * deriv (J a) x = J (a - 1) x - J (a + 1) x := by
+  have hx0 : x ≠ 0 := fun h ↦ by simp_all
+  rw [← mul_left_inj' hx0]
+  linear_combination mul_deriv_besselJ_eq_besselJ_sub_one a h +
+    mul_deriv_besselJ_eq_besselJ_add_one a h
+
+@[dlmf 10.6.E1]
+theorem two_mul_deriv_besselJ_int (a : ℤ) (x : ℂ) :
+    2 * deriv (J a) x = J (a - 1) x - J (a + 1) x := by
+  revert x
+  rw [← funext_iff]
+  apply AnalyticOnNhd.eq_of_frequently_eq (by fun_prop) (by norm_cast; fun_prop) (z₀ := 1)
+  refine (eventually_nhdsWithin_of_eventually_nhds (eventually_nhds_iff.mpr ?_)).frequently
+  exact ⟨slitPlane, fun x hx ↦ two_mul_deriv_besselJ a hx, isOpen_slitPlane, by simp⟩
+
+@[dlmf 10.6.E2]
+theorem mul_deriv_besselJ_eq_besselJ_add_one_int (a : ℤ) (x : ℂ) :
+    x * deriv (J a) x = a * J a x - x * J (a + 1) x := by
+  linear_combination x * two_mul_deriv_besselJ_int a x / 2 - two_mul_self_mul_besselJ a x / 2
+
+@[dlmf 10.6.E2]
+theorem mul_deriv_besselJ_eq_besselJ_sub_one_int (a : ℤ) (x : ℂ) :
+    x * deriv (J a) x = x * J (a - 1) x - a * J a x := by
+  linear_combination two_mul_self_mul_besselJ a x + mul_deriv_besselJ_eq_besselJ_add_one_int a x
+
+theorem norm_besselJ_le_exp {a : ℂ} (ha : 0 ≤ a.re) (x : ℂ) :
+    ‖J a x‖ ≤ ‖Gamma (a + 1)‖⁻¹ * ‖(x / 2) ^ a‖ * Real.exp (‖x / 2‖ ^ 2) := by
+  unfold besselJ
+  grw [norm_mul, regularizedHGFun_le_exp_of_one_le_re (by simpa using ha)]
+  apply le_of_eq
+  simp
+  ring
+
+theorem norm_besselJ_le_exp_int (a : ℤ) (x : ℂ) :
+    ‖J a x‖ ≤ (a.natAbs ! : ℝ)⁻¹ * ‖x / 2‖ ^ a.natAbs * Real.exp (‖x / 2‖ ^ 2) := by
+  wlog! ha : 0 ≤ a
+  · specialize this (-a) (-x) (by simpa using ha.le)
+    simpa [besselJ_neg_comm] using this
+  obtain ⟨a, rfl⟩ := Int.eq_ofNat_of_zero_le ha
+  grw [norm_besselJ_le_exp (by simp)]
+  simp [Gamma_nat_eq_factorial]
+
+-- Within a bounded set, `J a x * t ^ a` can be bounded uniformly by exp series terms.
+private theorem deriv_besselJ_mul_pow_le (t : ℂ) {s : Set ℂ} (hs : Bornology.IsBounded s) :
+    ∃ u v, ∀ a : ℤ, ∀ x ∈ s,
+      ‖J a x * t ^ a‖ ≤ (a.natAbs ! : ℝ)⁻¹ * (u ^ a.natAbs * ‖t ^ a‖) * v := by
+  obtain ⟨x, hx⟩ := hs.exists_norm_le
+  use ‖x / 2‖, Real.exp (‖x / 2‖ ^ 2)
+  intro a y hy
+  have hy' : ‖y / 2‖ ≤ ‖x / 2‖ := by
+    grw [norm_div, hx y hy, le_abs_self x]
+    simp
+  grw [norm_mul, norm_besselJ_le_exp_int, hy', hy']
+  apply le_of_eq
+  ring
+
+-- The uniform bound on `J a x * t ^ a` is summable
+private theorem summable_bound (u v : ℝ) (t : ℂ) :
+    Summable fun a : ℤ ↦ (a.natAbs ! : ℝ)⁻¹ * (u ^ a.natAbs * ‖t ^ a‖) * v := by
+  refine summable_int_iff_summable_nat_and_neg.mpr ⟨?_, ?_⟩
+  · simpa [mul_pow] using
+      (NormedSpace.exp_series_hasSum_exp' (𝕂 := ℝ) (u * ‖t‖)).summable.mul_right v
+  · simpa [mul_pow] using
+      (NormedSpace.exp_series_hasSum_exp' (𝕂 := ℝ) (u * ‖t‖⁻¹)).summable.mul_right v
+
+theorem analyticOnNhd_tsum_besselJ_mul_pow (t : ℂ) :
+    AnalyticOnNhd ℂ (∑' a : ℤ, J a · * t ^ a) Set.univ := by
+  refine (analyticOnNhd_iff_differentiableOn isOpen_univ).mpr fun x _ ↦ ?_
+  obtain ⟨u, v, h⟩ := deriv_besselJ_mul_pow_le t (Metric.isBounded_ball (x := x) (r := 1))
+  exact differentiableOn_tsum_of_summable_norm (summable_bound u v t)
+    (fun _ _ _ ↦ AnalyticAt.differentiableWithinAt (by fun_prop)) Metric.isOpen_ball h
+    |>.differentiableAt (Metric.ball_mem_nhds _ (by simp)) |>.differentiableWithinAt
+
+theorem summable_besselJ_mul_pow (x : ℂ) (t : ℂ) : Summable (fun a : ℤ ↦ J a x * t ^ a) := by
+  obtain ⟨u, v, h⟩ := deriv_besselJ_mul_pow_le t (Bornology.isBounded_singleton (x := x))
+  exact (summable_bound u v t).of_norm_bounded fun a ↦ h a x (Set.mem_singleton x)
+
+@[dlmf 10.12.E1]
+theorem tsum_besselJ_mul_pow (x : ℂ) {t : ℂ} (ht : t ≠ 0) :
+    ∑' a : ℤ, J a x * t ^ a = exp ((x / 2) * (t - t⁻¹)) := by
+  -- It sufficies to prove the equality in a ball at x = 0 where LHS is non-zero
+  have : ∀ᶠ x in nhds 0, ∑' a : ℤ, J a x * t ^ a ≠ 0 := by
+    apply (analyticOnNhd_tsum_besselJ_mul_pow t).continuous.continuousAt.eventually_ne
+    simp [besselJ_zero]
+  obtain ⟨r, hr0, hr⟩ := Metric.eventually_nhds_iff_ball.mp this
+  revert x
+  rw [← funext_iff]
+  refine (analyticOnNhd_tsum_besselJ_mul_pow t).eq_of_eventuallyEq (fun x hx ↦ by fun_prop)
+    (Metric.eventually_nhds_iff_ball.mpr ⟨r, hr0, ?_⟩) (z₀ := 0)
+  -- It sufficies to prove that both sides agree on logDeriv, because they agree at x = 0
+  suffices Set.EqOn (logDeriv fun x ↦ ∑' a : ℤ, J a x * t ^ a)
+      (logDeriv fun x ↦ cexp (x / 2 * (t - t⁻¹))) (Metric.ball 0 r) by
+    obtain ⟨k, hk0, hk⟩ := logDeriv_eqOn_iff
+      ((analyticOnNhd_tsum_besselJ_mul_pow t).differentiableOn.mono (by simp))
+      (by fun_prop) Metric.isOpen_ball Metric.isPreconnected_ball (by simp) hr |>.mp this
+    have hk1 : k = 1 := by simpa [besselJ_zero] using (hk (show 0 ∈ _ by simpa using hr0)).symm
+    simpa [hk1, Set.EqOn] using hk
+  intro x hx
+  calc
+    _ = deriv (∑' a : ℤ, J a · * t ^ a) x / ∑' a : ℤ, J a x * t ^ a := by rw [logDeriv_apply]
+    _ = (∑' a : ℤ, deriv (J a · * t ^ a) x) / ∑' a : ℤ, J a x * t ^ a := by
+      obtain ⟨u, v, h⟩ := deriv_besselJ_mul_pow_le t (Metric.isBounded_ball (x := 0) (r := r))
+      rw [hasSum_deriv_of_summable_norm (summable_bound u v t)
+        (fun _ _ _ ↦ AnalyticAt.differentiableWithinAt (by fun_prop)) Metric.isOpen_ball h hx
+        |>.tsum_eq]
+    _ = (∑' a : ℤ, (J (a - 1) x - J (a + 1) x) * t ^ a) / 2 / ∑' a : ℤ, J a x * t ^ a := by
+      simp [← two_mul_deriv_besselJ_int, ← tsum_div_const, mul_assoc]
+    _ = (∑' a : ℤ, (J (a - 1) x * t ^ (a - 1) * t - J (a + 1) x * t ^ (a + 1) * t⁻¹)) /
+        2 / ∑' a : ℤ, J a x * t ^ a := by
+      simp_rw [sub_mul, ← zpow_neg_one, mul_assoc, ← zpow_add_one₀ ht, ← zpow_add₀ ht]
+      simp
+    _ = ((∑' a : ℤ, J (a - 1) x * t ^ (a - 1)) * t - (∑' a : ℤ, J (a + 1) x * t ^ (a + 1)) * t⁻¹) /
+        2 / ∑' a : ℤ, J a x * t ^ a := by
+      rw [Summable.tsum_sub ?_ ?_]
+      · simp_rw [tsum_mul_right]
+      · simpa using ((Equiv.subRight 1).summable_iff.mpr (summable_besselJ_mul_pow x t)).mul_right t
+      · simpa using ((Equiv.addRight 1).summable_iff.mpr
+          (summable_besselJ_mul_pow x t)).mul_right t⁻¹
+    _ = ((∑' a : ℤ, J a x * t ^ a) * t - (∑' a : ℤ, J a x * t ^ a) * t⁻¹) /
+        2 / ∑' a : ℤ, J a x * t ^ a := by
+      congrm (?_ * _ - ?_ * _) / _ / _
+      · simpa using (Equiv.subRight 1).tsum_eq (fun a : ℤ ↦ J a x * t ^ a)
+      · simpa using (Equiv.addRight 1).tsum_eq (fun a : ℤ ↦ J a x * t ^ a)
+    _ = (t - t⁻¹) / 2 := by field [hr x hx]
+    _ = _ := by
+      rw [logDeriv_apply, deriv_cexp (by fun_prop)]
+      simp [field]
+
+theorem hasSum_besselJ_mul_pow (x : ℂ) {t : ℂ} (ht : t ≠ 0) :
+    HasSum (fun a : ℤ ↦ J a x * t ^ a) (exp ((x / 2) * (t - t⁻¹))) :=
+  (summable_besselJ_mul_pow x t).hasSum_iff.mpr (tsum_besselJ_mul_pow x ht)
+
 end Complex
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
index 8aea69baf71696..58aa6ccf9de3c7 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
@@ -316,6 +316,19 @@ theorem Gamma_add_one (s : ℂ) (h2 : s ≠ 0) : Gamma (s + 1) = s * Gamma s :=
   rw [Gamma_eq_GammaAux s n t1, Gamma_eq_GammaAux (s + 1) n t2, GammaAux_recurrence1 s n t1]
   field
 
+theorem norm_Gamma_le_norm_Gamma_add_one {s : ℂ} (hs : 1 ≤ ‖s‖) :
+    ‖Gamma s‖ ≤ ‖Gamma (s + 1)‖ := by
+  grw [Gamma_add_one _ (by contrapose hs; simp [hs]), norm_mul, ← hs, one_mul]
+
+/-- This bound is not tight and is provided for convenience. -/
+theorem norm_Gamma_le_norm_Gamma_add_of_one_le_re {s : ℂ} (hs : 1 ≤ s.re) (n : ℕ) :
+    ‖Gamma s‖ ≤ ‖Gamma (s + n)‖ := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    grw [ih, norm_Gamma_le_norm_Gamma_add_one (le_trans (by simp; grind) (Complex.re_le_norm _))]
+    simp [add_assoc]
+
 theorem Gamma_eq_integral {s : ℂ} (hs : 0 < s.re) : Gamma s = GammaIntegral s :=
   Gamma_eq_GammaAux s 0 (by norm_cast; linarith)
 
diff --git a/Mathlib/Analysis/SpecialFunctions/RegularizedHypergeometric.lean b/Mathlib/Analysis/SpecialFunctions/RegularizedHypergeometric.lean
index 853a81d44a7a0b..a05e6313c34fd0 100644
--- a/Mathlib/Analysis/SpecialFunctions/RegularizedHypergeometric.lean
+++ b/Mathlib/Analysis/SpecialFunctions/RegularizedHypergeometric.lean
@@ -8,6 +8,8 @@ module
 public import Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
 public import Mathlib.Analysis.SpecialFunctions.Gamma.Beta
 
+import Mathlib.Topology.Algebra.InfiniteSum.ContinuousEval
+
 /-! # Generalized hypergeometric function
 
 In this file we define the generalized hypergeometric function as well as the Gaussian
@@ -67,6 +69,8 @@ variable {a : Multiset ℂ} {b : Multiset ℂ} {n m : ℕ} {j k : ℂ}
 def regularizedHGFunCoeff (a : Multiset ℂ) (b : Multiset ℂ) (n : ℕ) : ℂ :=
   (a.map (ascPochhammer ℂ n).eval).prod / (n ! * (b.map (Gamma <| · + n)).prod)
 
+local notation "C" => regularizedHGFunCoeff
+
 attribute [grind .] Nat.factorial_ne_zero
 
 @[grind =]
@@ -122,6 +126,51 @@ theorem regularizedHGFunCoeff_add_one_div_self (h : regularizedHGFunCoeff a b n
       grind [Multiset.prod_eq_zero, Multiset.mem_map]
     simp [regularizedHGFunCoeff_eq_zero_right a b n 0, h₁]
 
+variable (a) in
+theorem mul_regularizedHGFunCoeff_of_mem_right (n : ℕ) {u : ℂ} (h : u ∈ b) :
+    (u - 1 + n) * C a b n = C a ((u - 1) ::ₘ b.erase u) n := by
+  by_cases h0 : u - 1 + n = 0
+  · symm
+    simp [h0, regularizedHGFunCoeff_eq_zero_iff]
+  unfold regularizedHGFunCoeff
+  rw [mul_div, mul_comm, mul_div_assoc]
+  suffices (u - 1 + n) / (n ! * (Multiset.map (fun x ↦ Gamma (x + n)) b).prod) =
+      1 / (n ! * (Multiset.map (fun x ↦ Gamma (x + n)) ((u - 1) ::ₘ b.erase u)).prod) by
+    rw [this]
+    ring
+  calc
+    _ = (u - 1 + n) / (n ! * (Gamma (u - 1 + n + 1)) *
+        (Multiset.map (fun x ↦ Gamma (x + n)) (b.erase u)).prod) := by
+      rw [← Multiset.prod_map_erase h]
+      ring_nf
+    _ = (u - 1 + n) / ((u - 1 + n) *
+        (n ! * (Gamma (u - 1 + n)) * (Multiset.map (fun x ↦ Gamma (x + n)) (b.erase u)).prod)) := by
+      rw [Complex.Gamma_add_one _ h0]
+      ring
+    _ = 1 / (n ! * (Multiset.map (fun x ↦ Gamma (x + n)) ((u - 1) ::ₘ b.erase u)).prod) := by
+      rw [← div_div, div_self h0, Multiset.map_cons, Multiset.prod_cons]
+      ring
+
+theorem mul_regularizedHGFunCoeff (n : ℕ) :
+    (n + 1) * regularizedHGFunCoeff a b (n + 1) =
+      a.prod * regularizedHGFunCoeff (a.map (· + 1)) (b.map (· + 1)) n := by
+  unfold regularizedHGFunCoeff
+  simp only [Nat.cast_add, Nat.cast_one, Multiset.map_map, Function.comp_apply]
+  calc
+    _ = (a.map ((ascPochhammer ℂ (n + 1)).eval ·)).prod /
+        (n ! * (b.map (fun x ↦ Gamma (x + (n + 1)))).prod) := by
+      rw [Nat.factorial_succ]
+      push_cast
+      field
+    _ = a.prod * (a.map fun x ↦ (ascPochhammer ℂ n).eval (x + 1)).prod /
+        (n ! * (b.map (fun x ↦ Gamma (x + (n + 1)))).prod) := by
+      simp [ascPochhammer, Multiset.prod_map_mul]
+    _ = a.prod * (a.map fun x ↦ (ascPochhammer ℂ n).eval (x + 1)).prod /
+        (n ! * (b.map (fun x ↦ Gamma (x + 1 + n))).prod) := by
+      congrm _ / (_ * (b.map fun x ↦ Gamma $(by ring)).prod)
+    _ = _ := by
+      ring
+
 @[simp]
 theorem regularizedHGFunCoeff_zero_neg_nat_add_one (n i : ℕ) :
     regularizedHGFunCoeff 0 {-(n : ℂ) + 1} (i + n) = regularizedHGFunCoeff 0 {(n : ℂ) + 1} i := by
@@ -299,6 +348,58 @@ theorem radius_regularizedHGFunSeries_ge_one (h : a.card = b.card + 1) :
     rw [radius_regularizedHGFunSeries_eq_top_of_finite hj h']
     simp
 
+private theorem regularizedHGFun_zero_singleton_eq_mul_add_mul_aux (u : ℂ) (n : ℕ) :
+    u * C 0 {u + 1} (n + 1) + C 0 {u + 2} n = C 0 {u} (n + 1) := by
+  suffices u * ((Gamma (u + 1 + (n + 1)))⁻¹ * ((↑ n !)⁻¹ * (n + 1 : ℂ)⁻¹)) +
+      (Gamma (u + 2 + n))⁻¹ * (↑ n !)⁻¹ = (Gamma (u + (n + 1)))⁻¹ * ((↑ n !)⁻¹ * (n + 1 : ℂ)⁻¹) by
+    simpa [regularizedHGFunCoeff, Nat.factorial_succ]
+  calc
+    _ = u * ((Gamma (u + (n + 1) + 1))⁻¹ * ((↑ n !)⁻¹ * (n + 1 : ℂ)⁻¹)) +
+        (Gamma (u + (n + 1) + 1))⁻¹ * (↑ n !)⁻¹ := by
+      ring_nf
+    _ = (Gamma (u + (n + 1) + 1))⁻¹ * (↑ n !)⁻¹ * (u * (n + 1 : ℂ)⁻¹ + 1) := by
+      ring
+    _ = (Gamma (u + (n + 1)))⁻¹ * ((↑ n !)⁻¹ * (n + 1 : ℂ)⁻¹) := by
+      by_cases h : u + (n + 1) = 0
+      · have h' : u * (n + 1 : ℂ)⁻¹ + 1 = 0 := by
+          rw [eq_neg_iff_add_eq_zero.mpr h, neg_mul, mul_inv_cancel₀ (by norm_cast), neg_add_cancel]
+        simp [h, h']
+      · rw [Gamma_add_one _ h, mul_inv]
+        field
+
+theorem regularizedHGFun_zero_singleton_eq_mul_add_mul (u : ℂ) (z : ℂ) :
+    regularizedHGFun 0 {u} z =
+      u * regularizedHGFun 0 {u + 1} z + z * regularizedHGFun 0 {u + 2} z := by
+  have hsummable1: Summable fun n ↦ z ^ n * C 0 {u + 1} n := by
+    simpa using (regularizedHGFunSeries 0 {u + 1}).summable (by simp)
+  have hsummable2 : Summable fun n ↦ u * (z ^ (n + 1) * C 0 {u + 1} (n + 1)) :=
+    (hsummable1.comp_injective (add_left_injective 1)).mul_left u
+  have hsummable3 : Summable fun n ↦ z * (z ^ n * C 0 {u + 2} n) := by
+    apply Summable.mul_left
+    simpa using (regularizedHGFunSeries 0 {u + 2}).summable (by simp)
+  have hsummable4: Summable fun n ↦ z ^ n * C 0 {u} n := by
+    simpa using (regularizedHGFunSeries 0 {u}).summable (by simp : z ∈ _)
+  symm
+  suffices u * ∑' n, z ^ n * C 0 {u + 1} n + z * ∑' n, z ^ n * C 0 {u + 2} n =
+      ∑' n, z ^ n * C 0 {u} n by
+    simpa [regularizedHGFun, FormalMultilinearSeries.sum]
+  calc
+    _ = u * C 0 {u + 1} 0 + (∑' n, u * (z ^ (n + 1) * C 0 {u + 1} (n + 1)) +
+        ∑' n, z * (z ^ n * C 0 {u + 2} n)) := by
+      rw [hsummable1.tsum_eq_zero_add]
+      simp [tsum_mul_left]
+      ring
+    _ = u * C 0 {u + 1} 0 + ∑' n, (u * (z ^ (n + 1) * C 0 {u + 1} (n + 1)) +
+        z * (z ^ n * C 0 {u + 2} n)) := by
+      rw [Summable.tsum_add hsummable2 hsummable3]
+    _ = u * C 0 {u + 1} 0 + ∑' n, z ^ (n + 1) * (u * C 0 {u + 1} (n + 1) + C 0 {u + 2} n) :=
+      congr(_ + ∑' n, $(by ring))
+    _ = u * C 0 {u + 1} 0 + ∑' n, z ^ (n + 1) * C 0 {u} (n + 1) :=
+      congr(_ + ∑' n, _ * $(regularizedHGFun_zero_singleton_eq_mul_add_mul_aux u n))
+    _ = ∑' n, z ^ n * C 0 {u} n := by
+      conv_rhs => rw [hsummable4.tsum_eq_zero_add]
+      simpa using mul_regularizedHGFunCoeff_of_mem_right 0 0 (Multiset.mem_singleton_self (u + 1))
+
 theorem analyticOnNhd_regularizedHGFun_of_card_eq_add_one (h : a.card = b.card + 1) :
     AnalyticOnNhd ℂ (regularizedHGFun a b) (Metric.eball 0 1) := by
   apply (regularizedHGFunSeries a b).analyticOnNhd.mono
@@ -331,6 +432,48 @@ theorem regularizedHGFun_zero_singleton_neg_nat_add_one (n : ℕ) (z : ℂ) :
     _ = _ := by
       simp [regularizedHGFun, FormalMultilinearSeries.sum]
 
+section Derivative
+
+private theorem summable_deriv_HGF {z : ℂ} (hz : ‖z‖ₑ < (regularizedHGFunSeries a b).radius) :
+    Summable fun n ↦ z ^ n • (regularizedHGFunSeries a b).derivSeries.coeff n := by
+  have hball : z ∈ Metric.eball 0 (regularizedHGFunSeries a b).radius := by simpa using hz
+  have hdball : z ∈ Metric.eball 0 (regularizedHGFunSeries a b).derivSeries.radius := by
+    simpa using hz.trans_le (FormalMultilinearSeries.radius_le_radius_derivSeries _)
+  simpa using ((regularizedHGFunSeries a b).derivSeries).summable hdball
+
+theorem deriv_regularizedHGFun {z : ℂ} (hz : ‖z‖ₑ < (regularizedHGFunSeries a b).radius) :
+    deriv (regularizedHGFun a b) z =
+      a.prod * regularizedHGFun (a.map (· + 1)) (b.map (· + 1)) z := by
+  unfold regularizedHGFun deriv
+  rw [FormalMultilinearSeries.fderiv_sum hz]
+  suffices ∑' n, z ^ n * ((n + 1) * C a b (n + 1)) =
+      a.prod * ∑' n, z ^ n * C (a.map (· + 1)) (b.map (· + 1)) n by
+    simpa [FormalMultilinearSeries.sum, tsum_apply (summable_deriv_HGF hz)]
+  rw [← tsum_mul_left]
+  congr with n
+  rw [mul_regularizedHGFunCoeff]
+  ring
+
+end Derivative
+
+theorem regularizedHGFun_le_exp_of_one_le_re (h : ∀ u ∈ b, 1 ≤ u.re) (z : ℂ) :
+    ‖regularizedHGFun 0 b z‖ ≤ ‖(b.map Gamma).prod‖⁻¹ * Real.exp ‖z‖ := by
+  rw [Real.exp_eq_exp_ℝ]
+  apply HasSum.norm_le_of_bounded ((regularizedHGFunSeries 0 b).hasSum (by simp : z ∈ _))
+    ((NormedSpace.exp_series_hasSum_exp' (𝕂 := ℝ) ‖z‖).mul_left ‖(b.map Gamma).prod‖⁻¹)
+  intro n
+  suffices ‖(Multiset.map (fun x ↦ Gamma (x + ↑n)) b).prod‖⁻¹ ≤ ‖(b.map Gamma).prod‖⁻¹ by
+    grw [← this]
+    apply le_of_eq
+    simp [regularizedHGFunCoeff]
+    ring
+  simp_rw [Multiset.norm_prod_map, ← Multiset.prod_map_inv]
+  apply Multiset.prod_map_le_prod_map₀ _ _ (by simp)
+  intro u hu
+  apply inv_le_of_inv_le₀ (by grind [inv_pos, norm_pos_iff, neg_re, natCast_re])
+  rw [inv_inv]
+  apply norm_Gamma_le_norm_Gamma_add_of_one_le_re (h u hu)
+
 section ZeroZero
 
 /-- The regularized hypergeometric series with `a = b = 0` is exponential series. -/