|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Weiyi Wang. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Weiyi Wang |
| 5 | +-/ |
| 6 | +import Mathlib.Combinatorics.Enumerative.Partition.Basic |
| 7 | +import Mathlib.RingTheory.PowerSeries.PiTopology |
| 8 | + |
| 9 | +/-! |
| 10 | +# Generating functions for partition functions |
| 11 | +
|
| 12 | +This file defines generating functions related to partitions. Given a character function $f(i, c)$ |
| 13 | +of a part $i$ and the number of the part $c$, the related generating function is |
| 14 | +$$ |
| 15 | +G_f(X) = \sum_{n = 0}^{\infty} \left(\sum_{p \in P_{n}} \prod_{i \in p} f(i, \#i)\right) X^n |
| 16 | += \prod_{i = 1}^{\infty}\left(1 + \sum_{j = 1}^{\infty} f(i, j) X^{ij}\right) |
| 17 | +$$ |
| 18 | +where $P_n$ is all partitions of $n$, $\#i$ is the count of $i$ in the partition $p$. |
| 19 | +We give the definition `Nat.Partition.genFun` using the first equation, and prove the second |
| 20 | +equation in `Nat.Partition.hasProd_genFun` (with shifted indices). |
| 21 | +
|
| 22 | +This generating function can be specialized to |
| 23 | +* When $f(i, c) = 1$, this is the generating function for partition function $p(n)$. |
| 24 | +* When $f(i, 1) = 1$ and $f(i, c) = 0$ for $c > 1$, this is the generating function for |
| 25 | + `#(Nat.Partition.distincts n)`. |
| 26 | +* When $f(i, c) = 1$ for odd $i$ and $f(i, c) = 0$ for even $i$, this is the generating function for |
| 27 | + `#(Nat.Partition.odds n)`. |
| 28 | +(TODO: prove these) |
| 29 | +
|
| 30 | +The definition of `Nat.Partition.genFun` ignores the value of $f(0, c)$ and $f(i, 0)$. The formula |
| 31 | +can be interpreted as assuming $f(i, 0) = 1$ and $f(0, c) = 0$ for $c \ne 0$. In theory we could |
| 32 | +respect the actual value of $f(0, c)$ and $f(i, 0)$, but it makes the otherwise finite sum and |
| 33 | +product potentially infinite. |
| 34 | +-/ |
| 35 | + |
| 36 | +open PowerSeries |
| 37 | +open scoped PowerSeries.WithPiTopology |
| 38 | + |
| 39 | +namespace Nat.Partition |
| 40 | +variable {M : Type*} [CommSemiring M] |
| 41 | + |
| 42 | +/-- Generating function associated with character $f(i, c)$ for partition functions, where $i$ is a |
| 43 | +part of the partition, and $c$ is the count of that part in the partition. The character function is |
| 44 | +multiplied within one `n.Partition`, and summed among all `n.Partition` for a fixed `n`. This way, |
| 45 | +each `n` is assigned a value, which we use as the coefficients of the power series. -/ |
| 46 | +def genFun (f : ℕ → ℕ → M) : M⟦X⟧ := |
| 47 | + PowerSeries.mk fun n ↦ ∑ p : n.Partition, ∏ i ∈ p.parts.toFinset, f i (p.parts.count i) |
| 48 | + |
| 49 | +variable [TopologicalSpace M] |
| 50 | + |
| 51 | +/-- The infinite sum in the formula `Nat.Partition.hasProd_genFun` always converges. -/ |
| 52 | +theorem summable_genFun_term (f : ℕ → ℕ → M) (i : ℕ) : |
| 53 | + Summable fun j ↦ f (i + 1) (j + 1) • (X : M⟦X⟧) ^ ((i + 1) * (j + 1)) := by |
| 54 | + rcases subsingleton_or_nontrivial M with h | h |
| 55 | + · simpa [Subsingleton.eq_zero] using summable_zero |
| 56 | + apply WithPiTopology.summable_of_tendsto_order_atTop_nhds_top |
| 57 | + refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩) |
| 58 | + intro m hm |
| 59 | + rw [PowerSeries.smul_eq_C_mul] |
| 60 | + refine (lt_of_lt_of_le (lt_add_of_nonneg_of_lt (by simp) ?_) (le_order_mul _ _)) |
| 61 | + rw [order_X_pow] |
| 62 | + norm_cast |
| 63 | + grind |
| 64 | + |
| 65 | +variable [T2Space M] |
| 66 | + |
| 67 | +private theorem aux_injOn_sub_one_parts {n : ℕ} (p : Partition n) : |
| 68 | + Set.InjOn (fun x ↦ x - 1) p.parts.toFinset := by |
| 69 | + intro a ha b hb |
| 70 | + exact tsub_inj_left (p.parts_pos (by simpa using ha)) (p.parts_pos (by simpa using hb)) |
| 71 | + |
| 72 | +private theorem aux_map_sub_one_parts_subset {n : ℕ} (p : Partition n) : |
| 73 | + (Multiset.map (fun x ↦ x - 1) p.parts).toFinset ⊆ Finset.range n := by |
| 74 | + intro m |
| 75 | + rw [Multiset.mem_toFinset, Finset.mem_range] |
| 76 | + suffices ∀ x ∈ p.parts, x - 1 = m → m < n by simpa |
| 77 | + rintro x h1 rfl |
| 78 | + exact Nat.sub_one_lt_of_le (p.parts_pos h1) (le_of_mem_parts h1) |
| 79 | + |
| 80 | +private theorem aux_mapsTo_sub_one_parts {n : ℕ} (p : Partition n) : |
| 81 | + Set.MapsTo (fun x ↦ x - 1) p.parts.toFinset (Finset.range n) := by |
| 82 | + intro a ha |
| 83 | + apply Finset.mem_of_subset (aux_map_sub_one_parts_subset p) |
| 84 | + rw [Multiset.mem_toFinset, Multiset.mem_map] |
| 85 | + exact ⟨a, by simpa using ha⟩ |
| 86 | + |
| 87 | +private def aux_toFinsuppAntidiag {n : ℕ} (p : Partition n) : ℕ →₀ ℕ where |
| 88 | + toFun m := p.parts.count (m + 1) * (m + 1) |
| 89 | + support := (p.parts.map (· - 1)).toFinset |
| 90 | + mem_support_toFun m := by |
| 91 | + suffices (∃ a ∈ p.parts, a - 1 = m) ↔ m + 1 ∈ p.parts by simpa |
| 92 | + trans (∃ a ∈ p.parts, a = m + 1) |
| 93 | + · refine ⟨fun ⟨a, h1, h2⟩ ↦ ⟨a, h1, ?_⟩, fun ⟨a, h1, h2⟩ ↦ ⟨a, h1, Nat.sub_eq_of_eq_add h2⟩⟩ |
| 94 | + exact Nat.eq_add_of_sub_eq (Nat.one_le_of_lt (p.parts_pos h1)) h2 |
| 95 | + · simp |
| 96 | + |
| 97 | +private theorem aux_toFinsuppAntidiag_injective (n : ℕ) : |
| 98 | + Function.Injective (aux_toFinsuppAntidiag (n := n)) := by |
| 99 | + unfold aux_toFinsuppAntidiag |
| 100 | + intro p q h |
| 101 | + rw [Finsupp.mk.injEq] at h |
| 102 | + obtain ⟨hfinset, hcount⟩ := h |
| 103 | + rw [Nat.Partition.ext_iff, Multiset.ext] |
| 104 | + intro m |
| 105 | + obtain rfl | h0 := Nat.eq_zero_or_pos m |
| 106 | + · trans 0 |
| 107 | + · rw [Multiset.count_eq_zero] |
| 108 | + exact fun h ↦ (lt_self_iff_false _).mp <| p.parts_pos h |
| 109 | + · symm |
| 110 | + rw [Multiset.count_eq_zero] |
| 111 | + exact fun h ↦ (lt_self_iff_false _).mp <| q.parts_pos h |
| 112 | + · refine Nat.eq_of_mul_eq_mul_right h0 <| ?_ |
| 113 | + convert funext_iff.mp hcount (m - 1) <;> exact (Nat.sub_eq_iff_eq_add h0).mp rfl |
| 114 | + |
| 115 | +private theorem aux_range_toFinsuppAntidiag (n : ℕ) : |
| 116 | + Set.range (aux_toFinsuppAntidiag (n := n)) ⊆ (Finset.range n).finsuppAntidiag n := by |
| 117 | + unfold aux_toFinsuppAntidiag |
| 118 | + rw [Set.range_subset_iff] |
| 119 | + intro p |
| 120 | + suffices ∑ m ∈ Finset.range n, Multiset.count (m + 1) p.parts * (m + 1) = n by |
| 121 | + simpa [aux_map_sub_one_parts_subset p] |
| 122 | + refine Eq.trans ?_ p.parts_sum |
| 123 | + simp_rw [Finset.sum_multiset_count, smul_eq_mul] |
| 124 | + refine (Finset.sum_of_injOn (· - 1) (aux_injOn_sub_one_parts p) |
| 125 | + (aux_mapsTo_sub_one_parts p) ?_ ?_).symm |
| 126 | + · suffices ∀ i ∈ Finset.range n, (∀ x ∈ p.parts, x - 1 ≠ i) → i + 1 ∉ p.parts by simpa |
| 127 | + intro i hi h |
| 128 | + contrapose! h |
| 129 | + exact ⟨i + 1, by simpa using h⟩ |
| 130 | + · intro i hi |
| 131 | + suffices i - 1 + 1 = i by simp [this] |
| 132 | + rw [Nat.sub_add_cancel (Nat.one_le_of_lt (p.parts_pos (by simpa using hi)))] |
| 133 | + |
| 134 | +private theorem aux_dvd_of_coeff_ne_zero {f : ℕ → ℕ → M} {d : ℕ} {s : Finset ℕ} |
| 135 | + {g : ℕ →₀ ℕ} (hg : g ∈ s.finsuppAntidiag d) |
| 136 | + (hprod : ∀ x ∈ s, |
| 137 | + (coeff (g x)) (1 + ∑' (j : ℕ), f (x + 1) (j + 1) • X ^ ((x + 1) * (j + 1))) ≠ (0 : M)) |
| 138 | + (x : ℕ) : x + 1 ∣ g x := by |
| 139 | + by_cases hx : x ∈ s |
| 140 | + · specialize hprod x hx |
| 141 | + contrapose! hprod |
| 142 | + rw [map_add, (summable_genFun_term f x).map_tsum _ (WithPiTopology.continuous_coeff _ _)] |
| 143 | + rw [show (0 : M) = 0 + ∑' (i : ℕ), 0 by simp] |
| 144 | + congrm (?_ + ∑' (i : ℕ), ?_) |
| 145 | + · suffices g x ≠ 0 by simp [this] |
| 146 | + contrapose! hprod |
| 147 | + simp [hprod] |
| 148 | + · rw [map_smul, coeff_X_pow] |
| 149 | + apply smul_eq_zero_of_right |
| 150 | + suffices g x ≠ (x + 1) * (i + 1) by simp [this] |
| 151 | + contrapose! hprod |
| 152 | + simp [hprod] |
| 153 | + · suffices g x = 0 by simp [this] |
| 154 | + contrapose! hx |
| 155 | + exact Finset.mem_of_subset (Finset.mem_finsuppAntidiag.mp hg).2 <| by simpa using hx |
| 156 | + |
| 157 | +private theorem aux_prod_coeff_eq_zero_of_notMem_range (f : ℕ → ℕ → M) {d : ℕ} {s : Finset ℕ} |
| 158 | + {g : ℕ →₀ ℕ} (hg : g ∈ s.finsuppAntidiag d) |
| 159 | + (hg' : g ∉ Set.range (aux_toFinsuppAntidiag (n := d))) : |
| 160 | + ∏ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), |
| 161 | + f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1)) : M⟦X⟧) = 0 := by |
| 162 | + suffices ∃ i ∈ s, (coeff (g i)) ((1 : M⟦X⟧) + |
| 163 | + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) = 0 by |
| 164 | + obtain ⟨i, hi, hi'⟩ := this |
| 165 | + apply Finset.prod_eq_zero hi hi' |
| 166 | + contrapose! hg' with hprod |
| 167 | + rw [Set.mem_range] |
| 168 | + refine ⟨Nat.Partition.mk (Finsupp.toMultiset |
| 169 | + (Finsupp.mk (g.support.map (Function.Embedding.mk (· + 1) (add_left_injective 1))) |
| 170 | + (fun i ↦ if i = 0 then 0 else g (i - 1) / i) ?_)) (by simp) ?_, ?_⟩ |
| 171 | + · intro a |
| 172 | + suffices (∃ b, g b ≠ 0 ∧ b + 1 = a) ↔ a ≠ 0 ∧ a ≤ g (a - 1) by simpa |
| 173 | + constructor |
| 174 | + · rintro ⟨b, h1, rfl⟩ |
| 175 | + simpa using Nat.le_of_dvd (Nat.pos_of_ne_zero h1) <| aux_dvd_of_coeff_ne_zero hg hprod b |
| 176 | + · rintro ⟨h1, h2⟩ |
| 177 | + exact ⟨a - 1, by grind⟩ |
| 178 | + · obtain ⟨h1, h2⟩ := Finset.mem_finsuppAntidiag.mp hg |
| 179 | + refine Eq.trans ?_ h1 |
| 180 | + suffices ∑ x ∈ g.support, g x / (x + 1) * (x + 1) = ∑ x ∈ s, g x by simpa [Finsupp.sum] |
| 181 | + rw [Finset.sum_subset h2 (by |
| 182 | + intro x _ |
| 183 | + suffices g x = 0 → g x < x + 1 by simpa; |
| 184 | + grind)] |
| 185 | + exact Finset.sum_congr rfl fun x _ ↦ Nat.div_mul_cancel <| aux_dvd_of_coeff_ne_zero hg hprod x |
| 186 | + · ext x |
| 187 | + simpa [aux_toFinsuppAntidiag] using Nat.div_mul_cancel <| aux_dvd_of_coeff_ne_zero hg hprod x |
| 188 | + |
| 189 | +private theorem aux_prod_f_eq_prod_coeff |
| 190 | + (f : ℕ → ℕ → M) {n : ℕ} (p : Partition n) {s : Finset ℕ} (hs : Finset.range n ≤ s) : |
| 191 | + ∏ i ∈ p.parts.toFinset, f i (Multiset.count i p.parts) = |
| 192 | + ∏ i ∈ s, coeff (p.aux_toFinsuppAntidiag i) |
| 193 | + (1 + ∑' j : ℕ, f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) := by |
| 194 | + refine Finset.prod_of_injOn (· - 1) (aux_injOn_sub_one_parts _) |
| 195 | + ((aux_mapsTo_sub_one_parts p).mono_right hs) ?_ ?_ |
| 196 | + · intro x hx h |
| 197 | + have hx : x + 1 ∉ p.parts := by |
| 198 | + contrapose! h |
| 199 | + exact ⟨x + 1, by simpa using h⟩ |
| 200 | + have hsum := (summable_genFun_term f x).map_tsum _ (WithPiTopology.continuous_constantCoeff M) |
| 201 | + simp [aux_toFinsuppAntidiag, hx, hsum] |
| 202 | + · intro i hi |
| 203 | + have hi : i ∈ p.parts := by simpa using hi |
| 204 | + rw [map_add, (summable_genFun_term f _).map_tsum _ (WithPiTopology.continuous_coeff _ _)] |
| 205 | + suffices f i (Multiset.count i p.parts) = |
| 206 | + ∑' j : ℕ, if Multiset.count i p.parts * i = i * (j + 1) then f i (j + 1) else 0 by |
| 207 | + simpa [Nat.one_le_of_lt (p.parts_pos hi), aux_toFinsuppAntidiag, hi, |
| 208 | + Nat.ne_zero_of_lt (p.parts_pos hi), coeff_X_pow] |
| 209 | + rw [tsum_eq_single (Multiset.count i p.parts - 1) ?_] |
| 210 | + · rw [mul_comm] |
| 211 | + simp [Nat.sub_add_cancel (Multiset.one_le_count_iff_mem.mpr hi)] |
| 212 | + intro b hb |
| 213 | + suffices Multiset.count i p.parts * i ≠ i * (b + 1) by simp [this] |
| 214 | + rw [mul_comm i, (mul_left_inj' (Nat.ne_zero_of_lt (p.parts_pos hi))).ne] |
| 215 | + grind |
| 216 | + |
| 217 | +theorem hasProd_genFun (f : ℕ → ℕ → M) : |
| 218 | + HasProd (fun i ↦ (1 : M⟦X⟧) + ∑' j : ℕ, f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) |
| 219 | + (genFun f) := by |
| 220 | + rw [HasProd, WithPiTopology.tendsto_iff_coeff_tendsto] |
| 221 | + refine fun d ↦ tendsto_atTop_of_eventually_const (fun s (hs : s ≥ Finset.range d) ↦ ?_) |
| 222 | + rw [genFun, coeff_mk, coeff_prod] |
| 223 | + refine (Finset.sum_of_injOn aux_toFinsuppAntidiag |
| 224 | + (aux_toFinsuppAntidiag_injective d).injOn ?_ ?_ ?_).symm |
| 225 | + · refine Set.MapsTo.mono_right (Set.mapsTo_range _ _) ((aux_range_toFinsuppAntidiag d).trans ?_) |
| 226 | + simpa using Finset.finsuppAntidiag_mono hs.le _ |
| 227 | + · exact fun g hg hg' ↦ aux_prod_coeff_eq_zero_of_notMem_range f hg (by simpa using hg') |
| 228 | + · exact fun p _ ↦ aux_prod_f_eq_prod_coeff f p hs.le |
| 229 | + |
| 230 | +end Nat.Partition |
0 commit comments