feat(Analysis/SpecialFunctions): generating function of besselJ

Author: wwylele

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

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,7 +40,6 @@ $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
 
 -/
@@ -203,4 +205,111 @@ 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

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)
 

Mathlib/Analysis/SpecialFunctions/RegularizedHypergeometric.lean

@@ -456,6 +456,24 @@ theorem deriv_regularizedHGFun {z : ℂ} (hz : ‖z‖ₑ < (regularizedHGFunSer
 
 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. -/