Euler's Pentagonal Number Theorem and Jacobi's Triple Product Identity #
This file formalizes Euler's pentagonal number theorem and Jacobi's triple product identity, following the treatment in the AlgebraicCombinatorics textbook.
Main definitions #
pentagonalNumber: The k-th pentagonal number w_k = (3k - 1) * k / 2Level: A "level" is a half-integer p + 1/2 for some integer p (used in the proof)State: A "state" is a set of levels containing all but finitely many negative levels and only finitely many positive levelsState.energy: The energy of a stateState.parnum: The particle number of a state
Main results #
pentagonalNumber_nonneg: Pentagonal numbers are nonnegativeeuler_pentagonal_number_theorem: ∏{k≥1} (1 - x^k) = ∑{k∈ℤ} (-1)^k x^{w_k}jacobi_triple_product: Jacobi's triple product identitypartition_recursive: Recursive formula for partition numbers using pentagonal numberseuler_sum_divisors_recursive: Euler's recursion for the sum of divisors function
References #
- AlgebraicCombinatorics textbook, Section on Partitions/PentagonalJacobi.tex
- [Bell, 2006] for history of Euler's pentagonal number theorem
- [Borcherds' proof via Cameron's book, §8.3]
Tags #
pentagonal number, Euler, Jacobi triple product, partitions, formal power series
Pentagonal Numbers #
The k-th pentagonal number, defined as w_k = (3k - 1) * k / 2. This is always a nonnegative integer for any k ∈ ℤ. (Definition \ref{def.pars.pent-num})
Instances For
Alternative definition using natural number arithmetic for nonnegative k.
The pentagonal number formula: w_k = (3k - 1) * k / 2 is always an integer.
Pentagonal numbers are nonnegative (trivial from the definition as ℕ).
The numerator (3k-1)*k is always even, so division by 2 yields an integer. This is because k and 3k-1 have opposite parities:
- If k is even, then k = 2m, so (3k-1)*k = (6m-1)*2m is even.
- If k is odd, then 3k-1 = 3(2m+1)-1 = 6m+2 is even. (Part of Definition \ref{def.pars.pent-num})
Alternative formula: 2 * w_k = (3k - 1) * k. This is sometimes more convenient than the division form. (Part of Definition \ref{def.pars.pent-num})
Table of pentagonal numbers: k : ... -5 -4 -3 -2 -1 0 1 2 3 4 5 ... w_k: ... 40 26 15 7 2 0 1 5 12 22 35 ...
Pentagonal numbers grow quadratically with |k|.
Key bound: w_k ≥ |k| for k ≠ 0. This is because for k ≥ 1: (3k-1)k/2 ≥ k, and for k ≤ -1: (3|k|+1)|k|/2 ≥ |k|.
The pentagonal numbers for all k ∈ ℤ are distinct. Specifically: w_0 < w_1 < w_{-1} < w_2 < w_{-2} < w_3 < w_{-3} < ...
The ordering of pentagonal numbers.
The pentagonal number formula: 3ℓ² + ℓ = 2w_{-ℓ}. This identity is key to connecting Jacobi's triple product to Euler's pentagonal theorem. When we set q = x³, z = -x in Jacobi's triple product, the RHS exponent is: 3ℓ² + ℓ = (3(-ℓ) - 1)(-ℓ) = 2w_{-ℓ} This allows us to rewrite the sum as ∑_{k∈ℤ} (-1)^k (x²)^{w_k}.
Formal Power Series Setup #
Helper: Check if n is a pentagonal number and return the corresponding k. Returns none if n is not a pentagonal number.
This is computable for any given n by checking a finite range of k values, since pentagonal numbers grow quadratically.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The coefficient of x^n in the pentagonal series. Returns (-1)^k if n = w_k for some k, and 0 otherwise.
Note: We use k.natAbs to compute the sign correctly for negative k,
since (-1)^k = (-1)^|k| for integers (as (-1)^{-m} = (-1)^m).
Equations
- AlgebraicCombinatorics.pentagonalCoeff n = match AlgebraicCombinatorics.pentagonalNumberInverse n with | some k => (-1) ^ k.natAbs | none => 0
Instances For
The pentagonal coefficient at 0 is 1 (since pentagonalNumber 0 = 0 and (-1)^0 = 1).
The alternating sum ∑_{k∈ℤ} (-1)^k x^{w_k} as a formal power series. This is well-defined because the pentagonal numbers grow quadratically.
We define the coefficient at n to be (-1)^k if n = w_k for some k, and 0 otherwise. Since pentagonal numbers are injective, this is well-defined.
Equations
Instances For
The Euler product ∏_{k≥1} (1 - x^k).
This is defined using the discrete topology on R, which ensures the infinite product is well-defined via Mathlib's infrastructure for infinite products of power series. The product is multipliable because the order of (1 - X^k) is k, which tends to infinity.
Equations
- AlgebraicCombinatorics.eulerProduct = ∏' (k : ℕ), (1 - PowerSeries.X ^ (k + 1))
Instances For
Euler's Pentagonal Number Theorem #
Note: The theorem euler_pentagonal_number_theorem is defined later in this file
(after euler_pentagonal_number_theorem_rat) due to dependency ordering.
See the section "Euler's Pentagonal Number Theorem (Main Result)" below.
Recursive Formula for Partition Numbers #
Local alias for Nat.Partition.partitionCount from Partitions/Basics.lean.
This provides compatibility with existing code in this file.
Instances For
The generating function for partitions as a formal power series. ∑_{n∈ℕ} p(n) x^n
Equations
Instances For
The inverse Euler product ∏_{k≥1} 1/(1-x^k).
This is defined using Mathlib's partition generating function framework.
By Nat.Partition.genFun_eq_tprod, this equals:
∏' i, (1 + ∑' j, X ^ ((i + 1) * (j + 1)))
which is the product ∏{k≥1} (1 + X^k + X^{2k} + ...) = ∏{k≥1} 1/(1-X^k).
Equations
- AlgebraicCombinatorics.eulerProductInv = Nat.Partition.genFun fun (x x_1 : ℕ) => 1
Instances For
Theorem \ref{thm.pars.main-gf}: Main generating function for partitions.
∑{n∈ℕ} p(n) x^n = ∏{k≥1} 1/(1-x^k)
This is the fundamental identity connecting the partition function to the infinite product. It is used in the proof of Corollary \ref{cor.pars.pn-rec}.
Note: This may also be available in Mathlib as Nat.Partition.genFun related theorems.
Helper: eulerProduct * eulerProductInv = 1
Coefficient extraction for the product of partition generating function and pentagonal series.
Note: partitionGenFun_mul_pentagonalSeries is defined later in this file after
euler_pentagonal_number_theorem.
The n-th coefficient of 1 is 0 for n > 0
The antidiagonal sum can be split: separate the (n, 0) term
The sum reindexing lemma: relates the antidiagonal sum to the sum over pentagonal indices
Jacobi's Triple Product Identity #
The ring (ℤ[z^±])[[q]] for Jacobi's triple product identity. This is the ring of formal power series in q with coefficients that are Laurent polynomials in z over ℤ.
Instances For
The Laurent polynomial variable z, viewed as a constant power series in JacobiRing. This represents z = T(1) where T is the Laurent polynomial basis element.
Equations
Instances For
The inverse z^{-1} = T(-1) as a constant power series.
Equations
Instances For
z^ℓ for any integer ℓ, as a constant power series.
Equations
Instances For
The factor (1 + q^{2n-1}z) in Jacobi's product, for n ≥ 1. Here we index by n starting from 0, so the exponent is 2n+1.
Equations
Instances For
The factor (1 + q^{2n-1}z^{-1}) in Jacobi's product.
Equations
Instances For
The factor (1 - q^{2n}) in Jacobi's product. Here we index by n starting from 0, so the exponent is 2(n+1).
Equations
- AlgebraicCombinatorics.jacobiFactorQ n = 1 - PowerSeries.X ^ (2 * (n + 1))
Instances For
A single term in Jacobi's product: (1 + q^{2n-1}z)(1 + q^{2n-1}z^{-1})(1 - q^{2n}) indexed starting from n = 0 (corresponding to n = 1 in the mathematical formula).
Equations
Instances For
The left-hand side of Jacobi's triple product identity in JacobiRing: ∏_{n>0} ((1 + q^{2n-1}z)(1 + q^{2n-1}z^{-1})(1 - q^{2n}))
This is defined as an infinite product using the discrete topology on LaurentPolynomial ℤ and the product topology on PowerSeries.
Equations
Instances For
A single term q^{ℓ²} z^ℓ in Jacobi's sum.
Equations
Instances For
The right-hand side of Jacobi's triple product identity in JacobiRing: ∑_{ℓ∈ℤ} q^{ℓ²} z^ℓ
This is defined as an infinite sum over ℤ. The sum is well-defined because the exponent ℓ² grows quadratically, so only finitely many terms contribute to each coefficient of q.
Equations
Instances For
Helper lemmas for Jacobi's triple product identity #
z * z^{-1} = 1 in JacobiRing.
z^(a+b) = z^a * z^b in JacobiRing.
The coefficient of q^n in jacobiSumTerm ℓ is T(ℓ) if n = ℓ², else 0.
State Monomials #
The following definitions and lemmas connect the algebraic terms in Jacobi's identity to the state-based proof infrastructure. A "state monomial" q^e * z^p represents a state with energy e and particle number p.
The monomial q^e * z^p in JacobiRing, representing a state with energy e and particle number p. This is the building block for the state generating function.
Equations
Instances For
jacobiSumTerm ℓ equals the state monomial for energy ℓ² and particle number ℓ. This corresponds to the ground state G_ℓ, since groundState_energy gives energy(G_ℓ) = ℓ² and groundState_parnum gives parnum(G_ℓ) = ℓ.
The state monomial factors as q^{ℓ²} * q^{2n} * z^ℓ. This factorization is useful for relating excited states to the partition structure.
The state monomial for an excited state can be written as jacobiSumTerm ℓ * q^{2n}. This shows that excited state monomials factor into a ground state term (jacobiSumTerm) and a partition contribution (q^{2n} where n = |μ| for partition μ).
Coefficient of q^m in stateMonomial e p is T(p) if m = e, else 0.
The order of stateMonomial e p is exactly e. This is because stateMonomial e p = X^e * z^p, and z^p has order 0 (nonzero constant term).
The order of the state monomial for a pair (ℓ, μ) is ℓ² + 2|μ|. This is used to show that the state generating function is summable.
The tsum over integers ℓ with ℓ² = i equals the finite sum of T(ℓ) over that set.
This is used in the proof of stateGenFun_eq_jacobiRHS'_mul_partitionGenFunJacobi.
The tsum over partitions μ with 2|μ| = j equals the cardinality of that finite set.
This is used in the proof of stateGenFun_eq_jacobiRHS'_mul_partitionGenFunJacobi.
The state generating function in JacobiRing: ∑_{S state} q^{energy(S)} z^{parnum(S)}
In Borcherds' proof, this is the key object that both the LHS and RHS of Jacobi's triple product identity equal (after multiplying by the partition generating function).
Since states are in bijection with pairs (ℓ, μ) where ℓ ∈ ℤ and μ is a partition
(via partitionToState_bijective), and the bijection satisfies:
- energy(E_{ℓ,μ}) = ℓ² + 2|μ| (by
excitedState_energy) - parnum(E_{ℓ,μ}) = ℓ (by
excitedState_parnum)
we can write the state generating function as: ∑{ℓ∈ℤ} ∑{n≥0} ∑_{μ partition of n} q^{ℓ² + 2n} z^ℓ
This equals: ∑{ℓ∈ℤ} q^{ℓ²} z^ℓ · ∑{n≥0} (number of partitions of n) · q^{2n}
which is jacobiRHS' · partitionGenFun[q²].
Equations
Instances For
The partition generating function in JacobiRing with q replaced by q².
This is ∑_{n≥0} p(n) q^{2n} where p(n) is the number of partitions of n. Equivalently, it's the image of the partition generating function under the substitution q ↦ q².
This is a key ingredient in proving Jacobi's triple product identity: stateGenFun = jacobiRHS' * partitionGenFunJacobi
Note: We define this as a sum over partitions rather than using the product formula ∏_{k≥1}(1-q^{2k})^{-1} to match the structure of stateGenFun.
Equations
- AlgebraicCombinatorics.partitionGenFunJacobi = ∑' (p : (n : ℕ) × n.Partition), PowerSeries.X ^ (2 * p.fst)
Instances For
The constant term of partitionGenFunJacobi is 1.
This is because only the partition of 0 (the empty partition) contributes to the constant term, and X^0 = 1.
partitionGenFunJacobi is a unit (has constant term 1, hence invertible).
The product of Z and ZInv factors (without the Q factor): ∏_{n>0} ((1 + q^{2n-1}z)(1 + q^{2n-1}z^{-1})) This is the product that remains after canceling the (1-q^{2n}) factors.
Equations
Instances For
The Euler product (Q factors only): ∏_{n>0} (1 - q^{2n}) This is the product that cancels with partitionGenFunJacobi.
Equations
Instances For
Helper lemmas for the odd case proof #
These lemmas prove that the infinite product of power series with only even-degree terms also has only even-degree terms. This is used to show that the coefficient at odd degree in the product is 0.
Helper lemmas for the even case of partitionGenFunJacobi_mul_QProduct_eq_one #
These lemmas prove that the coefficient at 2*n in the JacobiRing product equals Nat.card (n.Partition).
The key insight is that the JacobiRing product equals the image of the ℤ⟦X⟧ product under
PowerSeries.map (algebraMap ℤ (LaurentPolynomial ℤ)), and the ℤ⟦X⟧ product equals
expand 2 (Nat.Partition.genFun (fun _ _ => 1)).
Key lemma 2: partitionGenFunJacobi * QProduct = 1 (Euler product identity). This is the key cancellation: the partition generating function times the Euler product equals 1, which is the classical identity ∑{μ partition} q^{2|μ|} * ∏{n>0}(1-q^{2n}) = 1 in JacobiRing.
The order of (jacobiFactorZ n * jacobiFactorZInv n - 1) is at least 2n+1. This is the key estimate for proving multipliability of the ZZ product.
The order of (jacobiFactorZ n * jacobiFactorZInv n - 1) tends to infinity as n → ∞. This is the condition needed for multipliability.
The order of (jacobiFactorQ n - 1) tends to infinity as n → ∞. This is the condition needed for multipliability.
The ZZ product is multipliable. The product ∏_n (jacobiFactorZ n * jacobiFactorZInv n) converges in the topology on JacobiRing.
The Q product is multipliable. The product ∏_n jacobiFactorQ n converges in the topology on JacobiRing.
Key lemma 1: jacobiLHS' factors as ZZProduct * QProduct. This follows from the definition of jacobiProductTerm and the fact that infinite products can be split when both factors are multipliable.
Explicit formulas for Jacobi factors #
These lemmas give explicit formulas for jacobiFactorZ n - 1 and jacobiFactorZInv n - 1, which are used in the binary expansion proof.
Explicit formula: jacobiFactorZ n - 1 = X^{2n+1} * jacobiZ.
Explicit formula: jacobiFactorZInv n - 1 = X^{2n+1} * jacobiZInv.
Product formula for Z factors over a finite set. ∏{n∈P} (jacobiFactorZ n - 1) = X^{∑{n∈P}(2n+1)} * jacobiZ^{|P|}
Product formula for ZInv factors over a finite set. ∏{n∈N} (jacobiFactorZInv n - 1) = X^{∑{n∈N}(2n+1)} * jacobiZInv^{|N|}
jacobiZ^m * jacobiZInv^n = jacobiZPow (m - n). This combines powers of z and z⁻¹.
The order of (jacobiFactorZ n - 1) is at least 2n+1.
The order of (jacobiFactorZInv n - 1) is at least 2n+1.
The product ∏' n, jacobiFactorZ n is multipliable. This is the product of (1 + q^{2n+1}z) over all n ≥ 0.
The product ∏' n, jacobiFactorZInv n is multipliable. This is the product of (1 + q^{2n+1}z^{-1}) over all n ≥ 0.
The ZZ product splits as the product of Z factors times ZInv factors. This is because both individual products are multipliable.
(P, N) to State Bijection Infrastructure #
The bijection between pairs (P, N) of finite subsets of ℕ and states is key to
proving jacobiZZProduct_eq_stateGenFun. Here we define the level set map and prove its properties.
Given (P, N):
- P represents the set of nonnegative integers in the state (positive half-integer levels)
- N represents the set of n such that -n-1 is NOT in the state (missing negative levels)
Note: The actual State definition is later in the file. The finsetPairToState function
is defined after State.
The set of levels corresponding to a pair (P, N) of finite subsets of ℕ.
The state S has:
- All negative levels except {-n-1 : n ∈ N}
- Exactly the levels in P among nonnegative levels
Equations
Instances For
Binary Expansion Infrastructure #
The following lemmas establish the binary expansion formula for infinite products: ∏' n, (1 + a_n) = ∑' P : Finset ℕ, ∏ n ∈ P, a_n
This is the key ingredient for proving jacobiZZProduct_eq_stateGenFun.
The order of a product over a finite set P of (jacobiFactorZ n - 1) terms. For each n, jacobiFactorZ n - 1 = X^{2n+1} * z, so the product over P has order at least ∑{n ∈ P} (2n+1) = 2 * (∑{n ∈ P} n) + |P|.
This grows quadratically with |P|, ensuring summability of the binary expansion.
The order of a product over a finite set P of (jacobiFactorZInv n - 1) terms. Similar to the Z case.
The sum of odd numbers 1 + 3 + 5 + ... + (2k-1) equals k². This is the key formula for the quadratic lower bound.
General lemma: order of a product over a finite set is at least the sum of orders. This is a key tool for proving order bounds on products.
If each a n has order at least 2n+1, then the product over P has order
at least ∑ n ∈ P, (2n+1). This is the key estimate for summability.
Binary expansion formula for infinite products. For a sequence a : ℕ → R of elements with increasing order, we have: ∏' n, (1 + a n) = ∑' P : Finset ℕ, ∏ n ∈ P, a n
This is the key formula for expanding the ZZ product.
The proof uses Mathlib's tprod_one_add theorem. The main work is establishing
summability of the RHS, which follows from order bounds:
- For each P, (∏ n ∈ P, a n).order ≥ ∑ n ∈ P, (2n+1) by
order_finset_prod_ge_sum_odd - For each degree d, only finitely many P have ∑ n ∈ P, (2n+1) ≤ d by
finite_finsets_sum_le - Therefore, only finitely many P contribute at each degree, ensuring summability
Key helper lemmas:
order_finset_prod_ge_sum_odd: order bound for products over finite setsfinite_finsets_sum_le: only finitely many P contribute at each degree
Binary expansion of the Z product: ∏' n, jacobiFactorZ n = ∑' P, ∏_{n∈P} (jacobiFactorZ n - 1). This applies the general binary expansion formula to the specific Z factors.
Binary expansion of the ZInv product: ∏' n, jacobiFactorZInv n = ∑' N, ∏_{n∈N} (jacobiFactorZInv n - 1). This applies the general binary expansion formula to the specific ZInv factors.
The sum ∑' P, ∏_{n∈P} (jacobiFactorZ n - 1) is summable. This is needed to apply Summable.tsum_mul_tsum.
The sum ∑' N, ∏_{n∈N} (jacobiFactorZInv n - 1) is summable. This is needed to apply Summable.tsum_mul_tsum.
The ZZ product equals a double sum over pairs (P, N) of finite subsets. This combines the binary expansions of the Z and ZInv products.
The formula is: jacobiZZProduct = ∑' (P, N), (∏{n∈P} (jacobiFactorZ n - 1)) * (∏{n∈N} (jacobiFactorZInv n - 1)) = ∑' (P, N), X^{∑(2n+1) + ∑(2m+1)} * z^{|P|} * z^{-|N|} = ∑' (P, N), X^{∑(2n+1) + ∑(2m+1)} * z^{|P| - |N|}
This is the key expansion needed to relate jacobiZZProduct to stateGenFun.
Proof sketch: Use tprod_jacobiFactorZ_eq_tsum, tprod_jacobiFactorZInv_eq_tsum,
and Summable.tsum_mul_tsum to expand the product of two sums into a double sum.
The explicit form of each term in the double sum. For a pair (P, N) of finite subsets of ℕ: (∏{n∈P} (jacobiFactorZ n - 1)) * (∏{n∈N} (jacobiFactorZInv n - 1)) = X^{∑{n∈P}(2n+1) + ∑{n∈N}(2n+1)} * z^{|P| - |N|}
This uses the explicit formulas for the products.
For a pair (P, N) of finite subsets of ℕ, the X-exponent in the double sum expansion can be written as 2·(∑P + ∑N) + |P| + |N|.
This is the first step in showing that the double sum equals the state generating function. The key equation is: ∑{n∈P}(2n+1) + ∑{m∈N}(2m+1) = ℓ² + 2|μ| where ℓ = |P| - |N| and μ is a partition encoding the excitations.
The order of (jacobiFactorQ n - 1) is at least 2(n+1).
The order of (jacobiProductTerm n - 1) is at least 2n+1. This is the key estimate for proving multipliability.
The order of (jacobiProductTerm n - 1) tends to infinity as n → ∞. This is the condition needed for multipliability.
The Jacobi product is multipliable. The product ∏_n jacobiProductTerm n converges in the topology on JacobiRing.
The order of jacobiSumTerm ℓ is ℓ², which grows quadratically. This is used to prove summability.
The order of jacobiSumTerm ℓ tends to infinity as |ℓ| → ∞. This is the condition needed for summability.
A family of PowerSeries indexed by ℤ is summable if their order tends to infinity
on the cofinite filter. This is the ℤ-indexed version of
PowerSeries.WithPiTopology.summable_of_tendsto_order_atTop_nhds_top.
The Jacobi sum is summable. The sum ∑_{ℓ∈ℤ} jacobiSumTerm ℓ converges in the topology on JacobiRing.
The coefficients of jacobiSumTerm are summable for each fixed n. Only finitely many ℓ contribute (those with ℓ² = n).
The left-hand side of Jacobi's triple product identity evaluated at q = u·x^a, z = v·x^b: ∏_{n>0} ((1 + q^{2n-1}z)(1 + q^{2n-1}z^{-1})(1 - q^{2n}))
Expanding with q = u·x^a and z = v·x^b: ∏_{n>0} ((1 + u^{2n-1}v·x^{(2n-1)a+b})(1 + u^{2n-1}v^{-1}·x^{(2n-1)a-b})(1 - u^{2n}·x^{2na}))
When a > 0 and a ≥ |b|, all exponents (2n-1)a+b, (2n-1)a-b, and 2na are nonnegative for n > 0, so this is a well-defined element of ℚ⟦X⟧. The infinite product is multipliable because the exponents grow linearly in n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The right-hand side of Jacobi's triple product identity evaluated at q = u·x^a, z = v·x^b: ∑{ℓ∈ℤ} q^{ℓ²} z^ℓ = ∑{ℓ∈ℤ} u^{ℓ²} v^ℓ x^{aℓ² + bℓ}
When a > 0 and a ≥ |b|, the exponent aℓ² + bℓ ≥ 0 for all ℓ ∈ ℤ, since: aℓ² + bℓ ≥ |b|·ℓ² - |b|·|ℓ| = |b|·|ℓ|·(|ℓ| - 1) ≥ 0
This is a well-defined element of ℚ⟦X⟧. The infinite sum is summable because the exponent aℓ² + bℓ grows quadratically in |ℓ|.
Equations
Instances For
The partition generating function evaluated at q = u·x^a: ∏{k>0} (1 - q^{2k})^{-1} = ∏{k>0} (1 - u^{2k}·x^{2ka})^{-1}
When a > 0, all exponents 2ka are positive for k > 0, so this is well-defined as a formal power series. The constant term is 1, so it is a unit in ℚ⟦X⟧.
This represents the generating function for partitions where each part contributes q^{2·part} to the weight.
Equations
Instances For
The partition generating function has constant term 1. This is because the only partition with |μ| = 0 is the empty partition.
The partition generating function is a unit (invertible) in ℚ⟦X⟧.
The Euler product with parameters: ∏_{k>0}(1 - u^{2k}·X^{2ak}).
This is the product that cancels with partitionGenFunEval.
Equations
Instances For
The Euler product has constant term 1. This is because each factor (1 - c·X^n) has constant term 1 for n > 0.
The Euler product is a unit (invertible) in ℚ⟦X⟧.
Helper lemmas for exponent calculations #
These lemmas establish key properties of the scaled exponents (2 * a * (k + 1)).toNat
used in the partition generating function identity.
Partition sum and product formulas #
These lemmas relate the multiset sum of a partition to the Finsupp representation, which is key for proving the partition generating function identity.
Key identity: partitionGenFunEval * eulerProductParam = 1.
This shows that partitionGenFunEval is the inverse of the Euler product.
The proof uses the geometric series identity: for each k,
(∑' j, x_k^j) * (1 - x_k) = 1
where x_k = u^{2(k+1)} * X^{2a(k+1)}.
Combined with the product decomposition of partitions, this gives the result.
Helper lemmas for parameterized product expansion #
These lemmas compute the explicit form of the finite products of parameterized factors.
They are used in the proof of jacobiLHS_mul_partitionGenFun to connect the binary
expansion of the product to the sum over (ℓ, μ) pairs.
The product of aZ factors over a finite set P equals a single term with coefficient u^(∑(2n+1)) * v^|P| and exponent ∑((2n+1)*a + b).
The product of aZInv factors over a finite set N equals a single term with coefficient u^(∑(2n+1)) * v^{-|N|} and exponent ∑((2n+1)*a - b).
The explicit form of the double sum term for a pair (P, N). This shows that the product of aZ and aZInv factors gives a term with:
- Coefficient: u^(∑(2n+1) + ∑(2m+1)) * v^(|P| - |N|)
- Exponent: ∑((2n+1)*a + b) + ∑((2m+1)*a - b)
The coefficient of X^d in the double sum term for a pair (P, N).
Using double_sum_term_param_explicit, we get:
- If d = exponent, then coefficient = u^energy * v^parnum
- Otherwise, coefficient = 0
Helper lemma: The factorZ k - 1 form equals the standard aZ form used in
coeff_double_sum_term_param. This bridges the gap between the definitions.
Helper lemma: The factorZInv k - 1 form equals the standard aZInv form.
Key lemma: The coefficient of X^d in the product of (factorZ - 1) terms equals
the coefficient formula from coeff_double_sum_term_param.
This bridges the gap between the factorZ k - 1 definition used in the main proof
and the standard aZ form used in coeff_double_sum_term_param.
Proof Infrastructure: States and Levels #
A "level" is a half-integer, represented as p + 1/2 for some integer p. We represent it simply by the integer p.
Equations
Instances For
A "state" is a set of levels that contains all but finitely many negative levels and only finitely many positive levels.
This is used in Borcherds' proof of Jacobi's triple product identity.
Important convention: A "level" in the tex source is a half-integer p + 1/2 for some integer p.
We represent it by the integer p. Thus:
- "positive level" in the tex source means
p + 1/2 > 0, i.e.,p ≥ 0in our representation - "negative level" in the tex source means
p + 1/2 < 0, i.e.,p < 0in our representation
The structure tracks:
finite_nonneg: the set of nonnegative integers p (representing positive half-integer levels) in Sfinite_negative_missing: the set of negative integers p (representing negative half-integer levels) NOT in S
The set of levels in this state
Only finitely many nonnegative levels (p ≥ 0, representing positive half-integers p+1/2 > 0) are in the state
Only finitely many negative levels (p < 0, representing negative half-integers p+1/2 < 0) are NOT in the state
Instances For
The energy of a state S is: energy(S) = ∑{p≥0, p∈S} (2p+1) - ∑{p<0, p∉S} (2p+1)
In the tex source, levels are half-integers q = p + 1/2, and the formula is:
energy(S) = ∑{q>0, q∈S} 2q - ∑{q<0, q∉S} 2q
Substituting q = p + 1/2:
- q > 0 ⟺ p ≥ 0
- 2q = 2(p + 1/2) = 2p + 1
For p ≥ 0: 2p + 1 = 2p.natAbs + 1 (since p.natAbs = p for p ≥ 0) For p < 0: -(2p + 1) = -2p - 1 = 2|p| - 1 = 2*p.natAbs - 1 (since p.natAbs = -p for p < 0)
Thus energy is always a natural number.
Equations
Instances For
The particle number of a state S is: parnum(S) = #{p ≥ 0 : p ∈ S} - #{p < 0 : p ∉ S}
In the tex source, this counts the number of positive half-integer levels in S minus the number of negative half-integer levels not in S.
Instances For
The ℓ-ground state G_ℓ = {all levels < ℓ}.
In the half-integer convention, G_ℓ contains all half-integer levels q < ℓ. In our integer representation (where level q = p + 1/2), this is {p : p < ℓ}.
For ℓ ≥ 0:
- Nonnegative integers in G_ℓ: {0, 1, ..., ℓ-1}
- No negative integers are missing from G_ℓ
For ℓ < 0:
- No nonnegative integers are in G_ℓ
- Negative integers missing from G_ℓ: {ℓ, ℓ+1, ..., -1}
Equations
- AlgebraicCombinatorics.State.groundState ell = { levels := {p : AlgebraicCombinatorics.Level | p < ell}, finite_nonneg := ⋯, finite_negative_missing := ⋯ }
Instances For
The energy of the ground state G_ℓ is ℓ².
For ℓ ≥ 0:
- G_ℓ = {p : p < ℓ}
- Nonnegative integers in G_ℓ: {0, 1, ..., ℓ-1}
- Energy from nonneg: (20+1) + (21+1) + ... + (2*(ℓ-1)+1) = 1 + 3 + 5 + ... + (2ℓ-1) = ℓ²
- No negative integers are missing, so energy from neg_missing = 0
- Total energy = ℓ²
For ℓ < 0:
- G_ℓ = {p : p < ℓ}
- No nonnegative integers in G_ℓ, so energy from nonneg = 0
- Negative integers missing from G_ℓ: {ℓ, ℓ+1, ..., -1}
- Energy from neg_missing: (2*|ℓ|-1) + (2*|ℓ+1|-1) + ... + (2*|-1|-1) = (2*|ℓ|-1) + (2*(|ℓ|-1)-1) + ... + (2*1-1) = (2|ℓ|-1) + (2|ℓ|-3) + ... + 1 = |ℓ|² = ℓ²
The proof is technical and involves showing that:
- The sum 1 + 3 + 5 + ... + (2n-1) = n² (sum of first n odd numbers)
- The correct correspondence between the finite sets and the sums
The particle number of the ground state G_ℓ is ℓ.
A jump by q steps raises the energy by 2q.
The proof tracks how the finite sums change when we jump from p to p+q:
- If p ≥ 0: p is removed from the nonneg set, contributing -(2*|p| + 1)
- If p+q ≥ 0: p+q is added to the nonneg set, contributing +(2*|p+q| + 1)
- If p < 0: p is added to the negative_missing set, contributing +(2*|p| - 1)
- If p+q < 0: p+q is removed from the negative_missing set, contributing -(2*|p+q| - 1)
The total change is always 2*q, as proven by energy_change_formula.
A state S is reachable from T by a sequence of jumps.
- refl {T : State} : T.ReachableByJumps T
- step {T : State} (S S' : State) (p : Level) (q : ℕ) (hp : p ∈ S.levels) (hpq : p + ↑q ∉ S.levels) (hq : q > 0) : T.ReachableByJumps S → S' = S.jump p q hp hpq hq → T.ReachableByJumps S'
Instances For
Any state reachable from the ground state by jumps has particle number ℓ.
A state S is reachable from T by a sequence of jumps with total jump amount m.
This is an extended version of ReachableByJumps that tracks the cumulative sum
of all jump sizes, which is needed to prove energy formulas.
- refl {T : State} : T.ReachableByJumpsWithTotal T 0
- step {T : State} (S S' : State) (p : Level) (q m : ℕ) (hp : p ∈ S.levels) (hpq : p + ↑q ∉ S.levels) (hq : q > 0) : T.ReachableByJumpsWithTotal S m → S' = S.jump p q hp hpq hq → T.ReachableByJumpsWithTotal S' (m + q)
Instances For
The energy increases by 2*m when a state is reachable with total jump amount m.
This follows from jump_energy by induction on the reachability.
The explicit set of levels in an excited state E_{ℓ,μ}. E_{ℓ,μ} = {p | p < ℓ-k} ∪ {ℓ-1-i+μ_i | i ∈ {0,...,k-1}} where k is the number of parts and μ_i are the parts (sorted in decreasing order).
We use mu.parts.sort (· ≥ ·) to get a canonical decreasing ordering of parts.
This ensures that the excited levels uniquely encode the partition, since with sorted
parts the function i ↦ parts[i] - i is strictly decreasing (hence injective).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The excited state E_{ℓ,μ} obtained from the ground state by jumping electrons according to the partition μ.
Given a partition μ = (μ₁, μ₂, ..., μₖ) of some n, we start with the ℓ-ground state and let the k highest electrons jump by μ₁, μ₂, ..., μₖ steps respectively.
Equations
- AlgebraicCombinatorics.State.excitedState ell mu = { levels := AlgebraicCombinatorics.State.excitedStateLevels ell mu, finite_nonneg := ⋯, finite_negative_missing := ⋯ }
Instances For
The target level (ell - 1 - i + parts[i]) is NOT in the intermediate state after i jumps, provided parts[i] ≥ 1 and parts are sorted in decreasing order.
The intermediate state levels after i+1 jumps equals the result of jumping from i.
The final intermediate state (after k jumps) equals the excited state.
The intermediate state (i+1) equals the jump from intermediate state i. This is the key lemma connecting the intermediate state construction to the jump operation.
The excited state is reachable from the ground state by a sequence of jumps. This follows from the construction: we apply k jumps, one for each part of μ.
The proof proceeds by induction on the number of parts k = (mu.parts.sort (· ≥ ·)).length:
- Base case (k = 0): The excited state has levels {p | p < ell} = groundState.levels, so ReachableByJumps.refl applies.
- Inductive case (k > 0): We construct k jumps where the i-th jump (0-indexed) is
from level (ell - 1 - i) by parts[i] steps. Each jump is valid because:
- (ell - 1 - i) is in the intermediate state (it's < ell - i)
- (ell - 1 - i + parts[i]) is NOT in the intermediate state (requires parts[i] > 0 and no collision with previous jump targets)
- parts[i] > 0 (all parts of a partition are positive)
The excited state is reachable from the ground state with total jump amount n. This is the key lemma for computing the energy: we apply k jumps, one for each part of μ, and the total jump amount is the sum of the parts, which equals n.
The energy of an excited state.
The proof uses reachableByJumpsWithTotal_energy with the fact that the excited
state is reachable with total jump amount n, combined with groundState_energy.
The particle number of an excited state equals ℓ.
The bijection Φ_ℓ : {partitions} → {states with particle number ℓ}. Here we use Σ n, Nat.Partition n to represent all partitions.
Equations
Instances For
The function i ↦ parts[i] - i is injective for sorted parts. This is key to proving that excited levels uniquely determine the partition.
Jump targets are distinct for different indices. This is key for showing the target of jump i doesn't collide with previous targets.
Equal excited state levels implies equal number of parts.
excitedState is injective: different partitions give different states. This follows from the fact that the levels in E_{ℓ,μ} uniquely encode μ. The excited state records exactly which electrons jumped and by how much, so the partition can be recovered from the state.
The proof uses the fact that with sorted parts, the function i ↦ parts[i] - i is strictly decreasing, hence injective. This means the set of excited levels {ell - 1 - i + parts[i] | i < k} uniquely determines the sequence of parts.
The base level of a state is the smallest level not in S. This is well-defined because:
- The set of levels not in S is nonempty (S can't contain all integers)
- The set is bounded below (only finitely many negative levels are missing)
Instances For
The base level is not in the state's levels.
The excited levels form a finite set.
The excited levels as a finset.
Equations
Instances For
All excited levels are strictly greater than baseLevel.
The particle number equals baseLevel plus the number of excited levels.
Every state with particle number ℓ can be written as an excited state. This is the "unjumping" operation: given S with parnum = ℓ, we find the unique partition μ such that E_{ℓ,μ} = S by comparing S to the ground state G_ℓ and extracting the jump sizes.
The construction proceeds as follows:
- Let t = baseLevel S (the smallest level not in S)
- Let k = ell - t (the number of parts, shown to be nonnegative)
- The excited levels E = excitedLevelsFinset S has exactly k elements
- Sort E decreasingly as [e_0, ..., e_{k-1}]
- Define parts[i] = e_i - (ell - 1 - i) (shown to be positive)
- The partition μ has parts given by this list
- Verify that excitedState ell μ = S
The key insight is that the parnum calculation shows |E| = ell - t:
- For t ≥ 0: parnum = t + |E|, so |E| = ell - t
- For t < 0: parnum = |E| + t, so |E| = ell - t
Every state with particle number ℓ can be written as E_{ℓ,μ} for a unique partition μ.
This establishes a bijection Φ_ℓ : {partitions} → {states with particle number ℓ}. The map sends a partition μ to the excited state E_{ℓ,μ}.
Note: We express this as bijectivity onto the subtype {S : State // S.parnum = ell} rather than as a map to State × ℤ (which would not be surjective since the particle number of excitedState is always ell).
Global bijection between (ℓ, μ) pairs and States.
This combines partitionToState_bijective across all values of ℓ to give a bijection
between ℤ × (Σ n, Nat.Partition n) and State.
The map sends (ℓ, μ) to the excited state E_{ℓ,μ}. The inverse sends S to (parnum(S), μ) where μ is the unique partition with E_{parnum(S),μ} = S.
This is key for reindexing sums: ∑{(ℓ,μ)} f(ℓ,μ) = ∑{S} f(parnum(S), μ(S)).
For any state S, there exists n ≥ 0 such that energy(S) = |parnum(S)|² + 2n.
This is the key relationship between energy and parnum that follows from the bijection with excited states. The value n is the size of the unique partition μ such that excitedState (parnum S) μ = S.
The "partition size" of a state: the n such that energy(S) = |parnum(S)|² + 2n.
This is well-defined by energy_eq_parnum_sq_add_even and equals the size of the unique partition μ with excitedState (parnum S) μ = S.
Instances For
The state monomial for an excited state E_{ℓ,μ} (where μ is a partition of n) equals q^{ℓ² + 2n} z^ℓ.
This follows from excitedState_energy (energy = ℓ² + 2n) and excitedState_parnum (parnum = ℓ). Combined with stateMonomial_eq_sumTerm_mul, this shows that excited state monomials factor as (ground state term) × (partition contribution).
Bijection between (P, N) pairs and States #
We establish a bijection between pairs (P, N) of finite subsets of ℕ and States.
- P represents the nonnegative levels in the state (n ∈ P means n ∈ S.levels)
- N represents the negative levels that are MISSING from the state (n ∈ N means -(n+1) ∉ S.levels, i.e., the negative level at position n is missing)
This bijection is key to proving coeff_double_sum_eq_coeff_stateGenFun.
Key insight: For a state S:
- The nonnegative levels in S form a finite set P ⊆ ℕ
- The negative levels missing from S can be indexed by a finite set N ⊆ ℕ where n ∈ N means the level -(n+1) is missing
Under this bijection:
- energy(S) = ∑{n∈P}(2n+1) + ∑{n∈N}(2n+1)
- parnum(S) = |P| - |N|
These formulas match the exponent and z-power in the double sum expansion of jacobiZZProduct.
Construct a state from a pair (P, N) of finite subsets of ℕ.
- P represents the nonnegative levels in the state (n ∈ P means n ∈ S.levels)
- N represents the negative levels that are MISSING from the state (n ∈ N means -(n+1) ∉ S.levels)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extract the P component (nonnegative levels) from a state. For a state S, this returns {n ∈ ℕ : n ∈ S.levels}.
Equations
- S.toP = Finset.image (fun (p : AlgebraicCombinatorics.Level) => Int.toNat p) ⋯.toFinset
Instances For
Extract the N component (missing negative levels) from a state. For a state S, this returns {n ∈ ℕ : -(n+1) ∉ S.levels}.
Equations
- S.toN = Finset.image (fun (p : AlgebraicCombinatorics.Level) => Int.toNat (-p - 1)) ⋯.toFinset
Instances For
The particle number of a state constructed from (P, N) equals |P| - |N|.
This matches the z-power in the double sum: z^{|P| - |N|} = z^{parnum(S)}.
Key identity: For S = fromFinsetPair P N, the "odd sum" representation equals the "squared parnum + partition" representation.
This shows: ∑{p∈P}(2p+1) + ∑{n∈N}(2n+1) = ||P| - |N||² + 2 * partitionSize(S)
This identity is the heart of the bijection between (P, N) pairs and (ℓ, μ) pairs. It follows from fromFinsetPair_energy, fromFinsetPair_parnum, and partitionSize_spec.
Round-trip property: fromFinsetPair (toP S) (toN S) = S.
This shows that every state can be reconstructed from its (P, N) components.
Round-trip property: toP (fromFinsetPair P N) = P.
Round-trip property: toN (fromFinsetPair P N) = N.
The map (P, N) ↦ fromFinsetPair P N is a bijection from Finset ℕ × Finset ℕ to State.
This establishes the bijection needed for coeff_double_sum_eq_coeff_stateGenFun.
For any (P, N) pair, the energy of fromFinsetPair P N equals ℓ.natAbs² + 2n for some partition of n, where ℓ = |P| - |N|.
This is the key connection between the (P, N) indexing and the (ℓ, μ) indexing in the state generating function. The proof uses:
- fromFinsetPair_parnum: parnum(fromFinsetPair P N) = |P| - |N|
- excitedState_surjective: every state with parnum = ℓ is excitedState ℓ μ for some μ
- excitedState_energy: energy(excitedState ℓ μ) = ℓ.natAbs² + 2|μ|
The energy formula for (P, N) pairs matches the excited state formula.
Combining fromFinsetPair_energy and fromFinsetPair_energy_form, we get: ∑ n ∈ P, (2n+1) + ∑ n ∈ N, (2n+1) = (|P| - |N|).natAbs² + 2|μ|
where μ is the unique partition such that excitedState (|P| - |N|) μ = fromFinsetPair P N.
The set of states with a given energy is finite.
This is because for energy = d, we need:
- ℓ.natAbs² + 2|μ| = d, which bounds |ℓ| ≤ √d and |μ| ≤ d/2
- There are finitely many such (ℓ, μ) pairs, and the bijection with states preserves this.
Key reindexing lemma: summing over (P, N) pairs with given energy equals summing over (ℓ, μ) pairs with the same energy, via the State bijection.
Both sums can be expressed as sums over states:
- LHS: ∑{(P,N): exp(P,N)=d} f(|P|-|N|) = ∑{S: energy(S)=d} f(S.parnum)
- RHS: ∑{(ℓ,μ): ℓ²+2|μ|=d} f(ℓ) = ∑{S: energy(S)=d} f(S.parnum)
This is the key combinatorial fact needed for coeff_double_sum_eq_coeff_stateGenFun.
The key bijection lemma: both finite sums equal the sum over states.
This proves that: ∑{(P,N): exp(P,N)=d} f(|P|-|N|) = ∑{(ℓ,μ): ℓ²+2|μ|=d} f(ℓ)
Both equal ∑_{S: energy(S)=d} f(S.parnum) via the State bijections.
The proof uses:
- finsetPair_bijective: (P, N) ↔ State is a bijection
- partitionToState_bijective: (ℓ, μ) ↔ {S : State // S.parnum = ℓ} is a bijection
- fromFinsetPair_energy, fromFinsetPair_parnum: connect (P,N) to State
- excitedState_energy, excitedState_parnum: connect (ℓ,μ) to State
- sum_finsetPair_eq_sum_partition_via_state: reindexing lemma
This lemma provides the key combinatorial fact needed to fill the sorry in
coeff_double_sum_eq_coeff_stateGenFun.
Generalized bijection lemma for any additive commutative monoid R.
This proves that: ∑{(P,N): exp(P,N)=d} f(|P|-|N|) = ∑{(ℓ,μ): ℓ²+2|μ|=d} f(ℓ)
for any function f : ℤ → R where R is an additive commutative monoid.
This is used in the parameterized Jacobi triple product proof where R = ℚ.
The exponent for (P, N) equals the exponent for the corresponding (ℓ, μ).
This lemma shows that the bijection (P, N) ↔ (ℓ, μ) preserves the exponent: exponent(P, N) = (a * energy + b * parnum).toNat = (a * (ℓ² + 2|μ|) + b * ℓ).toNat
where ℓ = |P| - |N| (parnum) and energy = ℓ² + 2|μ| (by fromFinsetPair_energy_parnum_relation).
This is the key lemma for jacobiLHS_mul_partitionGenFun: it shows that pairs (P, N) and (ℓ, μ)
with the same exponent are in bijection via the State infrastructure.
Parameterized bijection lemma for coefficient equality in Jacobi triple product.
This lemma establishes that the coefficient sums over (P, N) pairs and (ℓ, μ) pairs are equal when using the parameterized exponent formula.
The key insight is that the bijection (P, N) ↔ (ℓ, μ) via the State infrastructure
preserves both the exponent (by exponent_preserved_by_bijection) and the coefficient
values (since energy = ℓ² + 2|μ| and parnum = ℓ under the bijection).
This is the main technical lemma needed to complete jacobiLHS_mul_partitionGenFun.
Helper lemma for jacobiLHS_mul_partitionGenFun: the coefficient sum over (P, N) pairs
equals the coefficient sum over (ℓ, μ) pairs with the (pair.1^2).natAbs exponent form.
This bridges the gap between finsetPair_sum_eq_partition_sum_param (which uses pair.1.natAbs^2)
and the form needed in jacobiLHS_mul_partitionGenFun (which uses (pair.1^2).natAbs).
The key identity is (ℓ^2).natAbs = ℓ.natAbs^2 from Int.natAbs_pow.
The product jacobiLHSEval * partitionGenFunEval equals the state generating function.
This is the key step in the LHS computation: jacobiLHSEval · partitionGenFunEval = ∏{n>0}((1+q^{2n-1}z)(1+q^{2n-1}z^{-1})(1-q^{2n})) · ∏{k>0}(1-q^{2k})^{-1} = ∏_{n>0}((1+q^{2n-1}z)(1+q^{2n-1}z^{-1}))
Using binary expansion, this product equals: ∑{P finite, N finite} q^{∑{p∈P}(2p-1) + ∑{n∈N}(2n-1)} z^{|P| - |N|} = ∑{S state} q^{energy(S)} z^{parnum(S)}
The proof uses the binary expansion of the product over positive integers.
Jacobi's Triple Product Identity (Theorem \ref{thm.pars.jtp2})
The evaluated form of Jacobi's triple product identity: jacobiLHSEval a b u v = jacobiRHSEval a b u v
where the LHS is an infinite product and the RHS is an infinite sum.
This is the parameterized version with parameters a, b (integers with a > 0 and |b| ≤ a)
and u, v (rational numbers with v ≠ 0).
The proof follows Borcherds' approach via "states" (as presented in Cameron's book, §8.3). Both sides, when multiplied by the partition generating function, equal the same "state generating function", allowing cancellation.
See also jacobi_triple_product_fps' for the formal power series version (thm.pars.jtp1).
Alternative Proof Approach: Evaluation Homomorphism #
This section provides infrastructure for an alternative proof of jacobi_triple_product
that bypasses the file ordering issue in jacobiLHS_mul_partitionGenFun.
The idea is to derive jacobi_triple_product from jacobi_triple_product_fps'
(which is fully proved later in this file) by constructing an evaluation map from
JacobiRing to ℚ⟦X⟧ that sends q^e * z^ℓ to u^e * v^ℓ * X^{ae + bℓ}.
If we can show:
evalJacobi jacobiLHS' = jacobiLHSEval a b u vevalJacobi jacobiRHS' = jacobiRHSEval a b u v
Then jacobi_triple_product follows immediately from jacobi_triple_product_fps'.
Note: The original analysis was tracked in issue 9a9b6a12 (now resolved and split into issues 62191a41 and 9dd5829e for focused tracking of the remaining blockers).
Evaluation of a Laurent polynomial coefficient at z = v·X^b. For c ∈ LaurentPolynomial ℤ, evaluate at z = v·X^b to get an element of ℚ⟦X⟧. This sends T^ℓ → v^ℓ·X^{bℓ} when bℓ ≥ 0 for all ℓ in the support of c.
Equations
- AlgebraicCombinatorics.evalLaurentCoeff b v c = ∑ ℓ ∈ c.support, (↑(c ℓ) * v ^ ℓ) • PowerSeries.X ^ (b * ℓ).toNat
Instances For
evalLaurentCoeff sends T^1 to v·X^b.
evalLaurentCoeff sends T^(-1) to v^(-1)·X^{(-b).toNat}.
evalLaurentCoeff sends 1 to 1.
evalLaurentCoeff is additive.
evalLaurentCoeff sends T^ℓ to v^ℓ·X^{(bℓ).toNat}. This is the key evaluation formula for Laurent monomials.
evalLaurentCoeff is multiplicative on monomials.
Full evaluation map from JacobiRing to ℚ⟦X⟧. Sends a power series f = ∑_e c_e · q^e (where c_e ∈ LaurentPolynomial ℤ) to ∑_e evalLaurentCoeff(c_e) · u^e · X^{ae}.
This is well-defined when:
- a > 0 (ensures exponents ae are nonnegative for e ≥ 0)
- a ≥ |b| (ensures exponents ae + bℓ are nonnegative for all ℓ in supports)
Equations
- AlgebraicCombinatorics.evalJacobi a b u v f = ∑' (e : ℕ), u ^ e • AlgebraicCombinatorics.evalLaurentCoeff b v ((PowerSeries.coeff e) f) * PowerSeries.X ^ (a * ↑e).toNat
Instances For
Corrected evaluation infrastructure #
The original evalJacobi has a bug: it computes X^{ae} · X^{(bℓ).toNat} instead of
X^{(ae + bℓ).toNat}. These differ when bℓ < 0 but ae + bℓ ≥ 0.
We fix this by defining evalJacobiCorrect that computes the combined exponent directly.
Evaluation of a Laurent polynomial coefficient with a shift parameter. For c ∈ LaurentPolynomial ℤ and shift e, evaluate at z = v·X^b with base exponent a·e. This sends T^ℓ → v^ℓ·X^{(a·e + b·ℓ).toNat}, computing the combined exponent correctly.
Equations
Instances For
evalLaurentCoeffShifted sends T^ℓ to v^ℓ·X^{(a·e + b·ℓ).toNat}.
Coefficient of evalLaurentCoeffShifted_T at a specific power. This is key for the reindexing argument in evalJacobiCorrect_jacobiRHS'.
evalLaurentCoeffShifted is additive.
evalLaurentCoeffShifted distributes over finite sums.
Corrected full evaluation map from JacobiRing to ℚ⟦X⟧. This version computes the combined exponent (a·e + b·ℓ).toNat correctly, avoiding the truncation issue in the original evalJacobi.
Equations
- AlgebraicCombinatorics.evalJacobiCorrect a b u v f = ∑' (e : ℕ), u ^ e • AlgebraicCombinatorics.evalLaurentCoeffShifted a b v e ((PowerSeries.coeff e) f)
Instances For
Roadmap for completing jacobi_triple_product via evaluation #
The alternative proof approach uses jacobi_triple_product_fps' (proved later in this file)
which shows jacobiLHS' = jacobiRHS' in JacobiRing = PowerSeries (LaurentPolynomial ℤ).
To derive jacobi_triple_product (the evaluated form), we need:
evalJacobiCorrect_jacobiRHS':
evalJacobiCorrect a b u v jacobiRHS' = jacobiRHSEval a b u vProof sketch:
jacobiRHS' = ∑' ℓ, jacobiSumTerm ℓwherejacobiSumTerm ℓ = X^{ℓ²} · C(T^ℓ)- The coefficient of
q^{ℓ²}injacobiSumTerm ℓisT^ℓ - By
evalLaurentCoeffShifted_T: evaluation givesv^ℓ · X^{(aℓ² + bℓ).toNat} - So
evalJacobiCorrectofjacobiSumTerm ℓisu^{ℓ²} · v^ℓ · X^{(aℓ² + bℓ).toNat} - Summing over ℓ gives
jacobiRHSEval
evalJacobiCorrect_jacobiLHS':
evalJacobiCorrect a b u v jacobiLHS' = jacobiLHSEval a b u vThis is more complex because
jacobiLHS'is an infinite product. Proof sketch:jacobiLHS' = ∏' n, jacobiProductTerm n- Each
jacobiProductTerm ninvolves factors(1 + X^{2n-1} · C(T^1)), etc. - The evaluation preserves products (needs ring homomorphism property)
- Each factor evaluates to the corresponding factor in
jacobiLHSEval
jacobi_triple_product_via_evalCorrect: Alternative proof using evaluation
jacobiLHSEval = evalJacobiCorrect jacobiLHS' -- by evalJacobiCorrect_jacobiLHS' = evalJacobiCorrect jacobiRHS' -- by jacobi_triple_product_fps' = jacobiRHSEval -- by evalJacobiCorrect_jacobiRHS'
Current status: Corrected infrastructure added. The key lemmas need to be proved.
Helper: evalJacobiCorrect applied to a single jacobiSumTerm ℓ gives the ℓ-th term of jacobiRHSEval.
This is the key computation: for jacobiSumTerm ℓ = X^{ℓ²} · C(T^ℓ), we have evalJacobiCorrect a b u v (jacobiSumTerm ℓ) = u^{ℓ²} · v^ℓ · X^{(aℓ² + bℓ).toNat}
The proof uses:
- coeff e (jacobiSumTerm ℓ) = T ℓ if e = ℓ², else 0
- evalLaurentCoeffShifted_T: evaluation of T ℓ gives v^ℓ · X^{(ae + bℓ).toNat}
- Only the term at e = ℓ² contributes to the tsum
Key exponent identity: a * ℓ.natAbs² + b * ℓ = a * ℓ² + b * ℓ as integers. This is because ℓ.natAbs² = ℓ² for any integer ℓ (squares are always nonnegative). This is used in the reindexing argument for evalJacobiCorrect_jacobiRHS'.
The coefficient of X^n in evalJacobiCorrect(jacobiSumTerm ℓ) equals u^{ℓ²} * v^ℓ when (aℓ² + bℓ).toNat = n, and 0 otherwise.
This is a key step in proving evalJacobiCorrect_jacobiRHS' - it shows that each
term in the sum contributes exactly when the exponent matches.
Summability of the evaluated Jacobi sum terms in the Pi topology. This shows that ∑' ℓ, evalJacobiCorrect(jacobiSumTerm ℓ) is well-defined.
The RHS tsum equals jacobiRHSEval by definition (after simplification).
This is immediate from evalJacobiCorrect_jacobiSumTerm and the definition of jacobiRHSEval.
The coefficient tsum simplifies to a finite sum over matching ℓ values.
Bijection Infrastructure for Coefficient Equality #
These lemmas establish the key bijection argument for proving
coeff_double_sum_eq_coeff_stateGenFun. Both sums can be reindexed to sums
over states with a given energy, and the value at each state is T(parnum(S)).
The set of states with a given energy is finite.
Equations
Instances For
The set of states with energy = d is finite.
The sum over (P, N) pairs equals the sum over states with the same energy.
This is one half of the bijection argument for coeff_double_sum_eq_coeff_stateGenFun.
The sum over (ℓ, μ) pairs equals the sum over states with the same energy.
This is the other half of the bijection argument for coeff_double_sum_eq_coeff_stateGenFun.
State Generating Function Infrastructure #
The key to proving Jacobi's triple product identity is the "state generating function": ∑_{S state} q^{energy(S)} z^{parnum(S)}
Both the LHS and RHS of the identity, when multiplied by the partition generating function ∏_{k>0} (1-q^{2k})^{-1}, equal this state generating function.
For the RHS: RHS · ∏{k>0} (1-q^{2k})^{-1} = ∑{ℓ∈ℤ} q^{ℓ²} z^ℓ · ∑{μ partition} q^{2|μ|} = ∑{ℓ∈ℤ} ∑_{μ partition} q^{ℓ² + 2|μ|} z^ℓ
By the bijection partitionToState_bijective, this equals: ∑_{S state} q^{energy(S)} z^{parnum(S)}
since energy(E_{ℓ,μ}) = ℓ² + 2|μ| and parnum(E_{ℓ,μ}) = ℓ.
For the LHS: LHS · ∏{k>0} (1-q^{2k})^{-1} = ∏{k>0}((1+q^{2k-1}z)(1+q^{2k-1}z^{-1}))
Using binary expansion, this product equals: ∑{P,N finite} q^{∑{p∈P}(2p-1) + ∑_{n∈N}(2n-1)} z^{|P| - |N|}
which is exactly the state generating function.
Key lemma: The RHS of Jacobi's identity can be rewritten using the bijection.
The sum ∑{ℓ∈ℤ} ∑{μ partition} q^{ℓ² + 2|μ|} z^ℓ can be reindexed using the bijection partitionToState_bijective to give ∑_{S state} q^{energy(S)} z^{parnum(S)}.
This is because:
- excitedState_energy: energy(E_{ℓ,μ}) = ℓ² + 2|μ|
- excitedState_parnum: parnum(E_{ℓ,μ}) = ℓ
- partitionToState_bijective: the map (ℓ, μ) ↦ E_{ℓ,μ} is a bijection onto states
This lemma shows that for each (ℓ, μ) pair, the term in the algebraic RHS matches the corresponding term in the state generating function.
Lemma for Substitution #
Lemma \ref{lem.fps.fxx=gxx}: If f[x²] = g[x²], then f = g.
This justifies "substituting x for x²" in the proof of Euler's pentagonal theorem from Jacobi's triple product identity.
The key insight is: if f = ∑_n f_n x^n and g = ∑_n g_n x^n, then f[x²] = ∑_n f_n x^{2n} and g[x²] = ∑_n g_n x^{2n}
So if f[x²] = g[x²], comparing x^{2n}-coefficients gives f_n = g_n for all n, hence f = g.
Here f[x²] denotes the substitution of x² for x in f, i.e., PowerSeries.subst (X^2) f.
This substitution is well-defined because X² has zero constant coefficient,
satisfying the HasSubst condition.
Transfer from ℚ to ℤ for Euler's Pentagonal Number Theorem #
The proof of Euler's pentagonal number theorem proceeds by:
- Proving the identity over ℚ using Jacobi's triple product
- Transferring from ℚ to ℤ using the fact that both sides have integer coefficients
The key lemma eulerProduct_coeff_map shows that the coefficients of eulerProduct
are compatible with the ring homomorphism ℤ → ℚ.
The eulerProduct coefficients are compatible with ring homomorphisms.
The n-th coefficient of eulerProduct over ℤ, when cast to ℚ, equals the n-th coefficient
of eulerProduct over ℚ. This follows from the fact that MvPowerSeries.map commutes
with tprod for continuous ring homomorphisms.
This lemma is key for transferring euler_pentagonal_number_theorem_rat from ℚ to ℤ.
Connecting Lemmas for Euler's Pentagonal Number Theorem #
These lemmas connect jacobiLHSEval and jacobiRHSEval at the specific parameters
(a=3, b=1, u=1, v=-1) to eulerProduct and pentagonalSeries respectively.
Together with jacobi_triple_product and fps_eq_of_sq_eq, they complete the proof
of Euler's pentagonal number theorem.
Key property of pentagonalNumberInverse: if it returns some k, then pentagonalNumber k = m.
The proof follows from the definition: pentagonalNumberInverse searches through k values in a bounded range and returns some k only when pentagonalNumber k = m.
If pentagonalNumber k = m, then pentagonalNumberInverse m returns some k' with pentagonalNumber k' = m. Combined with injectivity, k' = k.
Euler's pentagonal theorem for ℚ⟦X⟧, derived from Jacobi's triple product.
This is the key intermediate step: we prove the identity over ℚ first, then transfer to ℤ using the fact that both sides have integer coefficients.
Euler's Pentagonal Number Theorem (Main Result) #
Euler's Pentagonal Number Theorem (Theorem \ref{thm.pars.pent})
The infinite product equals the alternating sum of powers at pentagonal numbers: ∏{k=1}^∞ (1 - x^k) = ∑{k∈ℤ} (-1)^k x^{w_k}
Concretely: = 1 - x - x² + x⁵ + x⁷ - x¹² - x¹⁵ + x²² + x²⁶ ∓ ...
The proof transfers from ℚ to ℤ using euler_pentagonal_number_theorem_rat and
the fact that both sides have integer coefficients.
partitionGenFun * pentagonalSeries = 1
Corollary \ref{cor.pars.pn-rec}: Recursive formula for partition numbers.
For each positive integer n: p(n) = ∑_{k∈ℤ, k≠0} (-1)^{k-1} p(n - w_k) = p(n-1) + p(n-2) - p(n-5) - p(n-7) + p(n-12) + p(n-15) - ...
where p(m) = 0 for m < 0.
Note: The sign (-1)^{k-1} is computed using (k.natAbs + 1) % 2 to handle
negative k correctly. For k ≠ 0, (-1)^{k-1} equals (-1)^{|k|-1} = (-1)^{|k|+1}.
Euler's Recursion for Sum of Divisors #
The sum of divisors generating function: S = ∑_{k>0} σ(k) x^k. This is the generating function for the sum of divisors function σ₁.
Equations
- AlgebraicCombinatorics.sigmaSeries = PowerSeries.mk fun (n : ℕ) => if n = 0 then 0 else ↑((ArithmeticFunction.sigma 1) n)
Instances For
Coefficient of the pentagonal series.
Coefficient of the derivative of the pentagonal series.
Coefficient of x times the derivative of the pentagonal series. For n > 0, this equals n * pentagonalCoeff n. For n = 0, this is 0.
Express the coefficient of x * Q' in terms of pentagonalNumberInverse. The coefficient is (-1)^|k| * n if n = w_k for some k, and 0 otherwise.
Helper Lemmas for the Partition-Sigma Identity #
Key Combinatorial Identity: n * p(n) = ∑_{k=1}^n σ_1(k) * p(n-k)
This identity relates the partition function p(n) to the sum of divisors function σ_1.
Proof Approaches #
1. Logarithmic Derivative (Classical) #
Since P = ∏_{k≥1} 1/(1-X^k), we have:
- log(P) = -∑{k≥1} log(1-X^k) = ∑{k≥1} ∑_{m≥1} X^{km}/m
- X * d/dX log(P) = ∑{k≥1} ∑{m≥1} k * X^{km} = ∑_{n≥1} σ_1(n) * X^n = S
- Since d/dX log(P) = P'/P, we get X * P'/P = S, hence X * P' = S * P.
This approach requires PowerSeries.log which is not yet in Mathlib.
2. Combinatorial Bijection #
The identity can be proved by establishing a bijection between:
- Type A: Pairs (λ, cell) where λ partitions n and cell ∈ {1,...,n} marks a cell in the Young diagram
- Type B: Quadruples (d, m, j, μ) where:
- d ≥ 1 is a part size
- m ≥ 1 is a multiplicity (so md ≤ n)
- j ∈ {1,...,d} is a position within a row
- μ partitions n - md
The bijection:
- Forward: (λ, cell) → (d, m, j, μ) where d = length of row containing cell, m = count of d-rows in λ, j = position of cell in its row, μ = λ minus all d-rows
- Backward: (d, m, j, μ) → (λ, cell) where λ = μ plus m rows of length d, cell = position j in the first new row
Counting:
- |Type A| = n * p(n) (n cells per partition, p(n) partitions)
- |Type B| = ∑{d,m: md≤n} d * p(n-md) = ∑{k=1}^n (∑{d|k} d) * p(n-k) = ∑{k=1}^n σ_1(k) * p(n-k)
3. Direct Verification #
One can verify the identity directly by computing both sides for each n, using the recursive formula for p(n) from Euler's pentagonal theorem.
Note #
This lemma is the key remaining piece for proving euler_sum_divisors_recursive.
The bijection approach is the most elementary but requires formalizing Young diagrams
and cell positions. The logarithmic derivative approach is cleaner but requires
infrastructure for power series logarithms.
The identity X * P' = S * P, where P is the partition generating function and S is the sum of divisors generating function.
This is equivalent to the classical identity: n * p(n) = ∑_{k=1}^n σ(k) * p(n-k)
which is proved in partition_sigma_identity.
The proof follows from the logarithmic derivative of the partition generating function. Since P = ∏{k≥1} 1/(1-x^k), we have: log(P) = -∑{k≥1} log(1-x^k) = ∑{k≥1} ∑{m≥1} x^{km}/m X * d/dx log(P) = ∑{k≥1} ∑{m≥1} k * x^{km} = ∑_{n≥1} σ(n) * x^n = S Since d/dx log(P) = P'/P, we get X * P'/P = S, i.e., X * P' = S * P.
The key identity x * Q' = -Q * S, where Q is the pentagonal series and S is the sum of divisors generating function.
This follows from Euler's pentagonal number theorem (PQ = 1 where P is the partition generating function) and the identity xP' = SP. Taking the derivative of PQ = 1 gives P'Q + PQ' = 0, so Q' = -P'Q/P. Multiplying by x: xQ' = -xP'Q/P = -SQ (using xP' = SP).
Note: This lemma depends on euler_pentagonal_number_theorem and partition_generating_function
which are being proved separately.
Coefficient of the sigma series.
The coefficient of x^n in Q * S (product of pentagonal series and sigma series). By the convolution formula, this is the sum over pairs (a, b) with a + b = n of pentagonalCoeff(a) * σ(b), where σ(0) = 0 by convention.
Since σ(0) = 0, only terms with b > 0 (i.e., a < n) contribute.
pentagonalCoeff at a pentagonal number equals (-1)^|k|.
pentagonalCoeff is zero at non-pentagonal numbers.
Coefficient extraction for -Q * S. The coefficient of x^n in -Q*S equals the negative of the sum over all k with w_k < n of (-1)^|k| * σ(n - w_k).
Proof outline #
The proof uses the convolution formula for power series multiplication: [x^n](Q * S) = ∑_{a+b=n} [x^a]Q * [x^b]S
Since [x^0]S = 0 (the sigma series has no constant term), only pairs with b > 0 contribute. For each such pair (a, b) with a + b = n and b > 0:
- [x^a]Q = pentagonalCoeff(a) is nonzero only when a = pentagonalNumber(k) for some k
- When a = pentagonalNumber(k), [x^a]Q = (-1)^|k|
- We have b = n - a = n - pentagonalNumber(k)
- [x^b]S = σ(b) = σ(n - pentagonalNumber(k))
The sum over (a, b) with a pentagonal can be reindexed to a sum over k with w_k < n. The condition w_k < n ensures b = n - w_k > 0 (so σ(b) is well-defined).
The tsum over the finite subtype {k : ℤ // pentagonalNumber k < n} equals a Finset.sum
because the subtype is finite (by pentagonal_below_fintype).
Theorem \ref{thm.pars.euler-sum-div-rec}: Euler's recursion for the sum of divisors.
For each positive integer n: ∑_{k∈ℤ, w_k < n} (-1)^k σ(n - w_k) = { (-1)^{k-1} n, if n = w_k for some k ∈ ℤ { 0, otherwise
where σ(n) is the sum of all positive divisors of n.
The proof compares coefficients of x^n in the identity x * Q' = -Q * S, where Q is the pentagonal series and S is the sum of divisors generating function.
Note: The sign (-1)^k is computed using k.natAbs to handle negative k correctly.
For any integer k, (-1)^k = (-1)^|k| since (-1)^{-m} = (-1)^m.
Similarly, (-1)^{k-1} = (-1)^{|k|+1} for k ≠ 0.
Proof Strategy (from tex source) #
The proof requires Euler's pentagonal number theorem (euler_pentagonal_number_theorem)
which states: ∏{k≥1} (1 - x^k) = ∑{k∈ℤ} (-1)^k x^{w_k}
The key identity used is: xQ' = -QS where
- Q = ∑_{k∈ℤ} (-1)^k x^{w_k} (pentagonal series)
- S = ∑_{n>0} σ(n) x^n (sum of divisors generating function)
- P = ∑_{n≥0} p(n) x^n (partition generating function)
This is derived from:
- PQ = 1 (from Euler's pentagonal theorem and partition generating function)
- xP' = SP (identity relating partition function derivative to σ)
- Taking derivatives and using PQ = 1 gives xQ' = -QS
Then comparing coefficients of x^n on both sides of ∑_{k∈ℤ} (-1)^k w_k x^{w_k} = -QS gives the result.
Blocking Dependencies #
- Power series infrastructure for xP' = SP identity
Additional Infrastructure for Jacobi Triple Product #
The following lemmas provide additional infrastructure for the proof of
jacobi_triple_product_fps'. They establish key coefficient properties
for both the LHS and RHS of the identity.
The constant term of jacobiFactorZ n equals 1. This follows from the fact that (jacobiFactorZ n - 1) has order ≥ 2n+1 > 0.
The constant term of jacobiFactorZInv n equals 1.
The constant term of jacobiFactorQ n equals 1.
The constant term of jacobiProductTerm n equals 1. This is a key fact: each factor in the Jacobi product has constant term 1.
The coefficient of q^0 in jacobiRHS' equals 1.
This is because only ℓ = 0 contributes to the coefficient of q^0, and jacobiSumTerm 0 = q^0 * T(0) = 1.
The coefficient of q^n in jacobiRHS' for a perfect square n = k².
For n = k² with k > 0, exactly two values ℓ = k and ℓ = -k contribute, giving T(k) + T(-k) = z^k + z^{-k}.
The coefficient of q^n in jacobiRHS' for a non-perfect-square n.
If n is not a perfect square, no ℓ satisfies ℓ² = n, so the coefficient is 0.
Moved Lemmas: coeff_double_sum_eq_coeff_stateGenFun and dependencies #
These lemmas were moved here from earlier in the file because they depend on
the State infrastructure and finsetPair_sum_eq_partition_sum.
The coefficient of X^d in the double sum over (P, N) pairs equals the coefficient of X^d in the state generating function.
This is the key lemma connecting the binary expansion of the Jacobi product to the state generating function. The proof uses the bijection: (P, N) ↔ State S ↔ (ℓ, μ) where energy and parnum are preserved.
This is documented in tex source lines 500-570 of PentagonalJacobi.tex.
Key lemma 3: ZZProduct = stateGenFun (binary expansion). The product ∏{n>0}((1+q^{2n-1}z)(1+q^{2n-1}z^{-1})) expands via binary enumeration to the state generating function ∑{S state} q^{energy(S)} z^{parnum(S)}.
This is because:
- The product over positive levels (1+q^{2p}z) for p > 0 gives ∑{P finite} ∏{p∈P} q^{2p}z
- The product over negative levels (1+q^{-2p}z^{-1}) for p < 0 gives ∑{N finite} ∏{p∈N} q^{-2p}z^{-1}
- Combining these gives the state generating function via the bijection between pairs (P, N) and states.
RABBIT HOLE NOTE: This lemma is used by jacobi_triple_product_fps' (thm.pars.jtp1),
but is NOT on the critical path for jacobi_triple_product (thm.pars.jtp2). The evaluated
form (jtp2) uses a different route via jacobiLHS_mul_partitionGenFun.
Jacobi's Triple Product Identity (Theorem \ref{thm.pars.jtp1})
In the ring (ℤ[z^±])[[q]], we have: ∏{n>0} ((1 + q^{2n-1}z)(1 + q^{2n-1}z^{-1})(1 - q^{2n})) = ∑{ℓ∈ℤ} q^{ℓ²} z^ℓ
This is the main form of Jacobi's triple product identity, stated in the ring JacobiRing = (ℤ[z^±])[[q]] = PowerSeries (LaurentPolynomial ℤ).
The left-hand side jacobiLHS' is the infinite product defined using:
jacobiZ= T(1), the indeterminate zjacobiZInv= T(-1), the inverse z⁻¹jacobiProductTerm n= (1 + q^{2n+1}z)(1 + q^{2n+1}z⁻¹)(1 - q^{2(n+1)})
The right-hand side jacobiRHS' is the infinite sum:
jacobiSumTerm ℓ= q^{ℓ²} z^ℓ
Note: The identity is stated in the specific ring JacobiRing with:
- q = X (the power series indeterminate)
- z = T(1) (the Laurent polynomial indeterminate)
A parameterized version jacobiLHS q z for arbitrary q, z would be mathematically
ill-formed because z⁻¹ does not exist for arbitrary z. The identity only makes
sense when z is invertible, which is the case in JacobiRing where z = T(1).
The proof uses Borcherds' approach via states and energy/particle number, as implemented in the State infrastructure above.
Evaluation of jacobiLHS' using the corrected evaluation gives jacobiLHSEval.
This proof uses the chain:
jacobi_triple_product_fps':jacobiLHS' = jacobiRHS'evalJacobiCorrect_jacobiRHS':evalJacobiCorrect jacobiRHS' = jacobiRHSEvaljacobi_triple_product:jacobiLHSEval = jacobiRHSEval
The lemma is placed here (after jacobi_triple_product_fps') because it depends on that theorem
which was not available at the original location in the file.
Alternative proof of Jacobi's triple product identity using the corrected evaluation homomorphism.
This proof derives jacobi_triple_product from jacobi_triple_product_fps' (which is fully proved)
by showing that the corrected evaluation map sends jacobiLHS' to jacobiLHSEval and jacobiRHS' to
jacobiRHSEval.
This approach bypasses the file ordering issue in jacobiLHS_mul_partitionGenFun by using
the independent proof path through the State infrastructure.
Note: This uses evalJacobiCorrect which computes combined exponents correctly, unlike
the original evalJacobi which has truncation issues with negative intermediate exponents.