BellCompletion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ParameterThetaCompletion
6 
7 /-!
8 # Complete exponential Bell coefficients
9 
10 The Bell coefficients are defined by their standard generating function,
11 independently of the reciprocal family. The specialization below proves the
12 exact normalization in Theorem 7.2, including the parameter degree.
13 -/
14 
15 namespace Komorebi.PaperIV
16 open scoped PowerSeries
17 noncomputable section
18 variable {K : Type*} [Field K] [CharZero K]
19 
20 /-- The zero-constant EGF input used to define the complete Bell polynomials. -/
21 def bellInput (x : ℕ → K) : K⟦X⟧ :=
22   PowerSeries.mk fun m => if m = 0 then 0 else x m / (m.factorial : K)
23 
24 /-- The standard complete exponential Bell coefficient, normalized by `n!`. -/
25 def completeExponentialBell (n : ℕ) (x : ℕ → K) : K :=
26   (n.factorial : K) *
27     PowerSeries.coeff n ((PowerSeries.exp K).subst (bellInput x))
28 
29 omit [CharZero K] in
30 @[simp] theorem constantCoeff_bellInput (x : ℕ → K) :
31     (bellInput x).constantCoeff = 0 := by
32   simp [bellInput]
33 
34 /-- Generating-function normalization, including the zeroth coefficient. -/
35 theorem completeExponentialBell_generating_coefficient (n : ℕ) (x : ℕ → K) :
36     PowerSeries.coeff n ((PowerSeries.exp K).subst (bellInput x)) =
37       completeExponentialBell n x / (n.factorial : K) := by
38   have hn : (n.factorial : K) ≠ 0 := by exact_mod_cast n.factorial_ne_zero
39   simp [completeExponentialBell, hn]
40 
41 @[simp] theorem completeExponentialBell_zero (x : ℕ → K) :
42     completeExponentialBell 0 x = 1 := by
43   simp only [completeExponentialBell, Nat.factorial_zero, Nat.cast_one, one_mul,
44     PowerSeries.coeff_zero_eq_constantCoeff]
45   change MvPowerSeries.constantCoeff ((PowerSeries.exp K).subst (bellInput x)) = 1
46   rw [PowerSeries.constantCoeff_subst_of_constantCoeff_zero (constantCoeff_bellInput x)]
47   simp
48 
49 /-- The logarithmic normalization gives exactly the Bell input in Paper IV. -/
50 theorem bellInput_reciprocal (N : ℕ) (r : K) :
51     bellInput (fun m => r * ((m - 1).factorial : K) * kappaCoeff N m) =
52       PowerSeries.C r * negativeLogDenominator N := by
53   ext m
54   cases m with
55   | zero => simp [bellInput, constantCoeff_negativeLogDenominator,
56       PowerSeries.coeff_zero_eq_constantCoeff]
57   | succ m =>
58     simp only [bellInput, PowerSeries.coeff_mk, Nat.succ_ne_zero, ↓reduceIte,
59       Nat.succ_sub_one, kappaCoeff, PowerSeries.coeff_C_mul]
60     rw [Nat.factorial_succ, Nat.cast_mul]
61     have hm : (m.factorial : K) ≠ 0 := by exact_mod_cast m.factorial_ne_zero
62     have hs : (m.succ : K) ≠ 0 := by exact_mod_cast Nat.succ_ne_zero m
63     field_simp
64 
65 /-- Theorem 7.2: the exact Bell formula, for every coefficient and parameter. -/
66 theorem reciprocalCoeff_bell_formula (N n : ℕ) (r : K) :
67     reciprocalCoeff N n r =
68       ((N * n).factorial : K) / (n.factorial : K) *
69         completeExponentialBell n
70           (fun m => r * ((m - 1).factorial : K) * kappaCoeff N m) := by
71   rw [completeExponentialBell, bellInput_reciprocal, reciprocalCoeff, blockCoeff,
72     reciprocalSeries, formalExpFamily_eq_exp_subst (constantCoeff_negativeLogDenominator N)]
73   have hn : (n.factorial : K) ≠ 0 := by exact_mod_cast n.factorial_ne_zero
74   field_simp
75 
76 theorem coeff_one_negativeLogDenominator (N : ℕ) :
77     PowerSeries.coeff 1 (negativeLogDenominator (R := K) N) =
78       (N.factorial : K)⁻¹ := by
79   rw [negativeLogDenominator, map_neg,
80     coeff_one_logOf_of_constantCoeff_one (constantCoeff_reducedDenominator N),
81     coeff_reducedDenominator]
82   simp only [Nat.mul_one, pow_one, map_div₀, map_neg, map_one, map_natCast]
83   ring
84 
85 /-- Exact leading parameter coefficient of the reciprocal polynomial. -/
86 theorem coeff_reciprocalCoeffPolynomialOver_parameterDegree (N n : ℕ) :
87     (reciprocalCoeffPolynomialOver (K := K) N n).coeff n =
88       ((N * n).factorial : K) /
89         ((n.factorial : K) * (N.factorial : K) ^ n) := by
90   let L : K⟦X⟧ := negativeLogDenominator (R := K) N
91   let Cφ : K →ₐ[ℚ] Polynomial K :=
92     (Polynomial.CAlgHom : K →ₐ[K] Polynomial K).restrictScalars ℚ
93   have hmapL : PowerSeries.map Polynomial.C L =
94       negativeLogDenominator (R := Polynomial K) N := by
95     have h := map_negativeLogDenominator Cφ N
96     have hc : (Cφ : K →+* Polynomial K) = Polynomial.C := by
97       ext x
98       simp [Cφ]
99     simpa only [hc] using h
100   rw [reciprocalCoeffPolynomialOver, reciprocalCoeff, blockCoeff,
101     reciprocalSeries, ← hmapL]
102   rw [show ((N * n).factorial : Polynomial K) =
103       Polynomial.C ((N * n).factorial : K) by simp]
104   rw [Polynomial.coeff_C_mul,
105     coeff_parameterDegree_formalExpFamily_map_C L
106       (constantCoeff_negativeLogDenominator N)]
107   simp only [L, coeff_one_negativeLogDenominator, inv_pow]
108   ring
109 
110 /-- The degree is exact, not merely bounded above. -/
111 theorem natDegree_reciprocalCoeffPolynomialOver (N n : ℕ) :
112     (reciprocalCoeffPolynomialOver (K := K) N n).natDegree = n := by
113   apply Polynomial.natDegree_eq_of_le_of_coeff_ne_zero
114     (natDegree_reciprocalCoeffPolynomialOver_le N n)
115   rw [coeff_reciprocalCoeffPolynomialOver_parameterDegree]
116   apply div_ne_zero
117   · exact_mod_cast (N * n).factorial_ne_zero
118   · apply mul_ne_zero
119     · exact_mod_cast n.factorial_ne_zero
120     · apply pow_ne_zero
121       exact_mod_cast N.factorial_ne_zero
122 
123 /-- The parameter factor holds over every characteristic-zero field. -/
124 theorem X_dvd_reciprocalCoeffPolynomialOver (N : ℕ) {n : ℕ} (hn : 0 < n) :
125     Polynomial.X ∣ reciprocalCoeffPolynomialOver (K := K) N n := by
126   rw [Polynomial.X_dvd_iff]
127   have h := eval_reciprocalCoeffPolynomialOver (K := K) N n 0
128   rw [reciprocalCoeff_zero_parameter_of_pos N hn] at h
129   rw [Polynomial.coeff_zero_eq_eval_zero]
130   exact h
131 
132 end
133 end Komorebi.PaperIV

Back to source controls