InfiniteSymmetric.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.CompleteHomogeneous
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 open Set Filter
10 open scoped Topology Classical
11 set_option maxHeartbeats 800000
12 
13 theorem summable_norm_positive_powers {ι : Type*} {a : ι → ℂ}
14     (ha : Summable (fun i => ‖a i‖)) {m : ℕ} (hm : 0 < m) :
15     Summable (fun i => ‖a i ^ m‖) := by
16   apply ha.of_norm_bounded_eventually
17   filter_upwards [ha.tendsto_cofinite_zero.eventually (gt_mem_nhds (by norm_num : (0 : ℝ) < 1))] with i hi
18   simp only [norm_norm, norm_pow]
19   simpa using pow_le_pow_of_le_one (norm_nonneg (a i)) hi.le hm
20 
21 @[simp] theorem homogeneousCoeff_zero (q : ℕ → ℂ) : homogeneousCoeff q 0 = 1 := by
22   simp [homogeneousCoeff, PowerSeries.coeff_zero_eq_constantCoeff]
23 
24 theorem homogeneousCoeff_succ (q : ℕ → ℂ) (n : ℕ) :
25     homogeneousCoeff q (n + 1) =
26       (∑ k ∈ Finset.range (n + 1), homogeneousCoeff q k * q (n - k + 1)) / (n + 1 : ℂ) := by
27   apply (eq_div_iff (by exact_mod_cast Nat.succ_ne_zero n : (n + 1 : ℂ) ≠ 0)).mpr
28   simpa only [mul_comm] using homogeneousCoeff_recurrence q n
29 
30 theorem homogeneousCoeff_continuous (n : ℕ) : Continuous (fun q : ℕ → ℂ => homogeneousCoeff q n) := by
31   induction n using Nat.strong_induction_on with
32   | h n ih =>
33       cases n with
34       | zero => simpa using (continuous_const : Continuous (fun _ : ℕ → ℂ => (1 : ℂ)))
35       | succ n =>
36           simp_rw [homogeneousCoeff_succ]
37           apply Continuous.div_const
38           apply continuous_finsetSum
39           intro k hk
40           exact (ih k (Finset.mem_range.mp hk)).mul (continuous_apply _)
41 
42 theorem homogeneousSeries_congr_positive {q Q : ℕ → ℂ} (h : ∀ m, 0 < m → q m = Q m) :
43     homogeneousSeries q = homogeneousSeries Q := by
44   have he : powerSumLog q = powerSumLog Q := by
45     ext n
46     simp only [powerSumLog, PowerSeries.coeff_mk]
47     by_cases hn : n = 0
48     · simp [hn]
49     · rw [h n (Nat.pos_of_ne_zero hn)]
50   rw [homogeneousSeries, homogeneousSeries, he]
51 
52 def completeHomogeneous {ι : Type*} (a : ι → ℂ) (n : ℕ) : ℂ :=
53   homogeneousCoeff (fun m => ∑' i, a i ^ m) n
54 
55 theorem finiteHomogeneousSeries_coefficient_limit {ι : Type*} {a : ι → ℂ}
56     (ha : Summable (fun i => ‖a i‖)) (n : ℕ) :
57     Tendsto (fun S : Finset ι => PowerSeries.coeff n (finiteHomogeneousSeries a S))
58       atTop (𝓝 (completeHomogeneous a n)) := by
59   let q : Finset ι → ℕ → ℂ := fun S m => if m = 0 then 0 else ∑ i ∈ S, a i ^ m
60   let Q : ℕ → ℂ := fun m => if m = 0 then 0 else ∑' i, a i ^ m
61   have ht : Tendsto q atTop (𝓝 Q) := by
62     apply tendsto_pi_nhds.mpr
63     intro m
64     by_cases hm : m = 0
65     · simp [q, Q, hm]
66     · simpa only [q, Q, ite_eq_right hm] using! (summable_norm_positive_powers ha (Nat.pos_of_ne_zero hm)).of_norm.hasSum
67   have h := (homogeneousCoeff_continuous n).tendsto Q |>.comp ht
68   change Tendsto (fun S => homogeneousCoeff (q S) n) atTop (𝓝 (homogeneousCoeff Q n)) at h
69   have he (S : Finset ι) : homogeneousSeries (q S) = homogeneousSeries (fun m => ∑ i ∈ S, a i ^ m) :=
70     homogeneousSeries_congr_positive (fun m hm => by simp [q, hm.ne'])
71   have hE : homogeneousSeries Q = homogeneousSeries (fun m => ∑' i, a i ^ m) :=
72     homogeneousSeries_congr_positive (fun m hm => by simp [Q, hm.ne'])
73   simpa only [Function.comp_def, homogeneousCoeff, he, hE, completeHomogeneous,
74     finiteHomogeneousSeries_eq_homogeneous] using! h
75 
76 /-- The infinite-variable meaning is the limit of the actual finite monomial sums. -/
77 theorem completeHomogeneous_monomial_limit {ι : Type*} {a : ι → ℂ}
78     (ha : Summable (fun i => ‖a i‖)) (n : ℕ) :
79     Tendsto (fun S : Finset ι => ∑ l ∈ S.finsuppAntidiag n, ∏ i ∈ S, a i ^ (l i))
80       atTop (𝓝 (completeHomogeneous a n)) := by
81   simpa only [finiteHomogeneousSeries_monomials] using finiteHomogeneousSeries_coefficient_limit ha n
82 
83 def repeatedEigenvalue {ι : Type*} (a : ι → ℂ) (r : ℕ) : ι × Fin r → ℂ := fun p => a p.1
84 
85 theorem repeatedEigenvalue_norm_summable {ι : Type*} {a : ι → ℂ}
86     (ha : Summable (fun i => ‖a i‖)) (r : ℕ) : Summable (fun p => ‖repeatedEigenvalue a r p‖) := by
87   apply (summable_prod_of_nonneg (fun p => norm_nonneg (repeatedEigenvalue a r p))).mpr
88   refine ⟨fun i => (hasSum_fintype _).summable, ?_⟩
89   simpa [repeatedEigenvalue, tsum_fintype, nsmul_eq_mul] using ha.mul_left (r : ℝ)
90 
91 theorem repeatedEigenvalue_powerSum {ι : Type*} {a : ι → ℂ}
92     (ha : Summable (fun i => ‖a i‖)) (r : ℕ) {m : ℕ} (hm : 0 < m) :
93     (∑' p, repeatedEigenvalue a r p ^ m) = (r : ℂ) * ∑' i, a i ^ m := by
94   have hs := (summable_norm_positive_powers (repeatedEigenvalue_norm_summable ha r) hm).of_norm
95   rw [hs.tsum_prod]
96   simp [repeatedEigenvalue, tsum_fintype, nsmul_eq_mul, tsum_mul_left]
97 
98 theorem reciprocalSeries_eq_homogeneous_zero_sums {N : ℕ} (hN : 2 ≤ N) (r : ℂ) :
99     reciprocalSeries N r = homogeneousSeries (fun m => r * zeroPowerSum (entireReducedDenominator N) m) := by
100   have hd : PowerSeries.derivative ℂ (powerSumLog (fun m => r * zeroPowerSum (entireReducedDenominator N) m)) =
101       PowerSeries.C r * PowerSeries.derivative ℂ (negativeLogDenominator N) := by
102     ext n
103     rw [powerSumLog_derivative_coeff, PowerSeries.coeff_C_mul, PowerSeries.coeff_derivative,
104       ← kappaCoeff_eq_zeroPowerSum hN (Nat.succ_pos n)]
105     simp [kappaCoeff, mul_comm]
106   apply powerSeries_linear_ode_unique (H := PowerSeries.C r * PowerSeries.derivative ℂ (negativeLogDenominator N))
107   · simp [constantCoeff_reciprocalSeries]
108   · rw [derivative_reciprocalSeries]; ring
109   · rw [homogeneousSeries_derivative, hd]
110 
111 theorem reciprocalCoeff_completeHomogeneous {N : ℕ} (hN : 2 ≤ N) (n r : ℕ) :
112     reciprocalCoeff N n (r : ℂ) / ((N * n).factorial : ℂ) =
113       completeHomogeneous (repeatedEigenvalue
114         (fun i : ZeroMultiplicityIndex (entireReducedDenominator N) => (indexedZero i)⁻¹) r) n := by
115   have ha : Summable (fun i : ZeroMultiplicityIndex (entireReducedDenominator N) => ‖(indexedZero i)⁻¹‖) := by
116     simpa [norm_inv, one_div] using zeroMultiplicity_reciprocal_summable
117       (entireReducedDenominator_reciprocal_zeros_summable hN)
118   have he : homogeneousSeries (fun m => ∑' p, repeatedEigenvalue
119       (fun i : ZeroMultiplicityIndex (entireReducedDenominator N) => (indexedZero i)⁻¹) r p ^ m) =
120       homogeneousSeries (fun m => (r : ℂ) * zeroPowerSum (entireReducedDenominator N) m) := by
121     apply homogeneousSeries_congr_positive
122     intro m hm
123     simpa only [zeroPowerSum, one_div, inv_pow] using repeatedEigenvalue_powerSum ha r hm
124   change ((N * n).factorial : ℂ) * PowerSeries.coeff n (reciprocalSeries N (r : ℂ)) /
125       ((N * n).factorial : ℂ) = _
126   rw [mul_div_cancel_left₀ _ (by exact_mod_cast (N * n).factorial_ne_zero),
127     reciprocalSeries_eq_homogeneous_zero_sums hN]
128   exact congrArg (PowerSeries.coeff n) he.symm
129 
130 /-- Arbitrary complex r has the exact Bell-polynomial continuation of these power sums. -/
131 theorem reciprocalCoeff_symmetric_polynomial_continuation {N : ℕ} (hN : 2 ≤ N) (n : ℕ) (r : ℂ) :
132     reciprocalCoeff N n r = ((N * n).factorial : ℂ) / (n.factorial : ℂ) *
133       completeExponentialBell n (fun m => r * ((m - 1).factorial : ℂ) *
134         zeroPowerSum (entireReducedDenominator N) m) := reciprocalCoeff_zero_sum_bell hN n r
135 
136 end
137 end Komorebi.PaperIV

Back to source controls