Free probability, free products, and random matrix models
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremTauCeti.apply_prod_ofFn_eq_sum_prod_freeCumulant#
The moment–cumulant formula for a word a₁, …, aₙ with n ≥ 1 in multiplicative form:
φ (a₁ * ⋯ * aₙ) = ∑_{π ∈ NC(n)} ∏_{B ∈ π} κ_B(a₁, …, aₙ).
TauCeti.apply_prod_ofFn_eq_sum_prod_freeCumulant.{u_1, u_2} {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 = ∑ π, ∏ B ∈ (↑π).parts, TauCeti.freeCumulant φ a B
Lean
Formalized in Tau Ceti as TauCeti.apply_prod_ofFn_eq_sum_prod_freeCumulant.
Sources
Uses 2 · Used by 1
TheoremTauCeti.freeCumulant_eq_sum_mu_mul_partitionMoment#
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).
TauCeti.freeCumulant_eq_sum_mu_mul_partitionMoment.{u_1, u_2, u_3} {R : Type u_1} {A : Type u_2}
{α : Type u_3} [LinearOrder α] [CommRing R] [Monoid A] (φ : A → R) (a : α → A) (s : Finset α) :
TauCeti.freeCumulant φ a s = ∑ π, (IncidenceAlgebra.mu R) π ⊤ * TauCeti.partitionMoment φ a ↑π
Lean
Formalized in Tau Ceti as TauCeti.freeCumulant_eq_sum_mu_mul_partitionMoment.
Sources
Uses 1 · Used by 1
TheoremTauCeti.freeCumulant_fiberProd_eq_sum_prod#
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.
TauCeti.freeCumulant_fiberProd_eq_sum_prod.{u_1, u_2, u_3, u_4} {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) :
TauCeti.freeCumulant φ (TauCeti.fiberProd a s f) (Finset.image f s) =
∑ π with π ⊔ (TauCeti.NoncrossingPartition.comap hf) ⊥ = ⊤,
∏ B ∈ (↑π).parts, TauCeti.freeCumulant φ a B
Uses 2 · Used by 1
TheoremTauCeti.NoncrossingPartition.card_fin_eq_catalan#
There are catalan n noncrossing partitions of the n ordered positions of Fin n.
TauCeti.NoncrossingPartition.card_fin_eq_catalan (n : ℕ) :
Fintype.card (TauCeti.NoncrossingPartition Finset.univ) = catalan n
Lean
Formalized in Tau Ceti as TauCeti.NoncrossingPartition.card_fin_eq_catalan.
Sources
TheoremTauCeti.NoncrossingPartition.card_isPairing_fin_eq_catalan#
There are catalan n noncrossing pairings of the 2 * n ordered positions of Fin (2 * n).
TauCeti.NoncrossingPartition.card_isPairing_fin_eq_catalan (n : ℕ) :
Fintype.card { P // (↑P).IsPairing } = catalan n
Lean
Formalized in Tau Ceti as TauCeti.NoncrossingPartition.card_isPairing_fin_eq_catalan.
Sources
Used by 1
TheoremPositiveLinearMap.law_eq_law_iff_forall_apply_pow#
Two selfadjoint elements, possibly in different C⋆-algebras and with respect to different
positive functionals, have the same law exactly when they have the same moments:
μ_a = μ_b ↔ ∀ n, φ (a ^ n) = ψ (b ^ n).
PositiveLinearMap.law_eq_law_iff_forall_apply_pow.{u_1, u_2} {A : Type u_1} [CStarAlgebra A]
[PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) {a : A} {B : Type u_2} [CStarAlgebra B]
[PartialOrder B] [StarOrderedRing B] (ψ : B →ₚ[ℂ] ℂ) {b : B} (ha : IsSelfAdjoint a)
(hb : IsSelfAdjoint b) : φ.law a = ψ.law b ↔ ∀ (n : ℕ), φ (a ^ n) = ψ (b ^ n)
Lean
Formalized in Tau Ceti as PositiveLinearMap.law_eq_law_iff_forall_apply_pow.
Sources
Uses 1
TheoremRealization of compactly supported laws#
A finite measure μ on ℝ concentrated on a
compact set K is the law of the coordinate function x ↦ x in the commutative C⋆-algebra
C(K, ℂ), with respect to integration against μ on K. This functional is a state when μ is
a probability measure (ContinuousMap.integralPositiveLinearMap_one).
PositiveLinearMap.law_integralPositiveLinearMap_comap_restrict_id {K : Set ℝ} [CompactSpace ↑K]
{μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ Kᶜ = 0) :
(ContinuousMap.integralPositiveLinearMap (MeasureTheory.Measure.comap Subtype.val μ)).law
(ContinuousMap.realToRCLike ℂ (ContinuousMap.restrict K (ContinuousMap.id ℝ))) =
μ
Lean
Formalized in Tau Ceti as PositiveLinearMap.law_integralPositiveLinearMap_comap_restrict_id.
Sources
- Tau Ceti documentation:
PositiveLinearMap.law_integralPositiveLinearMap_comap_restrict_id - Source of
PositiveLinearMap.law_integralPositiveLinearMap_comap_restrict_idin TauCeti/Probability/FreeProbability/Law/Basic.lean - Tau Ceti roadmap status: Free probability, free products, and random matrix models
Uses 1
TheoremTauCeti.IsFreelyIndependent.eqOn_iSup#
Freeness determines the joint distribution from the individual ones: two normalised
functionals for which B is free and which agree on each B i agree on the subalgebra
generated by the B i.
TauCeti.IsFreelyIndependent.eqOn_iSup.{u_1, u_2, u_4} {R : Type u_1} {A : Type u_2} {ι : Type u_4}
[CommRing R] [Ring A] [Algebra R A] {φ ψ : A →ₗ[R] R} {B : ι → Subalgebra R A} (hφ : φ 1 = 1)
(hψ : ψ 1 = 1) (hfφ : TauCeti.IsFreelyIndependent φ B) (hfψ : TauCeti.IsFreelyIndependent ψ B)
(h : ∀ (i : ι), Set.EqOn ⇑φ ⇑ψ ↑(B i)) : Set.EqOn ⇑φ ⇑ψ ↑(⨆ i, B i)
Uses 1
DefinitionTauCeti.freeCumulant#
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.
TauCeti.freeCumulant.{u_1, u_2, u_3} {R : Type u_1} {A : Type u_2} {α : Type u_3} [LinearOrder α]
[CommRing R] [Monoid A] (φ : A → R) (a : α → A) (s : Finset α) : R
TheoremTauCeti.partitionCumulant_eq_prod_freeCumulant#
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).
TauCeti.partitionCumulant_eq_prod_freeCumulant.{u_1, u_2, u_3} {R : Type u_1} {A : Type u_2}
{α : Type u_3} [LinearOrder α] {s : Finset α} [CommRing R] [Monoid A] (φ : A → R) (a : α → A)
(π : TauCeti.NoncrossingPartition s) :
TauCeti.partitionCumulant φ a π = ∏ B ∈ (↑π).parts, TauCeti.freeCumulant φ a B
Uses 2 · Used by 3
DefinitionTauCeti.NoncrossingPartition.iicOrderIso#
The lower interval [0_s, π] of the lattice of noncrossing partitions of s is isomorphic
to the product of the lattices of noncrossing partitions of the parts of π: a noncrossing
partition σ ≤ π corresponds to its restrictions to the parts of π, and a family of noncrossing
partitions of the parts corresponds to their juxtaposition.
TauCeti.NoncrossingPartition.iicOrderIso.{u_1} {α : Type u_1} [LinearOrder α] {s : Finset α}
(π : TauCeti.NoncrossingPartition s) :
↑(Set.Iic π) ≃o ((B : ↥(↑π).parts) → TauCeti.NoncrossingPartition ↑B)
Used by 1
DefinitionPositiveLinearMap.law#
The law μ_a of an element a of a C⋆-algebra with respect to a positive linear
functional φ: for selfadjoint a, the finite Borel measure on ℝ, concentrated on
spectrum ℝ a (law_compl_spectrum), with ∫ f dμ_a = φ (cfc f a) for every f continuous on
the spectrum (ofReal_integral_law), and characterized by this property (eq_law_iff). For a
not selfadjoint it is the zero measure (law_of_not_isSelfAdjoint).
PositiveLinearMap.law.{u_1} {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
(φ : A →ₚ[ℂ] ℂ) (a : A) : MeasureTheory.Measure ℝ
DefinitionTauCeti.IsFreelyIndependent#
Subalgebras B i of A are freely independent with respect to a linear functional φ if
φ (a₁ * ⋯ * aₙ) = 0 for every nonempty word [(i₁, a₁), …, (iₙ, aₙ)] whose consecutive labels
are distinct and whose letters satisfy aⱼ ∈ B iⱼ and φ aⱼ = 0. Labels that are not adjacent
may coincide.
TauCeti.IsFreelyIndependent.{u_1, u_2, u_4} {R : Type u_1} {A : Type u_2} {ι : Type u_4}
[CommSemiring R] [Semiring A] [Algebra R A] (φ : A →ₗ[R] R) (B : ι → Subalgebra R A) : Prop
Used by 2
TheoremThe weak free central limit theorem#
Centered free selfadjoint elements whose moments
are uniformly bounded in each degree and whose average variance tends to v ≥ 0 have
normalized-sum laws converging weakly to semicircleReal 0 v. No common compact support of the
approximating laws is required.
TauCeti.IsFreelyIndependentElements.tendsto_law_inv_sqrt_smul_sum_semicircleReal.{u_1}
{A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {φ : A →ₚ[ℂ] ℂ} {a : ℕ → A}
(h : TauCeti.IsFreelyIndependentElements φ.toLinearMap a) (hφ : φ 1 = 1)
(ha : ∀ (j : ℕ), IsSelfAdjoint (a j)) (hcen : ∀ (j : ℕ), φ (a j) = 0)
(hbdd : ∀ (k : ℕ), ∃ M, ∀ (j : ℕ), ‖φ (a j ^ k)‖ ≤ M) {v : NNReal}
(hvar :
Filter.Tendsto (fun N => (↑N)⁻¹ * ∑ j ∈ Finset.range N, φ (a j ^ 2)) Filter.atTop (nhds ↑↑v)) :
Filter.Tendsto (fun N => ⟨φ.law ((√↑N)⁻¹ • ∑ j ∈ Finset.range N, a j), ⋯⟩) Filter.atTop
(nhds (TauCeti.Probability.semicircleReal 0 v).toProbabilityMeasure)
Lean
Formalized in Tau Ceti as TauCeti.IsFreelyIndependentElements.tendsto_law_inv_sqrt_smul_sum_semicircleReal.
Other forms
The weak free central limit theorem for identically distributed elements. Formalized in Tau Ceti as TauCeti.IsFreelyIndependentElements.tendsto_law_inv_sqrt_smul_sum_of_apply_pow_eq.
TauCeti.IsFreelyIndependentElements.tendsto_law_inv_sqrt_smul_sum_of_apply_pow_eq.{u_1}
{A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {φ : A →ₚ[ℂ] ℂ} {a : ℕ → A}
(h : TauCeti.IsFreelyIndependentElements φ.toLinearMap a) (hφ : φ 1 = 1)
(ha : ∀ (j : ℕ), IsSelfAdjoint (a j)) (hid : ∀ (j k : ℕ), φ (a j ^ k) = φ (a 0 ^ k))
(hcen : φ (a 0) = 0) {v : NNReal} (hv : φ (a 0 ^ 2) = ↑↑v) :
Filter.Tendsto (fun N => ⟨φ.law ((√↑N)⁻¹ • ∑ j ∈ Finset.range N, a j), ⋯⟩) Filter.atTop
(nhds (TauCeti.Probability.semicircleReal 0 v).toProbabilityMeasure)
Sources
Uses 8
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.