|
| 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 partitions |
| 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 occurrences 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 Finset PowerSeries |
| 37 | +open scoped PowerSeries.WithPiTopology |
| 38 | + |
| 39 | +namespace Nat.Partition |
| 40 | +variable {R : Type*} [CommSemiring R] |
| 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 | +
|
| 47 | +See the module docstring of `Combinatorics.Enumerative.Partition.GenFun` for more details. -/ |
| 48 | +def genFun (f : ℕ → ℕ → R) : R⟦X⟧ := |
| 49 | + PowerSeries.mk fun n ↦ ∑ p : n.Partition, p.parts.toFinsupp.prod f |
| 50 | + |
| 51 | +@[simp] |
| 52 | +lemma coeff_genFun (f : ℕ → ℕ → R) (n : ℕ) : |
| 53 | + (genFun f).coeff n = ∑ p : n.Partition, p.parts.toFinsupp.prod f := |
| 54 | + PowerSeries.coeff_mk _ _ |
| 55 | + |
| 56 | +variable [TopologicalSpace R] |
| 57 | + |
| 58 | +/-- The infinite sum in the formula `Nat.Partition.hasProd_genFun` always converges. -/ |
| 59 | +theorem summable_genFun_term (f : ℕ → ℕ → R) (i : ℕ) : |
| 60 | + Summable fun j ↦ f (i + 1) (j + 1) • (X : R⟦X⟧) ^ ((i + 1) * (j + 1)) := by |
| 61 | + nontriviality R |
| 62 | + apply WithPiTopology.summable_of_tendsto_order_atTop_nhds_top |
| 63 | + refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩) |
| 64 | + intro m hm |
| 65 | + grw [PowerSeries.smul_eq_C_mul, ← le_order_mul] |
| 66 | + refine lt_add_of_nonneg_of_lt (by simp) ?_ |
| 67 | + rw [order_X_pow] |
| 68 | + norm_cast |
| 69 | + grind |
| 70 | + |
| 71 | +/-- Alternative form of `summable_genFun_term` that unshifts the first index. -/ |
| 72 | +theorem summable_genFun_term' (f : ℕ → ℕ → R) {i : ℕ} (hi : i ≠ 0) : |
| 73 | + Summable fun j ↦ f i (j + 1) • (X : R⟦X⟧) ^ (i * (j + 1)) := by |
| 74 | + obtain ⟨a, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hi |
| 75 | + apply summable_genFun_term |
| 76 | + |
| 77 | +variable [T2Space R] |
| 78 | + |
| 79 | +private theorem aux_dvd_of_coeff_ne_zero {f : ℕ → ℕ → R} {d : ℕ} {s : Finset ℕ} (hs0 : 0 ∉ s) |
| 80 | + {g : ℕ →₀ ℕ} (hg : g ∈ s.finsuppAntidiag d) |
| 81 | + (hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' j, f i (j + 1) • X ^ (i * (j + 1))) ≠ (0 : R)) (x : ℕ) : |
| 82 | + x ∣ g x := by |
| 83 | + by_cases hx : x ∈ s |
| 84 | + · specialize hprod x hx |
| 85 | + contrapose! hprod |
| 86 | + have hx0 : x ≠ 0 := fun h ↦ hs0 (h ▸ hx) |
| 87 | + rw [map_add, (summable_genFun_term' f hx0).map_tsum _ (WithPiTopology.continuous_coeff _ _)] |
| 88 | + rw [show (0 : R) = 0 + ∑' (i : ℕ), 0 by simp] |
| 89 | + congrm (?_ + ∑' (i : ℕ), ?_) |
| 90 | + · suffices g x ≠ 0 by simp [this] |
| 91 | + contrapose! hprod |
| 92 | + simp [hprod] |
| 93 | + · rw [map_smul, coeff_X_pow] |
| 94 | + apply smul_eq_zero_of_right |
| 95 | + suffices g x ≠ x * (i + 1) by simp [this] |
| 96 | + contrapose! hprod |
| 97 | + simp [hprod] |
| 98 | + · suffices g x = 0 by simp [this] |
| 99 | + contrapose! hx |
| 100 | + exact mem_of_subset (mem_finsuppAntidiag.mp hg).2 <| by simpa using hx |
| 101 | + |
| 102 | +private theorem aux_prod_coeff_eq_zero_of_notMem_range (f : ℕ → ℕ → R) {d : ℕ} {s : Finset ℕ} |
| 103 | + (hs0 : 0 ∉ s) {g : ℕ →₀ ℕ} (hg : g ∈ s.finsuppAntidiag d) |
| 104 | + (hg' : g ∉ Set.range (toFinsuppAntidiag (n := d))) : |
| 105 | + ∏ i ∈ s, (coeff (g i)) (1 + ∑' j, f i (j + 1) • X ^ (i * (j + 1)) : R⟦X⟧) = 0 := by |
| 106 | + suffices ∃ i ∈ s, (coeff (g i)) ((1 : R⟦X⟧) + ∑' j, f i (j + 1) • X ^ (i * (j + 1))) = 0 by |
| 107 | + obtain ⟨i, hi, hi'⟩ := this |
| 108 | + apply prod_eq_zero hi hi' |
| 109 | + contrapose! hg' with hprod |
| 110 | + rw [Set.mem_range] |
| 111 | + have hgne0 (i : ℕ) : g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i := by |
| 112 | + refine ⟨fun h ↦ ⟨?_, ?_⟩, by grind⟩ |
| 113 | + · contrapose! hs0 with rfl |
| 114 | + exact mem_of_subset (mem_finsuppAntidiag.mp hg).2 (by simpa using h) |
| 115 | + · exact Nat.le_of_dvd (Nat.pos_of_ne_zero h) <| aux_dvd_of_coeff_ne_zero hs0 hg hprod _ |
| 116 | + refine ⟨Nat.Partition.mk (Finsupp.mk g.support (fun i ↦ g i / i) ?_).toMultiset ?_ ?_, ?_⟩ |
| 117 | + · simpa using hgne0 |
| 118 | + · suffices ∀ i, g i ≠ 0 → i ≠ 0 by simpa [Nat.pos_iff_ne_zero] |
| 119 | + exact fun i h ↦ ((hgne0 i).mp h).1 |
| 120 | + · obtain ⟨h1, h2⟩ := mem_finsuppAntidiag.mp hg |
| 121 | + refine Eq.trans ?_ h1 |
| 122 | + suffices ∑ x ∈ g.support, g x / x * x = ∑ x ∈ s, g x by simpa [Finsupp.sum] |
| 123 | + apply sum_subset_zero_on_sdiff h2 (by simp) |
| 124 | + exact fun x hx ↦ Nat.div_mul_cancel <| aux_dvd_of_coeff_ne_zero hs0 hg hprod x |
| 125 | + · ext x |
| 126 | + simpa [toFinsuppAntidiag] using Nat.div_mul_cancel <| aux_dvd_of_coeff_ne_zero hs0 hg hprod x |
| 127 | + |
| 128 | +private theorem aux_prod_f_eq_prod_coeff (f : ℕ → ℕ → R) {n : ℕ} (p : Partition n) {s : Finset ℕ} |
| 129 | + (hs : Icc 1 n ⊆ s) (hs0 : 0 ∉ s) : |
| 130 | + p.parts.toFinsupp.prod f = |
| 131 | + ∏ i ∈ s, coeff (p.toFinsuppAntidiag i) (1 + ∑' j, f i (j + 1) • X ^ (i * (j + 1))) := by |
| 132 | + simp_rw [Finsupp.prod, Multiset.toFinsupp_support, Multiset.toFinsupp_apply] |
| 133 | + apply prod_subset_one_on_sdiff |
| 134 | + · grind [Multiset.mem_toFinset, mem_Icc] |
| 135 | + · intro x hx |
| 136 | + rw [mem_sdiff, Multiset.mem_toFinset] at hx |
| 137 | + have hx0 : x ≠ 0 := fun h ↦ hs0 (h ▸ hx.1) |
| 138 | + have hsum := (summable_genFun_term' f hx0).map_tsum _ |
| 139 | + (WithPiTopology.continuous_constantCoeff R) |
| 140 | + simp [toFinsuppAntidiag, hsum, hx.2, hx0] |
| 141 | + · intro i hi |
| 142 | + rw [Multiset.mem_toFinset] at hi |
| 143 | + have hi0 : i ≠ 0 := (p.parts_pos hi).ne.symm |
| 144 | + rw [map_add, (summable_genFun_term' f hi0).map_tsum _ (WithPiTopology.continuous_coeff _ _)] |
| 145 | + suffices f i (Multiset.count i p.parts) = |
| 146 | + ∑' j, if Multiset.count i p.parts * i = i * (j + 1) then f i (j + 1) else 0 by |
| 147 | + simpa [toFinsuppAntidiag, hi, hi0, coeff_X_pow] |
| 148 | + rw [tsum_eq_single (Multiset.count i p.parts - 1) ?_] |
| 149 | + · rw [mul_comm] |
| 150 | + simp [Nat.sub_add_cancel (Multiset.one_le_count_iff_mem.mpr hi)] |
| 151 | + intro b hb |
| 152 | + suffices Multiset.count i p.parts * i ≠ i * (b + 1) by simp [this] |
| 153 | + rw [mul_comm i, (mul_left_inj' (Nat.ne_zero_of_lt (p.parts_pos hi))).ne] |
| 154 | + grind |
| 155 | + |
| 156 | +theorem hasProd_genFun (f : ℕ → ℕ → R) : |
| 157 | + HasProd (fun i ↦ 1 + ∑' j, f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) (genFun f) := by |
| 158 | + rw [HasProd, WithPiTopology.tendsto_iff_coeff_tendsto] |
| 159 | + refine fun d ↦ tendsto_atTop_of_eventually_const (fun s (hs : s ≥ range d) ↦ ?_) |
| 160 | + have : ∏ i ∈ s, ((1 : R⟦X⟧) + ∑' j, f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) |
| 161 | + = ∏ i ∈ s.map (addRightEmbedding 1), (1 + ∑' j, f i (j + 1) • X ^ (i * (j + 1))) := by simp |
| 162 | + rw [this] |
| 163 | + have hs : Icc 1 d ⊆ s.map (addRightEmbedding 1) := by |
| 164 | + intro i |
| 165 | + suffices 1 ≤ i → i ≤ d → ∃ a ∈ s, a + 1 = i by simpa |
| 166 | + intro h1 h2 |
| 167 | + refine ⟨i - 1, mem_of_subset hs ?_, ?_⟩ <;> grind |
| 168 | + rw [coeff_genFun, coeff_prod] |
| 169 | + refine (sum_of_injOn toFinsuppAntidiag (toFinsuppAntidiag_injective d).injOn ?_ ?_ ?_).symm |
| 170 | + · intro p _ |
| 171 | + exact mem_of_subset (finsuppAntidiag_mono hs.le _) p.toFinsuppAntidiag_mem_finsuppAntidiag |
| 172 | + · exact fun g hg hg' ↦ aux_prod_coeff_eq_zero_of_notMem_range f (by simp) hg (by simpa using hg') |
| 173 | + · exact fun p _ ↦ aux_prod_f_eq_prod_coeff f p hs.le (by simp) |
| 174 | + |
| 175 | +theorem multipliable_genFun (f : ℕ → ℕ → R) : |
| 176 | + Multipliable fun i ↦ (1 : R⟦X⟧) + ∑' j, f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1)) := |
| 177 | + (hasProd_genFun f).multipliable |
| 178 | + |
| 179 | +theorem genFun_eq_tprod (f : ℕ → ℕ → R) : |
| 180 | + genFun f = ∏' i, (1 + ∑' j, f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) := |
| 181 | + (hasProd_genFun f).tprod_eq.symm |
| 182 | + |
| 183 | +end Nat.Partition |
0 commit comments