Normal Ordering Coefficients (Lemma 8.5)

This file defines the normal ordering coefficients b_{ij}(ℓ) from Lemma 8.5 of Stanley's Algebraic Combinatorics.

Given operators D, U with DU - UD = I, the expansion (D+U)^ℓ = ∑ b_{ij}(ℓ) U^i D^j has coefficients normalOrderCoeff i j ℓ defined via the recurrence (Equation 47):

b_{ij}(ℓ+1) = b_{i,j-1}(ℓ) + (i+1) b_{i+1,j}(ℓ) + b_{i-1,j}(ℓ)

with initial condition b_{0,0}(0) = 1, b_{i,j}(0) = 0 for (i,j) ≠ (0,0). This recurrence is derived from (D+U)^{ℓ+1} = (D+U)(D+U)^ℓ and the commutation relation DU^i = U^i D + iU^{i-1} (which follows from DU - UD = I).

Lemma 8.5 (Theorem normalOrderCoeff_eq_bijCoeffFormula) proves these coefficients equal the closed form:

• b_{ij}(ℓ) = 0 if ℓ - i - j is odd or ℓ < i + j
• b_{ij}(ℓ) = ℓ! / (2^m · i! · j! · m!) if ℓ - i - j = 2m ≥ 0

The proof is by induction on ℓ: verify the initial condition, then show the closed form satisfies recurrence (47).

Definition via recurrence

def NormalOrderCoeff.normalOrderCoeff : ℕ → ℕ → ℕ → ℚ

The normal ordering coefficient b_{ij}(ℓ) capturing the coefficients in the operator expansion (D+U)^ℓ = ∑ b_{ij}(ℓ) U^i D^j where D, U satisfy DU - UD = I.

Defined by the recurrence (Equation 47): b_{ij}(ℓ+1) = b_{i,j-1}(ℓ) + (i+1) · b_{i+1,j}(ℓ) + b_{i-1,j}(ℓ) with initial condition b_{0,0}(0) = 1 and b_{i,j}(0) = 0 for (i,j) ≠ (0,0).

@[simp]

theorem NormalOrderCoeff.normalOrderCoeff_base (i j : ℕ) : normalOrderCoeff i j 0 = if i = 0 ∧ j = 0 then 1 else 0

theorem NormalOrderCoeff.normalOrderCoeff_succ (i j ℓ : ℕ) : normalOrderCoeff i j (ℓ + 1) = (if j = 0 then 0 else normalOrderCoeff i (j - 1) ℓ) + ↑(i + 1) * normalOrderCoeff (i + 1) j ℓ + if i = 0 then 0 else normalOrderCoeff (i - 1) j ℓ

Closed-form formula

def NormalOrderCoeff.bijCoeffFormula (i j ℓ : ℕ) : ℚ

The closed-form expression for the normal ordering coefficient from Lemma 8.5, Equation 45: ℓ! / (2^m · i! · j! · m!) when ℓ - i - j = 2m ≥ 0, and 0 otherwise.

Basic properties of the formula

theorem NormalOrderCoeff.bijCoeffFormula_eq_zero_of_gt {i j ℓ : ℕ} (h : ℓ < i + j) : bijCoeffFormula i j ℓ = 0

bijCoeffFormula i j ℓ = 0 when ℓ < i + j.

theorem NormalOrderCoeff.bijCoeffFormula_eq_zero_of_odd {i j ℓ : ℕ} (h : (ℓ - i - j) % 2 = 1) : bijCoeffFormula i j ℓ = 0

bijCoeffFormula i j ℓ = 0 when ℓ - i - j is odd.

theorem NormalOrderCoeff.bijCoeffFormula_of_valid {i j ℓ : ℕ} (hij : i + j ≤ ℓ) (heven : (ℓ - i - j) % 2 = 0) : bijCoeffFormula i j ℓ = ↑ℓ.factorial / (2 ^ ((ℓ - i - j) / 2) * ↑i.factorial * ↑j.factorial * ↑((ℓ - i - j) / 2).factorial)

When i + j ≤ ℓ and ℓ - i - j is even, the formula unfolds to the closed form.

theorem NormalOrderCoeff.bijCoeffFormula_eq_zero {i j ℓ : ℕ} (h : ¬(i + j ≤ ℓ ∧ (ℓ - i - j) % 2 = 0)) : bijCoeffFormula i j ℓ = 0

bijCoeffFormula i j ℓ = 0 when the validity condition fails.

Private helper lemmas for the recurrence verification

The closed form satisfies the recurrence (Equation 47)

theorem NormalOrderCoeff.bijCoeffFormula_recurrence (i j ℓ : ℕ) : bijCoeffFormula i j (ℓ + 1) = (if j = 0 then 0 else bijCoeffFormula i (j - 1) ℓ) + ↑(i + 1) * bijCoeffFormula (i + 1) j ℓ + if i = 0 then 0 else bijCoeffFormula (i - 1) j ℓ

Equation 47. The closed-form formula satisfies the recurrence b_{ij}(ℓ+1) = b_{i,j-1}(ℓ) + (i+1) · b_{i+1,j}(ℓ) + b_{i-1,j}(ℓ).

This is verified by direct computation — the book says it is "a routine matter to check".

Lemma 8.5: The recurrence-defined coefficients equal the closed form

theorem NormalOrderCoeff.bijCoeffFormula_zero (i j : ℕ) : bijCoeffFormula i j 0 = if i = 0 ∧ j = 0 then 1 else 0

Base case helper: bijCoeffFormula i j 0 = if i = 0 ∧ j = 0 then 1 else 0.

theorem NormalOrderCoeff.normalOrderCoeff_eq_bijCoeffFormula (i j ℓ : ℕ) : normalOrderCoeff i j ℓ = bijCoeffFormula i j ℓ

Lemma 8.5. The normal ordering coefficients b_{ij}(ℓ), defined by the recurrence (Equation 47) derived from (D+U)^ℓ = ∑ b_{ij}(ℓ) U^i D^j and DU - UD = I, satisfy:

• b_{ij}(ℓ) = 0 if ℓ - i - j is odd or ℓ < i + j
• b_{ij}(ℓ) = ℓ! / (2^m · i! · j! · m!) if ℓ - i - j = 2m ≥ 0

The proof is by induction on ℓ: verify the base case b_{0,0}(0) = 1, then use the fact that the closed form satisfies the same recurrence (47) to conclude equality at all levels.

Corollaries: properties of normalOrderCoeff

theorem NormalOrderCoeff.normalOrderCoeff_zero_zero_zero : normalOrderCoeff 0 0 0 = 1

b_{0,0}(0) = 1: the initial condition.

theorem NormalOrderCoeff.normalOrderCoeff_eq_zero_of_gt {i j ℓ : ℕ} (h : ℓ < i + j) : normalOrderCoeff i j ℓ = 0

b_{ij}(ℓ) = 0 when ℓ < i + j.

theorem NormalOrderCoeff.normalOrderCoeff_eq_zero_of_odd {i j ℓ : ℕ} (h : (ℓ - i - j) % 2 = 1) : normalOrderCoeff i j ℓ = 0

b_{ij}(ℓ) = 0 when ℓ - i - j is odd.

theorem NormalOrderCoeff.normalOrderCoeff_of_valid {i j ℓ : ℕ} (hij : i + j ≤ ℓ) (heven : (ℓ - i - j) % 2 = 0) : normalOrderCoeff i j ℓ = ↑ℓ.factorial / (2 ^ ((ℓ - i - j) / 2) * ↑i.factorial * ↑j.factorial * ↑((ℓ - i - j) / 2).factorial)

When i + j ≤ ℓ and ℓ - i - j is even, the coefficient equals the closed form.

theorem NormalOrderCoeff.normalOrderCoeff_one_zero_one : normalOrderCoeff 1 0 1 = 1

b_{1,0}(1) = 1.

theorem NormalOrderCoeff.normalOrderCoeff_zero_one_one : normalOrderCoeff 0 1 1 = 1

b_{0,1}(1) = 1.

Legacy aliases for backward compatibility

@[reducible, inline]

abbrev NormalOrderCoeff.bijCoeff : ℕ → ℕ → ℕ → ℚ

Legacy alias: bijCoeff is the recurrence-defined coefficient.

theorem NormalOrderCoeff.bij_recurrence (i j ℓ : ℕ) : normalOrderCoeff i j (ℓ + 1) = (if j = 0 then 0 else normalOrderCoeff i (j - 1) ℓ) + ↑(i + 1) * normalOrderCoeff (i + 1) j ℓ + if i = 0 then 0 else normalOrderCoeff (i - 1) j ℓ

The recurrence relation (Equation 47), now a direct consequence of the definition.

theorem NormalOrderCoeff.bijCoeff_of_valid {i j ℓ : ℕ} (hij : i + j ≤ ℓ) (heven : (ℓ - i - j) % 2 = 0) : bijCoeff i j ℓ = ↑ℓ.factorial / (2 ^ ((ℓ - i - j) / 2) * ↑i.factorial * ↑j.factorial * ↑((ℓ - i - j) / 2).factorial)

Alias of normalOrderCoeff_of_valid for bijCoeff.

theorem NormalOrderCoeff.bijCoeff_eq_zero_of_gt {i j ℓ : ℕ} (h : ℓ < i + j) : bijCoeff i j ℓ = 0

Alias of normalOrderCoeff_eq_zero_of_gt for bijCoeff.

theorem NormalOrderCoeff.bijCoeff_eq_zero_of_odd {i j ℓ : ℕ} (h : (ℓ - i - j) % 2 = 1) : bijCoeff i j ℓ = 0

Alias of normalOrderCoeff_eq_zero_of_odd for bijCoeff.

theorem NormalOrderCoeff.bijCoeff_zero_zero_zero : bijCoeff 0 0 0 = 1

Alias of normalOrderCoeff_zero_zero_zero for bijCoeff.

Operator algebra: commutation identities from DU - UD = 1

theorem NormalOrderCoeff.comm_D_U_pow_succ {R : Type u_1} [Ring R] (D U : R) (hDU : D * U - U * D = 1) (n : ℕ) : D * U ^ (n + 1) = U ^ (n + 1) * D + (↑n + 1) * U ^ n

Equation 43. From the commutation relation D * U - U * D = 1, we derive by induction that D * U^(n+1) = U^(n+1) * D + (n+1) * U^n. This is the key identity used to derive the recurrence (Equation 47) for the normal ordering coefficients: multiplying (D+U) * (∑ b_{ij} U^i D^j) and using this identity on D * U^i yields the three terms b_{i,j-1}(ℓ), (i+1) · b_{i+1,j}(ℓ), and b_{i-1,j}(ℓ) in the recurrence.

theorem NormalOrderCoeff.comm_D_pow_U_succ {R : Type u_1} [Ring R] (D U : R) (hDU : D * U - U * D = 1) (j : ℕ) : D ^ (j + 1) * U = U * D ^ (j + 1) + (↑j + 1) * D ^ j

The dual commutation identity: D^(j+1) * U = U * D^(j+1) + (j+1) * D^j. This follows from DU - UD = 1 by induction on j, and is used when expanding (∑ b_{ij} U^i D^j) * U in the normal ordering expansion.

Operator expansion (Lemma 8.5, operator form)

def NormalOrderCoeff.pairsLE (ℓ : ℕ) : Finset (ℕ × ℕ)

The index set of pairs (i, j) with i + j ≤ ℓ, used to sum the normal order expansion.

@[simp]

theorem NormalOrderCoeff.mem_pairsLE {p : ℕ × ℕ} {ℓ : ℕ} : p ∈ pairsLE ℓ ↔ p.1 + p.2 ≤ ℓ

theorem NormalOrderCoeff.D_mul_U_pow_D_pow {R : Type u_1} [Ring R] (D U : R) (hDU : D * U - U * D = 1) (i j : ℕ) : D * (U ^ i * D ^ j) = U ^ i * D ^ (j + 1) + ↑i * (U ^ (i - 1) * D ^ j)

Key commutation identity: D * (U^i * D^j) = U^i * D^{j+1} + i * (U^{i-1} * D^j). Uses comm_D_U_pow_succ for i ≥ 1 and is trivial for i = 0.

theorem NormalOrderCoeff.normalOrder_expansion {R : Type u_1} [Ring R] [Algebra ℚ R] (D U : R) (hDU : D * U - U * D = 1) (ℓ : ℕ) : (D + U) ^ ℓ = ∑ p ∈ pairsLE ℓ, (algebraMap ℚ R) (normalOrderCoeff p.1 p.2 ℓ) * (U ^ p.1 * D ^ p.2)