Mixed fixed-point convolution

Expresses the colour character of a lifted permutation as a convolution over tail-content vectors.

theorem RS.colourChar_viaEmbedding {m n N : ℕ} (h : m ≤ n) (σ : Equiv.Perm (Fin m)) (α : Fin N → ℕ) : colourChar α ((Equiv.Perm.viaEmbeddingHom (Fin.castLEEmb h)) σ) = ∑ w ∈ Fintype.piFinset fun (x : Fin N) => Finset.range (n + 1), if ∀ (a : Fin N), w a ≤ α a then colourChar (fun (a : Fin N) => α a - w a) σ * {t : { i : Fin n // m ≤ ↑i } → Fin N | ∀ (a : Fin N), {i : { i : Fin n // m ≤ ↑i } | t i = a}.card = w a}.card else 0

The colour character of a lifted permutation is a convolution over how the free tail is coloured.