HypergeometricAnalytic.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.HypergeometricCompletion
6 import KomorebiPaperIV.EntireBridge
7 import Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Finset
12 
13 /-- Exactly the manuscript's denominator parameters, with the parameter 1 omitted. -/
14 def residueHypergeometricParameters (N j : ℕ) : Multiset ℂ :=
15   ((range N).erase (N-j-1)).val.map (fun a => ((j+a+1 : ℕ) : ℂ)/(N : ℂ))
16 
17 theorem residueHypergeometricParameters_card {N j : ℕ} (hj : j < N) :
18     (residueHypergeometricParameters N j).card = N-1 := by
19   rw [residueHypergeometricParameters, Multiset.card_map]
20   change ((range N).erase (N-j-1)).card = N-1
21   rw [Finset.card_erase_of_mem (show N-j-1 ∈ range N by simp; omega), card_range]
22 
23 theorem residueHypergeometricParameters_re_pos {N j : ℕ} (hN : 0 < N)
24     {c : ℂ} (hc : c ∈ residueHypergeometricParameters N j) : 0 < c.re := by
25   obtain ⟨a, _, rfl⟩ := Multiset.mem_map.mp hc
26   have hNr : (0 : ℝ) < N := by exact_mod_cast hN
27   simpa using div_pos (show (0 : ℝ) < (j+a+1 : ℕ) by positivity) hNr
28 
29 private theorem pochhammer_ratCast (q : ℕ) (x : ℚ) :
30     (((ascPochhammer ℚ q).eval x : ℚ) : ℂ) = (ascPochhammer ℂ q).eval (x : ℂ) := by
31   simpa using (Polynomial.eval_map_apply (f := Rat.castHom ℂ)
32     (p := ascPochhammer ℚ q) x).symm
33 
34 private theorem residuePochhammerProduct_erase {N j : ℕ} (hN : 0 < N) (hj : j < N) (q : ℕ) :
35     (residuePochhammerProduct N j q : ℂ) = (q.factorial : ℂ) *
36       ((residueHypergeometricParameters N j).map (ascPochhammer ℂ q).eval).prod := by
37   have ho := congrArg (fun x : ℚ => (x : ℂ))
38     (omitted_residuePochhammer_eq_factorial hN hj q)
39   simp only [pochhammer_ratCast, Rat.cast_div, Rat.cast_natCast] at ho
40   have he := Finset.mul_prod_erase (range N)
41     (fun a => (ascPochhammer ℂ q).eval (((j+a+1 : ℕ) : ℂ)/(N : ℂ)))
42     (show N-j-1 ∈ range N by simp; omega)
43   rw [ho] at he
44   rw [residuePochhammerProduct, Rat.cast_prod]
45   simp only [pochhammer_ratCast, Rat.cast_div, Rat.cast_natCast]
46   simpa only [residueHypergeometricParameters, Multiset.map_map,
47     Finset.prod_eq_multiset_prod, Function.comp_apply] using he.symm
48 
49 /-- Gamma normalization converts Mathlib's regularized coefficients to ordinary coefficients. -/
50 theorem regularized_zeroF_normalization (b : Multiset ℂ)
51     (hb : ∀ c ∈ b, ∀ k : ℕ, c ≠ -(k : ℂ)) (q : ℕ) :
52     (b.map Complex.Gamma).prod * Complex.regularizedHGFunCoeff 0 b q =
53       ((q.factorial : ℂ) * (b.map (ascPochhammer ℂ q).eval).prod)⁻¹ := by
54   have hn : (b.map Complex.Gamma).prod ≠ 0 := by
55     apply Multiset.prod_ne_zero
56     intro hc
57     obtain ⟨a, ha, he⟩ := Multiset.mem_map.mp hc
58     exact Complex.Gamma_ne_zero (hb a ha) he
59   have hp : (b.map (ascPochhammer ℂ q).eval).prod =
60       (b.map (fun c => Complex.Gamma (c+q))).prod / (b.map Complex.Gamma).prod := by
61     rw [← Multiset.prod_map_div]
62     congr 1
63     apply Multiset.map_congr rfl
64     intro c hc
65     exact (Complex.Gamma_add_nat_div_Gamma_eq c (hb c hc)).symm
66   rw [Complex.regularizedHGFunCoeff, hp]
67   simp only [Multiset.map_zero, Multiset.prod_zero, one_div]
68   field_simp
69 
70 /-- Ordinary `₀F_{N-1}` with the paper's literal parameter multiset. -/
71 def residueHypergeometric (N j : ℕ) (w : ℂ) : ℂ :=
72   ((residueHypergeometricParameters N j).map Complex.Gamma).prod *
73     Complex.regularizedHGFun 0 (residueHypergeometricParameters N j) w
74 
75 theorem residueHypergeometric_hasSum {N j : ℕ} (hN : 0 < N) (hj : j < N) (w : ℂ) :
76     HasSum (fun q => (residueZeroFCoeff N j q : ℂ) * w^q)
77       (residueHypergeometric N j w) := by
78   let b := residueHypergeometricParameters N j
79   have hb : ∀ c ∈ b, ∀ k : ℕ, c ≠ -(k : ℂ) := by
80     intro c hc k he
81     have hp := residueHypergeometricParameters_re_pos hN hc
82     rw [he] at hp
83     simp only [Complex.neg_re, Complex.natCast_re] at hp
84     have hk : (0 : ℝ) ≤ k := Nat.cast_nonneg k
85     linarith
86   have hs := (Complex.regularizedHGFunSeries 0 b).hasSum (x := w) (by
87     rw [Complex.radius_regularizedHGFunSeries_eq_top (by simp)]
88     simp)
89   have h := hs.mul_left (b.map Complex.Gamma).prod
90   change HasSum _ (residueHypergeometric N j w) at h
91   apply h.congr_fun
92   intro q
93   simp only [Complex.regularizedHGFunSeries, FormalMultilinearSeries.ofScalars_apply_eq,
94     smul_eq_mul, ← mul_assoc, regularized_zeroF_normalization b hb]
95   rw [← residuePochhammerProduct_erase hN hj]
96   simp [residueZeroFCoeff]
97 
98 /-- The pointwise hypergeometric formula, with ordinary normalization and exactly N-1 parameters. -/
99 theorem entireTransfer_hypergeometric {N j : ℕ} (hN : 0 < N) (hj : j < N)
100     {omega : ℂ} (ho : IsPrimitiveRoot omega N) (lambda z : ℂ) :
101     entireTransfer N j omega lambda z =
102       (lambda*z)^j / (j.factorial : ℂ) *
103         residueHypergeometric N j ((lambda*z)^N / (N : ℂ)^N) := by
104   let f := fun m => PowerSeries.coeff m (transferSection N j lambda) * z^m
105   have hi : Function.Injective (fun q : ℕ => N*q+j) := by
106     intro a b h
107     exact Nat.eq_of_mul_eq_mul_left hN (Nat.add_right_cancel h)
108   have hf : ∀ m, m ∉ Set.range (fun q : ℕ => N*q+j) → f m = 0 := by
109     intro m hm
110     have he : m%N ≠ j := by
111       intro he
112       apply hm
113       use m/N
114       change N*(m/N)+j=m
115       rw [← he, Nat.add_comm, Nat.mod_add_div]
116     simp [f, coeff_transferSection, transferSectionCoeff, he]
117   have ha := (hi.hasSum_iff hf).2 (hasSum_entireTransfer hN hj ho lambda z)
118   have hh := (residueHypergeometric_hasSum hN hj ((lambda*z)^N / (N : ℂ)^N)).mul_left
119     ((lambda*z)^j / (j.factorial : ℂ))
120   apply ha.unique
121   apply hh.congr_fun
122   intro q
123   dsimp [Function.comp_def, f]
124   rw [coeff_transferSection, transferSectionCoeff,
125     show (N*q+j)%N = j by simp [Nat.add_mod, Nat.mod_eq_of_lt hj]]
126   simp only [one_div, map_inv₀, map_natCast]
127   have hn := congrArg (fun a : ℚ => (a : ℂ)) (residueZeroFCoeff_normalization hN j q)
128   push_cast at hn
129   rw [← hn]
130   simp only [div_eq_mul_inv, mul_pow, inv_pow, ← pow_mul]
131   rw [pow_add, pow_add]
132   simp only [ite_true]
133   ring
134 
135 end
136 end Komorebi.PaperIV

Back to source controls