Free cumulants with products as arguments

Let φ : A → R be a function on a monoid, a : α → A a word indexed by a finite set s of positions in a linear order, and f : α → β a map to a linear order that is monotone on s. The fibres of f cut s into consecutive intervals; multiplying the letters of a along each fibre, in increasing order, gives the grouped word fiberProd a s f, indexed by the image f '' s. Let σ_f ∈ NC(s) be the partition of s into the fibres of f.

The free cumulants of the grouped word are sums of free cumulants of the original word: for every noncrossing partition ρ of f '' s, κ_ρ(fiberProd a s f) = ∑_{π ∈ NC(s), π ⊔ σ_f = ρ̂} κ_π(a), where ρ̂ is the pullback of ρ along f and the join is taken in NC(s). For ρ the partition into one part this is the formula κ_m(A₁, …, A_m) = ∑_{π ∈ NC(n), π ⊔ σ = 1_n} κ_π(a₁, …, aₙ) for cumulants whose arguments A_j are products of consecutive letters, the key step towards the characterisation of freeness by the vanishing of mixed cumulants.

The proof identifies the block moments of ρ̂ with those of ρ, so that both sides satisfy the moment–cumulant formula on NC(f '' s), and then uses that pulling back is an order isomorphism of NC(f '' s) onto the upper interval [σ_f, 1_s] of NC(s).

Main definitions

• TauCeti.fiberProd a s f — the word indexed by f '' s whose letter at y is the product, in increasing order, of the letters of a at the positions of s over y.

Main results

• TauCeti.partitionMoment_comap — the block moment of the pullback of a partition P of f '' s is the block moment of P for the grouped word.
• TauCeti.partitionCumulant_fiberProd — κ_ρ(fiberProd a s f) = ∑_{π ⊔ σ_f = ρ̂} κ_π(a).
• TauCeti.freeCumulant_fiberProd and TauCeti.freeCumulant_fiberProd_eq_sum_prod — the free cumulant of the grouped word is ∑_{π ⊔ σ_f = 1_s} κ_π(a), and in multiplicative form ∑_{π ⊔ σ_f = 1_s} ∏_{B ∈ π} κ_B(a).
• TauCeti.freeCumulant_comp_of_strictMonoOn — for injective f no letters are grouped, so free cumulants are invariant under increasing relabelling of the positions; in particular TauCeti.freeCumulant_eq_freeCumulant_comp_orderEmbOfFin — every free cumulant is a cumulant κ_n of a word indexed by Fin n.

References

• A. Nica, R. Speicher, Lectures on the Combinatorics of Free Probability, Theorem 11.12.
• M. Krawczyk, R. Speicher, Combinatorics of free cumulants, J. Combin. Theory Ser. A 90 (2000), 267–292.

def TauCeti.fiberProd {A : Type u_2} {α : Type u_3} {β : Type u_4} [LinearOrder α] [Monoid A] [DecidableEq β] (a : α → A) (s : Finset α) (f : α → β) (y : β) : A

The word obtained from a by grouping along the fibres of f: its letter at y is the product a_{x₁} * ⋯ * a_{xₖ} over the positions x₁ < ⋯ < xₖ of s with f xᵢ = y. When β is linearly ordered and f is monotone on s these positions are consecutive in s.

theorem TauCeti.fiberProd_def {A : Type u_2} {α : Type u_3} {β : Type u_4} [LinearOrder α] [Monoid A] [DecidableEq β] (a : α → A) (s : Finset α) (f : α → β) (y : β) : fiberProd a s f y = (List.map a ({x ∈ s | f x = y}.sort fun (a b : α) => a ≤ b)).prod

Unfolding of the word grouped along the fibres of f.

theorem TauCeti.partitionMoment_comap {R : Type u_1} {A : Type u_2} {α : Type u_3} {β : Type u_4} [LinearOrder α] {s : Finset α} {f : α → β} [LinearOrder β] [Monoid A] [CommMonoid R] (φ : A → R) (a : α → A) (hf : MonotoneOn f ↑s) (P : Finpartition (Finset.image f s)) : partitionMoment φ a (Finpartition.comap f P) = partitionMoment φ (fiberProd a s f) P

The block moment of the pullback along f of a partition P of f '' s is the block moment of P for the word grouped along the fibres of f.

theorem TauCeti.partitionCumulant_fiberProd {R : Type u_1} {A : Type u_2} {α : Type u_3} {β : Type u_4} [LinearOrder α] {s : Finset α} {f : α → β} [LinearOrder β] [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (hf : MonotoneOn f ↑s) (ρ : NoncrossingPartition (Finset.image f s)) : partitionCumulant φ (fiberProd a s f) ρ = ∑ π : NoncrossingPartition s with π ⊔ (NoncrossingPartition.comap hf) ⊥ = (NoncrossingPartition.comap hf) ρ, partitionCumulant φ a π

Free cumulants with products as arguments: the free cumulant of a noncrossing partition ρ of f '' s for the word grouped along the fibres of f is the sum of the free cumulants of the noncrossing partitions π of s whose join with the partition σ_f of s into the fibres of f is the pullback of ρ.

theorem TauCeti.freeCumulant_fiberProd {R : Type u_1} {A : Type u_2} {α : Type u_3} {β : Type u_4} [LinearOrder α] {s : Finset α} {f : α → β} [LinearOrder β] [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (hf : MonotoneOn f ↑s) : freeCumulant φ (fiberProd a s f) (Finset.image f s) = ∑ π : NoncrossingPartition s with π ⊔ (NoncrossingPartition.comap hf) ⊥ = ⊤, partitionCumulant φ a π

Free cumulants with products as arguments: the free cumulant of the word grouped along the fibres of f is the sum of the free cumulants of the noncrossing partitions π of s whose join with the partition σ_f of s into the fibres of f is the partition into one part, κ(fiberProd a s f) = ∑_{π ⊔ σ_f = 1_s} κ_π(a).

theorem TauCeti.freeCumulant_fiberProd_eq_sum_prod {R : Type u_1} {A : Type u_2} {α : Type u_3} {β : Type u_4} [LinearOrder α] {s : Finset α} {f : α → β} [LinearOrder β] [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (hf : MonotoneOn f ↑s) : freeCumulant φ (fiberProd a s f) (Finset.image f s) = ∑ π : NoncrossingPartition s with π ⊔ (NoncrossingPartition.comap hf) ⊥ = ⊤, ∏ B ∈ (↑π).parts, freeCumulant φ a B

Free cumulants with products as arguments, in multiplicative form: κ(fiberProd a s f) = ∑_{π ⊔ σ_f = 1_s} ∏_{B ∈ π} κ_B(a), where σ_f is the partition of s into the fibres of f.

theorem TauCeti.freeCumulant_comp_of_strictMonoOn {R : Type u_1} {A : Type u_2} {α : Type u_3} {β : Type u_4} [LinearOrder α] {s : Finset α} [LinearOrder β] [CommRing R] [Monoid A] (φ : A → R) {e : α → β} (he : StrictMonoOn e ↑s) (b : β → A) : freeCumulant φ (b ∘ e) s = freeCumulant φ b (Finset.image e s)

Increasing relabelling: for a map e that is strictly monotone on s, the free cumulant of the word b ∘ e along s is the free cumulant of b along the image e '' s.

theorem TauCeti.freeCumulant_eq_freeCumulant_comp_orderEmbOfFin {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α] [CommRing R] [Monoid A] (φ : A → R) (b : α → A) (s : Finset α) : freeCumulant φ b s = freeCumulant φ (b ∘ ⇑(s.orderEmbOfFin ⋯)) Finset.univ

Relabelling the positions of s increasingly by Fin #s: the free cumulant of b along s is the cumulant κ_n of the word b ∘ s.orderEmbOfFin, which lists the letters of b at the positions of s in increasing order.