Free cumulants

Let φ : A → R be a function on a monoid A (in free probability, a linear functional on an algebra A, used through its coercion to a function), and let a : α → A assign an element of A to each position of a linear order α. For a finite set s of positions and a finite partition P of s, the block moment φ_P(a) is the product over the parts B of P of the moments φ (a_{b₁} * ⋯ * a_{bₖ}), where b₁ < ⋯ < bₖ lists B in increasing order.

The free cumulants are obtained from the block moments by Möbius inversion on the lattice NC(s) of noncrossing partitions of s: for π ∈ NC(s), κ_π(a) = ∑_{σ ≤ π} μ(σ, π) φ_σ(a), where μ is the Möbius function of NC(s), and the free cumulant of the word (a_i)_{i ∈ s} is κ_s(a) = κ_{1_s}(a) for the partition 1_s of s into one part. Equivalently, the cumulants are the unique family satisfying the moment–cumulant formula φ_π(a) = ∑_{σ ≤ π} κ_σ(a); in particular, for nonempty s, φ (a_{i₁} * ⋯ * a_{iₙ}) = ∑_{π ∈ NC(s)} κ_π(a) where i₁ < ⋯ < iₙ lists s. Taking s = Finset.univ : Finset (Fin n) gives the cumulants κ_n(a₁, …, aₙ) of free probability.

The cumulant of a noncrossing partition is the product of the cumulants of the words read along its parts, κ_π(a) = ∏_{B ∈ π} κ_B(a). This follows by induction from the factorisation of the lower interval [0_s, π] of NC(s) as the product of the lattices NC(B) over the parts B of π, and turns the moment–cumulant formula into its usual multiplicative form φ (a_{i₁} * ⋯ * a_{iₙ}) = ∑_{π ∈ NC(s)} ∏_{B ∈ π} κ_B(a).

When φ 1 = 1, a free cumulant of order at least two vanishes as soon as one of its arguments is the unit. In the moment–cumulant formula for such a word, the partitions in which the unit forms a part on its own reproduce the moment of the word with the unit deleted, and in every remaining partition other than 1_s the part through the unit gives a shorter cumulant with a unit argument.

Apart from that vanishing result, no normalisation φ 1 = 1 is assumed; positivity and traciality are never assumed. For s = ∅ the cumulant κ_∅(a) is the empty product 1; it carries no meaning, since free cumulants are indexed by n ≥ 1.

Main definitions

• TauCeti.partitionMoment φ a P — the block moment φ_P(a) of a finite partition P.
• TauCeti.partitionCumulant φ a π — the free cumulant κ_π(a) of a noncrossing partition π, defined by Möbius inversion on NC(s).
• TauCeti.freeCumulant φ a s — the free cumulant κ_s(a) of the word (a_i)_{i ∈ s}.

Main results

• TauCeti.sum_Iic_partitionCumulant — the moment–cumulant formula ∑_{σ ≤ π} κ_σ(a) = φ_π(a), and TauCeti.eq_partitionCumulant_of_forall_sum_Iic — the cumulants are the only family satisfying it.
• TauCeti.apply_prod_eq_sum_partitionCumulant and TauCeti.apply_prod_ofFn_eq_sum_partitionCumulant — a moment is the sum of the cumulants over all noncrossing partitions.
• TauCeti.freeCumulant_eq_sum_mu_mul_partitionMoment — the cumulant is the sum of the block moments weighted by μ(π, 1_s).
• TauCeti.partitionCumulant_eq_of_orderIso and TauCeti.freeCumulant_eq_of_orderIso — free cumulants transport along order isomorphisms of noncrossing partition lattices that match block moments.
• TauCeti.partitionCumulant_eq_prod_freeCumulant — the cumulants are multiplicative, κ_π(a) = ∏_{B ∈ π} κ_B(a); hence TauCeti.apply_prod_eq_sum_prod_freeCumulant and TauCeti.apply_prod_ofFn_eq_sum_prod_freeCumulant — a moment is the sum over all noncrossing partitions of the products of the cumulants along their parts.
• TauCeti.apply_pow_card_eq_sum_prod_freeCumulant — the same for the powers of one element, and TauCeti.freeCumulant_const_eq_of_forall_apply_pow — conversely, a sequence c that produces the moments of an element through this formula is its sequence of free cumulants.
• TauCeti.freeCumulant_eq_of_forall_apply_prod_eq_sum_prod — more generally, a function on the subsets of s that satisfies this multiplicative formula for every nonempty subset is the family of free cumulants.
• TauCeti.freeCumulant_singleton and TauCeti.freeCumulant_pair — the first two cumulants are the mean φ a_i and the covariance φ (a_i * a_j) - φ a_i * φ a_j.
• TauCeti.freeCumulant_const_of_card_eq_two — the second free cumulant of a constant word is the variance φ (x ^ 2) - φ x ^ 2.
• TauCeti.freeCumulant_eq_zero_of_apply_eq_one — if φ 1 = 1, the free cumulant of a word of length at least two with a unit argument vanishes.
• TauCeti.sum_prod_freeCumulant_mul_eq_sum_erase_of_apply_eq_one — a unit letter can be deleted from the multiplicative moment–cumulant sum, weighted by a function of the number of parts.
• TauCeti.partitionMoment_const — the block moment of a constant word (x, …, x) is the product of the moments φ (x ^ #B) over the parts B.
• TauCeti.partitionMoment_congr, TauCeti.partitionCumulant_congr and TauCeti.freeCumulant_congr — block moments and cumulants depend only on the letters at the positions of s.

References

• A. Nica, R. Speicher, Lectures on the Combinatorics of Free Probability, Lectures 10 and 11 (Proposition 11.15 for the vanishing of cumulants with a unit argument).
• R. Speicher, Multiplicative functions on the lattice of non-crossing partitions and free convolution, Math. Ann. 298 (1994), 611–628.

def TauCeti.partitionMoment {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommMonoid R] [Monoid A] (φ : A → R) (a : α → A) (P : Finpartition s) : R

The block moment φ_P(a) of a finite partition P of a set s of positions: the product over the parts B of P of φ (a_{b₁} * ⋯ * a_{bₖ}), where b₁ < ⋯ < bₖ lists B in increasing order.

theorem TauCeti.partitionMoment_def {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommMonoid R] [Monoid A] (φ : A → R) (a : α → A) (P : Finpartition s) : partitionMoment φ a P = ∏ B ∈ P.parts, φ (List.map a (B.sort fun (a b : α) => a ≤ b)).prod

Unfolding of the block moment.

theorem TauCeti.partitionMoment_congr {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommMonoid R] [Monoid A] (φ : A → R) {a b : α → A} (h : Set.EqOn a b ↑s) (P : Finpartition s) : partitionMoment φ a P = partitionMoment φ b P

The block moment φ_P(a) depends only on the letters of a at the positions of s.

@[simp]

theorem TauCeti.partitionMoment_const {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommMonoid R] [Monoid A] (φ : A → R) (x : A) (P : Finpartition s) : partitionMoment φ (fun (x_1 : α) => x) P = ∏ B ∈ P.parts, φ (x ^ B.card)

The block moment of a constant word (x, …, x) is the product over the parts B of the moments φ (x ^ #B).

@[simp]

theorem TauCeti.partitionMoment_bot {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommMonoid R] [Monoid A] (φ : A → R) (a : α → A) : partitionMoment φ a ⊥ = ∏ i ∈ s, φ (a i)

The block moment of the partition into singletons is the product of the individual moments.

@[simp]

theorem TauCeti.partitionMoment_top {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommMonoid R] [Monoid A] (φ : A → R) (a : α → A) (hs : s.Nonempty) : partitionMoment φ a ⊤ = φ (List.map a (s.sort fun (a b : α) => a ≤ b)).prod

The block moment of the partition of a nonempty set into one part is the moment of the whole word, read in increasing order.

def TauCeti.partitionCumulant {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (π : NoncrossingPartition s) : R

The free cumulant κ_π(a) of a noncrossing partition π of s, defined by Möbius inversion of the block moments on the lattice of noncrossing partitions: κ_π(a) = ∑_{σ ≤ π} μ(σ, π) φ_σ(a).

theorem TauCeti.partitionCumulant_def {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (π : NoncrossingPartition s) : partitionCumulant φ a π = ∑ σ ≤ π, (IncidenceAlgebra.mu R) σ π * partitionMoment φ a ↑σ

Unfolding of the free cumulant of a noncrossing partition.

def TauCeti.freeCumulant {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (s : Finset α) : R

The free cumulant κ_s(a) of the word (a_i)_{i ∈ s}: the cumulant of the partition of s into one part. For s = Finset.univ : Finset (Fin n) with n ≥ 1 this is the n-th free cumulant κ_n(a₁, …, aₙ); for s = ∅ it is the meaningless value 1.

theorem TauCeti.freeCumulant_def {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (s : Finset α) : freeCumulant φ a s = partitionCumulant φ a ⊤

Unfolding of the free cumulant of a word.

theorem TauCeti.partitionCumulant_congr {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) {a b : α → A} (h : Set.EqOn a b ↑s) (π : NoncrossingPartition s) : partitionCumulant φ a π = partitionCumulant φ b π

The free cumulant κ_π(a) depends only on the letters of a at the positions of s.

theorem TauCeti.freeCumulant_congr {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) {a b : α → A} (h : Set.EqOn a b ↑s) : freeCumulant φ a s = freeCumulant φ b s

The free cumulant κ_s(a) depends only on the letters of a at the positions of s.

theorem TauCeti.sum_Iic_partitionCumulant {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (π : NoncrossingPartition s) : ∑ σ ≤ π, partitionCumulant φ a σ = partitionMoment φ a ↑π

The moment–cumulant formula: the block moment of a noncrossing partition π is the sum of the free cumulants of the noncrossing partitions refining π.

theorem TauCeti.eq_partitionCumulant_of_forall_sum_Iic {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (c : NoncrossingPartition s → R) (hc : ∀ (π : NoncrossingPartition s), ∑ σ ≤ π, c σ = partitionMoment φ a ↑π) : c = partitionCumulant φ a

The free cumulants are the only family satisfying the moment–cumulant formula ∑_{σ ≤ π} c_σ = φ_π(a).

@[simp]

theorem TauCeti.partitionCumulant_bot {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (a : α → A) : partitionCumulant φ a ⊥ = ∏ i ∈ s, φ (a i)

The free cumulant of the partition into singletons is the product of the individual moments.

theorem TauCeti.freeCumulant_eq_sum_mu_mul_partitionMoment {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (s : Finset α) : freeCumulant φ a s = ∑ π : NoncrossingPartition s, (IncidenceAlgebra.mu R) π ⊤ * partitionMoment φ a ↑π

The free cumulant of a word is the sum over the noncrossing partitions π of its block moments weighted by the Möbius function, κ_s(a) = ∑_{π ∈ NC(s)} μ(π, 1_s) φ_π(a).

theorem TauCeti.freeCumulant_const_eq_of_apply_pow_eq {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [CommRing R] [Monoid A] (φ : A → R) {x y : A} (h : ∀ (k : ℕ), φ (x ^ k) = φ (y ^ k)) (s : Finset α) : freeCumulant φ (fun (x_1 : α) => x) s = freeCumulant φ (fun (x : α) => y) s

Elements with the same scalar moments have the same free cumulants on constant words.

theorem TauCeti.apply_prod_eq_sum_partitionCumulant {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (hs : s.Nonempty) : φ (List.map a (s.sort fun (a b : α) => a ≤ b)).prod = ∑ π : NoncrossingPartition s, partitionCumulant φ a π

The moment–cumulant formula for a word: a moment of a nonempty word is the sum of its free cumulants over all noncrossing partitions, φ (a_{i₁} * ⋯ * a_{iₙ}) = ∑_{π ∈ NC(s)} κ_π(a) for s = {i₁ < ⋯ < iₙ}.

theorem TauCeti.apply_prod_ofFn_eq_sum_partitionCumulant {R : Type u_1} {A : Type u_2} [CommRing R] [Monoid A] (φ : A → R) {n : ℕ} (hn : n ≠ 0) (a : Fin n → A) : φ (List.ofFn a).prod = ∑ π : NoncrossingPartition Finset.univ, partitionCumulant φ a π

The moment–cumulant formula for a word a₁, …, aₙ with n ≥ 1: φ (a₁ * ⋯ * aₙ) = ∑_{π ∈ NC(n)} κ_π(a₁, …, aₙ).

@[simp]

theorem TauCeti.freeCumulant_empty {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [CommRing R] [Monoid A] (φ : A → R) (a : α → A) : freeCumulant φ a ∅ = 1

The free cumulant of the empty word is the empty product 1.

@[simp]

theorem TauCeti.freeCumulant_singleton {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (i : α) : freeCumulant φ a {i} = φ (a i)

The first free cumulant is the mean, κ₁(a_i) = φ a_i.

theorem TauCeti.freeCumulant_pair {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [CommRing R] [Monoid A] (φ : A → R) (a : α → A) {i j : α} (hij : i < j) : freeCumulant φ a {i, j} = φ (a i * a j) - φ (a i) * φ (a j)

The second free cumulant is the covariance, κ₂(a_i, a_j) = φ (a_i * a_j) - φ a_i * φ a_j for positions i < j.

theorem TauCeti.freeCumulant_const_of_card_eq_two {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [CommRing R] [Monoid A] (φ : A → R) (x : A) {B : Finset α} (hB : B.card = 2) : freeCumulant φ (fun (x_1 : α) => x) B = φ (x ^ 2) - φ x ^ 2

The second free cumulant of a constant word is the variance of its letter, κ₂(x, x) = φ (x ^ 2) - φ x ^ 2.

theorem TauCeti.partitionCumulant_eq_prod_freeCumulant {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (π : NoncrossingPartition s) : partitionCumulant φ a π = ∏ B ∈ (↑π).parts, freeCumulant φ a B

The free cumulants are multiplicative: the free cumulant of a noncrossing partition is the product of the free cumulants of the words read along its parts, κ_π(a) = ∏_{B ∈ π} κ_B(a).

theorem TauCeti.partitionMoment_eq_sum_prod_freeCumulant {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (π : NoncrossingPartition s) : partitionMoment φ a ↑π = ∑ σ ≤ π, ∏ B ∈ (↑σ).parts, freeCumulant φ a B

The moment–cumulant formula in multiplicative form: the block moment of a noncrossing partition π is the sum, over the noncrossing partitions σ refining π, of the products of the free cumulants along the parts of σ.

theorem TauCeti.apply_prod_eq_sum_prod_freeCumulant {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (hs : s.Nonempty) : φ (List.map a (s.sort fun (a b : α) => a ≤ b)).prod = ∑ π : NoncrossingPartition s, ∏ B ∈ (↑π).parts, freeCumulant φ a B

The moment–cumulant formula for a nonempty word in multiplicative form: φ (a_{i₁} * ⋯ * a_{iₙ}) = ∑_{π ∈ NC(s)} ∏_{B ∈ π} κ_B(a) for s = {i₁ < ⋯ < iₙ}.

theorem TauCeti.apply_prod_ofFn_eq_sum_prod_freeCumulant {R : Type u_1} {A : Type u_2} [CommRing R] [Monoid A] (φ : A → R) {n : ℕ} (hn : n ≠ 0) (a : Fin n → A) : φ (List.ofFn a).prod = ∑ π : NoncrossingPartition Finset.univ, ∏ B ∈ (↑π).parts, freeCumulant φ a B

The moment–cumulant formula for a word a₁, …, aₙ with n ≥ 1 in multiplicative form: φ (a₁ * ⋯ * aₙ) = ∑_{π ∈ NC(n)} ∏_{B ∈ π} κ_B(a₁, …, aₙ).

theorem TauCeti.apply_pow_card_eq_sum_prod_freeCumulant {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (x : A) (hs : s.Nonempty) : φ (x ^ s.card) = ∑ π : NoncrossingPartition s, ∏ B ∈ (↑π).parts, freeCumulant φ (fun (x_1 : α) => x) B

The moment–cumulant formula for the powers of a single element: for nonempty s, φ (x ^ #s) = ∑_{π ∈ NC(s)} ∏_{B ∈ π} κ_B(x, …, x).

theorem TauCeti.freeCumulant_const_eq_of_forall_apply_pow {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) {x : A} (c : ℕ → R) (hs : s.Nonempty) (h : ∀ t ⊆ s, t.Nonempty → φ (x ^ t.card) = ∑ π : NoncrossingPartition t, ∏ B ∈ (↑π).parts, c B.card) : freeCumulant φ (fun (x_1 : α) => x) s = c s.card

The free cumulants of a single element are determined by its moments: if the moments of x are given by the moment–cumulant formula for a sequence c, that is φ (x ^ #t) = ∑_{π ∈ NC(t)} ∏_{B ∈ π} c #B for every nonempty t ⊆ s, then κ_s(x, …, x) = c #s.

theorem TauCeti.freeCumulant_eq_of_forall_apply_prod_eq_sum_prod {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (f : Finset α → R) (hf : ∀ X ⊆ s, X.Nonempty → φ (List.map a (X.sort fun (a b : α) => a ≤ b)).prod = ∑ π : NoncrossingPartition X, ∏ C ∈ (↑π).parts, f C) (hs : s.Nonempty) : freeCumulant φ a s = f s

The free cumulants are determined by the multiplicative moment–cumulant formula: if a function f on the subsets of s satisfies φ (a_{i₁} * ⋯ * a_{iₖ}) = ∑_{π ∈ NC(X)} ∏_{C ∈ π} f C for every nonempty X = {i₁ < ⋯ < iₖ} ⊆ s, then κ_s(a) = f s for nonempty s.

theorem TauCeti.freeCumulant_eq_zero_of_apply_eq_one {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (h1 : φ 1 = 1) {i : α} (hai : a i = 1) (hi : i ∈ s) (hs : 1 < s.card) : freeCumulant φ a s = 0

A free cumulant of order at least two vanishes as soon as one of its arguments is the unit, for a normalised φ: if φ 1 = 1, i ∈ s, a i = 1 and s has at least two elements, then κ_s(a) = 0.

theorem TauCeti.sum_prod_freeCumulant_mul_eq_sum_erase_of_apply_eq_one {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (h1 : φ 1 = 1) {i : α} (hai : a i = 1) (hi : i ∈ s) (w : ℕ → R) : ∑ π : NoncrossingPartition s, (∏ B ∈ (↑π).parts, freeCumulant φ a B) * w (↑π).parts.card = ∑ τ : NoncrossingPartition (s.erase i), (∏ B ∈ (↑τ).parts, freeCumulant φ a B) * w ((↑τ).parts.card + 1)

A unit letter can be deleted from the multiplicative moment–cumulant sum weighted by a function w of the number of parts: if φ 1 = 1, i ∈ s and a i = 1, then ∑_{π ∈ NC(s)} κ_π(a) w(#π) = ∑_{τ ∈ NC(s ∖ {i})} κ_τ(a) w(#τ + 1).

theorem TauCeti.partitionCumulant_eq_of_orderIso {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) {β : Type u_4} [LinearOrder β] {t : Finset β} {a : α → A} {b : β → A} (e : NoncrossingPartition s ≃o NoncrossingPartition t) (h : ∀ (π : NoncrossingPartition s), partitionMoment φ a ↑π = partitionMoment φ b ↑(e π)) (π : NoncrossingPartition s) : partitionCumulant φ a π = partitionCumulant φ b (e π)

Free cumulants transport along an order isomorphism e : NC(s) ≃o NC(t) that matches the block moments of two words: if φ_π(a) = φ_{e π}(b) for every π, then κ_π(a) = κ_{e π}(b).

theorem TauCeti.freeCumulant_eq_of_orderIso {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) {β : Type u_4} [LinearOrder β] {t : Finset β} {a : α → A} {b : β → A} (e : NoncrossingPartition s ≃o NoncrossingPartition t) (h : ∀ (π : NoncrossingPartition s), partitionMoment φ a ↑π = partitionMoment φ b ↑(e π)) : freeCumulant φ a s = freeCumulant φ b t

Free cumulants of two words agree when an order isomorphism NC(s) ≃o NC(t) matches their block moments.