Multilinearity of free cumulants

Let φ : A →ₗ[R] R be a linear functional on an R-algebra A. Every position i of a finite set s lies in exactly one part of a finite partition P of s, and appears exactly once in the word read along that part. Hence the block moment φ_P(a) is linear in the entry a i, and so is the free cumulant κ_π(a), which is a linear combination of block moments by Möbius inversion. In other words, the block moments and the free cumulants κ_n(a₁, …, aₙ) are multilinear functionals of their arguments.

The additive laws only require an additive map from a semiring A to a commutative semiring R (a commutative ring for cumulants), without a common scalar algebra.

Multilinearity is the basic tool for computing with cumulants: it reduces cumulants of sums and scalar multiples to cumulants of the summands, for example when splitting each argument into its centred part and a multiple of 1.

Main definitions

For a finite linear order α of positions, such as Fin n, the functionals on words indexed by all of α are bundled as multilinear maps (α → A) → R:

• TauCeti.partitionMomentMultilinear φ P — the block moment a ↦ φ_P(a);
• TauCeti.partitionCumulantMultilinear φ π — the free cumulant a ↦ κ_π(a);
• TauCeti.freeCumulantMultilinear φ — the free cumulant a ↦ κ_α(a); for α = Fin n with n ≥ 1 this is the n-th free cumulant κ_n as an element of MultilinearMap R (fun _ : Fin n => A) R.

Main results

• TauCeti.partitionMoment_update_add, TauCeti.partitionMoment_update_smul — the block moment φ_P(a) is linear in each entry a i with i ∈ s.
• TauCeti.partitionCumulant_update_add, TauCeti.partitionCumulant_update_smul, TauCeti.freeCumulant_update_add, TauCeti.freeCumulant_update_smul — the free cumulants κ_π(a) and κ_s(a) are linear in each entry a i with i ∈ s.
• TauCeti.freeCumulant_add_algebraMap — for a normalised φ, free cumulants of order at least two are invariant under adding scalars to their arguments, in particular under centring.
• TauCeti.freeCumulant_sum_smul — the free cumulant of linear combinations of a family expands as a sum over words in the family.

Implementation notes

The linearity of a block moment in a single entry is proved by writing the word of the part containing that entry as a list, updated at one index via List.Nodup.map_update, and splitting its product with List.prod_set. This follows the proof of multilinearity of ordered products in Mathlib's MultilinearMap.mkPiAlgebraFin.

References

• A. Nica, R. Speicher, Lectures on the Combinatorics of Free Probability, Lecture 11.

@[simp]

theorem TauCeti.partitionMoment_update_add {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommSemiring R] [Semiring A] {F : Type u_4} [FunLike F A R] [AddHomClass F A R] (φ : F) (a : α → A) (P : Finpartition s) {i : α} (hi : i ∈ s) (x y : A) : partitionMoment (⇑φ) (Function.update a i (x + y)) P = partitionMoment (⇑φ) (Function.update a i x) P + partitionMoment (⇑φ) (Function.update a i y) P

The block moment φ_P(a) is additive in each entry a i with i ∈ s.

@[simp]

theorem TauCeti.partitionMoment_update_smul {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommSemiring R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (a : α → A) (P : Finpartition s) {i : α} (hi : i ∈ s) (c : R) (x : A) : partitionMoment (⇑φ) (Function.update a i (c • x)) P = c * partitionMoment (⇑φ) (Function.update a i x) P

The block moment φ_P(a) is homogeneous in each entry a i with i ∈ s.

@[simp]

theorem TauCeti.partitionCumulant_update_add {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Semiring A] {F : Type u_4} [FunLike F A R] [AddHomClass F A R] (φ : F) (a : α → A) (π : NoncrossingPartition s) {i : α} (hi : i ∈ s) (x y : A) : partitionCumulant (⇑φ) (Function.update a i (x + y)) π = partitionCumulant (⇑φ) (Function.update a i x) π + partitionCumulant (⇑φ) (Function.update a i y) π

The free cumulant κ_π(a) is additive in each entry a i with i ∈ s.

@[simp]

theorem TauCeti.freeCumulant_update_add {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Semiring A] {F : Type u_4} [FunLike F A R] [AddHomClass F A R] (φ : F) (a : α → A) {i : α} (hi : i ∈ s) (x y : A) : freeCumulant (⇑φ) (Function.update a i (x + y)) s = freeCumulant (⇑φ) (Function.update a i x) s + freeCumulant (⇑φ) (Function.update a i y) s

The free cumulant κ_s(a) of a word is additive in each entry a i with i ∈ s.

theorem TauCeti.freeCumulant_eq_zero_of_apply_eq_zero {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Semiring A] {F : Type u_4} [FunLike F A R] [AddHomClass F A R] (φ : F) (a : α → A) {i : α} (hai : a i = 0) (hi : i ∈ s) : freeCumulant (⇑φ) a s = 0

A free cumulant for an additive map vanishes if one of its letters is zero.

@[simp]

theorem TauCeti.partitionCumulant_update_smul {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (a : α → A) (π : NoncrossingPartition s) {i : α} (hi : i ∈ s) (c : R) (x : A) : partitionCumulant (⇑φ) (Function.update a i (c • x)) π = c * partitionCumulant (⇑φ) (Function.update a i x) π

The free cumulant κ_π(a) is homogeneous in each entry a i with i ∈ s.

@[simp]

theorem TauCeti.freeCumulant_update_smul {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (a : α → A) {i : α} (hi : i ∈ s) (c : R) (x : A) : freeCumulant (⇑φ) (Function.update a i (c • x)) s = c * freeCumulant (⇑φ) (Function.update a i x) s

The free cumulant κ_s(a) of a word is homogeneous in each entry a i with i ∈ s.

theorem TauCeti.freeCumulant_add_algebraMap {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (a : α → A) (hφ : φ 1 = 1) (c : α → R) (hs : 1 < s.card) : freeCumulant (⇑φ) (fun (x : α) => a x + (algebraMap R A) (c x)) s = freeCumulant (⇑φ) a s

For a normalised φ, a free cumulant of order at least two is unchanged by adding scalar multiples of 1 to its arguments: κ_s(a + c • 1) = κ_s(a) when φ 1 = 1 and #s ≥ 2. In particular, centring the letters a x ↦ a x - φ (a x) • 1 does not change it.

@[simp]

theorem TauCeti.freeCumulant_algebraMap {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (hφ : φ 1 = 1) (c : α → R) (hs : 1 < s.card) : freeCumulant (⇑φ) (fun (i : α) => (algebraMap R A) (c i)) s = 0

Scalar words have vanishing free cumulants of order at least two for a normalised functional.

def TauCeti.partitionMomentMultilinear {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [Fintype α] [CommSemiring R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (P : Finpartition Finset.univ) : (α → A) →ₘₗ[R] R

The block moment a ↦ φ_P(a) of a finite partition P of all positions of a finite linear order α, as a multilinear map.

@[simp]

theorem TauCeti.partitionMomentMultilinear_apply {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [Fintype α] [CommSemiring R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (P : Finpartition Finset.univ) (a : α → A) : (partitionMomentMultilinear φ P) a = partitionMoment (⇑φ) a P

Evaluating the bundled block moment at a word gives its block moment.

def TauCeti.partitionCumulantMultilinear {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [Fintype α] [CommRing R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (π : NoncrossingPartition Finset.univ) : (α → A) →ₘₗ[R] R

The free cumulant a ↦ κ_π(a) of a noncrossing partition π of all positions of a finite linear order α, as a multilinear map.

@[simp]

theorem TauCeti.partitionCumulantMultilinear_apply {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [Fintype α] [CommRing R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (π : NoncrossingPartition Finset.univ) (a : α → A) : (partitionCumulantMultilinear φ π) a = partitionCumulant (⇑φ) a π

Evaluating the bundled free cumulant of π at a word gives its free cumulant.

def TauCeti.freeCumulantMultilinear {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [Fintype α] [CommRing R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) : (α → A) →ₘₗ[R] R

The free cumulant a ↦ κ_α(a) of the words indexed by a finite linear order α, as a multilinear map. For α = Fin n with n ≥ 1 this is the n-th free cumulant κ_n(a₁, …, aₙ).

@[simp]

theorem TauCeti.freeCumulantMultilinear_apply {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [Fintype α] [CommRing R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (a : α → A) : (freeCumulantMultilinear φ) a = freeCumulant (⇑φ) a Finset.univ

Evaluating the bundled free cumulant at a word gives the free cumulant of the whole word.

theorem TauCeti.freeCumulant_sum_smul {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [Fintype α] [CommRing R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) {ι : Type u_4} [DecidableEq α] [Fintype ι] (s : ι → A) (c : α → ι → R) : freeCumulant (⇑φ) (fun (m : α) => ∑ i : ι, c m i • s i) Finset.univ = ∑ v : α → ι, (∏ m : α, c m (v m)) * freeCumulant (⇑φ) (s ∘ v) Finset.univ

Multilinear expansion: the free cumulant of the linear combinations m ↦ ∑ i, c m i • s i is the sum, over all words v in the family s, of the product of the coefficients c m (v m) times the free cumulant of s ∘ v.

@[simp]

theorem TauCeti.freeCumulant_smul {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [CommRing R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (c : α → R) (a : α → A) (s : Finset α) : freeCumulant (⇑φ) (fun (i : α) => c i • a i) s = (∏ i ∈ s, c i) * freeCumulant (⇑φ) a s

Scaling each letter scales the free cumulant by the product of the corresponding scalars.