feat(Analysis/SpecialFunctions): generating function of besselJ

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
 

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,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

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)