The law of a selfadjoint element in a C⋆-probability space

Let A be a unital C⋆-algebra, φ : A →ₚ[ℂ] ℂ a positive linear functional and a ∈ A selfadjoint. The functional f ↦ φ (f(a)) on real continuous functions on spectrum ℝ a is positive, because the continuous functional calculus sends nonnegative functions to positive elements. By the Riesz–Markov–Kakutani theorem it is integration against a unique finite Borel measure. Pushed forward to ℝ, this is the law (or distribution) μ_a of a:

φ (f(a)) = ∫ f dμ_a for every f continuous on spectrum ℝ a.

It is concentrated on the compact set spectrum ℝ a, has total mass φ 1, so it is a probability measure when φ is a state, and its moments are the moments φ (a ^ n) of a. The law turns statements about a single selfadjoint noncommutative random variable into statements about a compactly supported measure on the line, which is how free convolutions and free limit theorems are formulated analytically.

Conversely, the law is determined by the moments: a compactly supported finite measure whose moments are the φ (a ^ n) is μ_a, so two selfadjoint elements, possibly in different C⋆-algebras, have the same law exactly when they have the same moments. And every compactly supported finite measure μ on ℝ is a law, realized in a commutative C⋆-algebra: if μ is concentrated on the compact set K, it is the law of the coordinate x ↦ x in C(K, ℂ) with respect to integration against μ on K, which is a state when μ is a probability measure. So the laws of selfadjoint elements with respect to states are exactly the compactly supported probability measures on ℝ.

Main declarations

• PositiveLinearMap.law φ a: the law of a with respect to φ, a finite measure on ℝ; it is the zero measure when a is not selfadjoint.
• PositiveLinearMap.ofReal_integral_law: ∫ f dμ_a = φ (cfc f a).
• PositiveLinearMap.eq_law_iff: μ_a is the only finite measure on ℝ with this property for continuous f.
• PositiveLinearMap.law_compl_spectrum: μ_a is concentrated on spectrum ℝ a.
• PositiveLinearMap.integrable_law: every f continuous on spectrum ℝ a is μ_a-integrable.
• PositiveLinearMap.isProbabilityMeasure_law: μ_a is a probability measure when φ 1 = 1.
• PositiveLinearMap.ofReal_integral_pow_law: the moments of μ_a are φ (a ^ n).
• PositiveLinearMap.law_cfc, PositiveLinearMap.law_aeval, PositiveLinearMap.law_smul_add_algebraMap: the law of g(a), of p(a) for a real polynomial p, and of r • a + c is the pushforward of μ_a along g, p and x ↦ r x + c.
• PositiveLinearMap.eq_law_iff_forall_integral_pow: a compactly supported finite measure is μ_a exactly when its moments are the φ (a ^ n).
• PositiveLinearMap.law_eq_law_iff_forall_apply_pow: two selfadjoint elements have the same law exactly when they have the same moments.
• PositiveLinearMap.law_integralPositiveLinearMap_realToRCLike: in C(X, ℂ) for a compact space X, the law of a real function g with respect to integration against ν is the pushforward of ν along g.
• PositiveLinearMap.law_integralPositiveLinearMap_comap_restrict_id: every finite measure on ℝ concentrated on a compact set K is the law of the coordinate x ↦ x in C(K, ℂ).

Implementation notes

The construction follows ContinuousLinearMap.diagMeasure in TauCeti/Analysis/InnerProductSpace/BorelCalculus/DiagonalMeasure.lean, which applies the same Riesz–Markov–Kakutani step to a vector state of a normal operator on a Hilbert space.

Moment determinacy is TauCeti.Measure.ext_of_forall_integral_pow_eq_of_support, the Stone–Weierstrass argument on a compact set containing both supports. The realization in C(X, ℂ) is identified with the pushforward through its moments rather than through the continuous functional calculus, so it uses only powers of the element.

References

• A. Nica, R. Speicher, Lectures on the Combinatorics of Free Probability, London Math. Soc. Lecture Note Ser. 335, Cambridge University Press (2006), Lecture 3.
• D. V. Voiculescu, K. J. Dykema, A. Nica, Free Random Variables, CRM Monograph Ser. 1, Amer. Math. Soc. (1992), §1.1.

noncomputable def PositiveLinearMap.law {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) (a : A) : MeasureTheory.Measure ℝ

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).

@[simp]

theorem PositiveLinearMap.law_of_not_isSelfAdjoint {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) {a : A} (ha : ¬IsSelfAdjoint a) : φ.law a = 0

The law of an element that is not selfadjoint is, by convention, the zero measure.

instance PositiveLinearMap.instIsFiniteMeasureRealLaw {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) (a : A) : MeasureTheory.IsFiniteMeasure (φ.law a)

The law of any element is a finite measure.

@[simp]

theorem PositiveLinearMap.law_compl_spectrum {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) (a : A) : (φ.law a) (spectrum ℝ a)ᶜ = 0

The law μ_a is concentrated on the spectrum of a.

@[simp]

theorem PositiveLinearMap.restrict_spectrum_law {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) (a : A) : (φ.law a).restrict (spectrum ℝ a) = φ.law a

The law μ_a is concentrated on the spectrum of a, as a restriction.

theorem PositiveLinearMap.integrable_law {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) (a : A) (f : ℝ → ℝ) (hf : ContinuousOn f (spectrum ℝ a) := by cfc_cont_tac) : MeasureTheory.Integrable f (φ.law a)

Every function continuous on the spectrum of a is integrable against the law μ_a.

theorem PositiveLinearMap.integrable_eval_law {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) (a : A) (p : Polynomial ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Polynomial.eval x p) (φ.law a)

Every real polynomial is integrable against the law μ_a.

theorem PositiveLinearMap.integrable_pow_law {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) (a : A) (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ n) (φ.law a)

Every power x ^ n is integrable against the law μ_a.

theorem PositiveLinearMap.ofReal_integral_law {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) {a : A} (f : ℝ → ℝ) (hf : ContinuousOn f (spectrum ℝ a) := by cfc_cont_tac) : ↑(∫ (x : ℝ), f x ∂φ.law a) = φ (cfc f a)

Integration against the law μ_a of an element a computes φ on the continuous functional calculus: ∫ f dμ_a = φ (f(a)) for f continuous on the spectrum of a. For a not selfadjoint both sides vanish.

theorem PositiveLinearMap.eq_law_iff {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {φ : A →ₚ[ℂ] ℂ} {a : A} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] : μ = φ.law a ↔ ∀ (f : ℝ → ℝ), Continuous f → ↑(∫ (x : ℝ), f x ∂μ) = φ (cfc f a)

The law μ_a of an element a is the unique finite measure on ℝ that represents f ↦ φ (f(a)) on continuous functions.

theorem PositiveLinearMap.ofReal_law_real_univ {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) {a : A} (ha : IsSelfAdjoint a) : ↑((φ.law a).real Set.univ) = φ 1

The total mass of the law of a selfadjoint element is φ 1.

theorem PositiveLinearMap.isProbabilityMeasure_law {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) {a : A} (hφ : φ 1 = 1) (ha : IsSelfAdjoint a) : MeasureTheory.IsProbabilityMeasure (φ.law a)

The law of a selfadjoint element with respect to a state is a probability measure.

theorem PositiveLinearMap.ofReal_integral_eval_law {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) {a : A} (ha : IsSelfAdjoint a) (p : Polynomial ℝ) : ↑(∫ (x : ℝ), Polynomial.eval x p ∂φ.law a) = φ ((Polynomial.aeval a) p)

The polynomial moments of the law of a selfadjoint element a are the corresponding values of φ: ∫ p dμ_a = φ (p(a)).

theorem PositiveLinearMap.ofReal_integral_pow_law {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) {a : A} (ha : IsSelfAdjoint a) (n : ℕ) : ↑(∫ (x : ℝ), x ^ n ∂φ.law a) = φ (a ^ n)

The moments of the law of a selfadjoint element a are the moments of a: ∫ x ^ n dμ_a = φ (a ^ n).

theorem PositiveLinearMap.law_cfc {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) {a : A} (ha : IsSelfAdjoint a) (g : ℝ → ℝ) (hg : ContinuousOn g (spectrum ℝ a) := by cfc_cont_tac) : φ.law (cfc g a) = MeasureTheory.Measure.map g (φ.law a)

The law of g(a), for a selfadjoint and g continuous on its spectrum, is the pushforward of the law of a along g.

theorem PositiveLinearMap.law_aeval {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) {a : A} (ha : IsSelfAdjoint a) (p : Polynomial ℝ) : φ.law ((Polynomial.aeval a) p) = MeasureTheory.Measure.map (fun (x : ℝ) => Polynomial.eval x p) (φ.law a)

The law of p(a), for a selfadjoint and p a real polynomial, is the pushforward of the law of a along p.

theorem PositiveLinearMap.law_smul_add_algebraMap {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (φ : A →ₚ[ℂ] ℂ) {a : A} (ha : IsSelfAdjoint a) (r c : ℝ) : φ.law (r • a + (algebraMap ℝ A) c) = MeasureTheory.Measure.map (fun (x : ℝ) => r * x + c) (φ.law a)

The law of the affine image r • a + c of a selfadjoint element a is the pushforward of the law of a along x ↦ r * x + c.

Moment determinacy

theorem PositiveLinearMap.eq_law_iff_forall_integral_pow {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {φ : A →ₚ[ℂ] ℂ} {a : A} (ha : IsSelfAdjoint a) {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] {K : Set ℝ} (hK : IsCompact K) (hμ : μ Kᶜ = 0) : μ = φ.law a ↔ ∀ (n : ℕ), ↑(∫ (x : ℝ), x ^ n ∂μ) = φ (a ^ n)

Moment determinacy of the law. A finite measure on ℝ concentrated on a compact set is the law μ_a of a selfadjoint element a exactly when its moments are the moments of a: ∫ x ^ n dμ = φ (a ^ n) for every n.

The support hypothesis cannot be dropped: the moments are Bochner integrals, which are 0 for non-integrable integrands, so a heavy-tailed μ can match the moments of a without being μ_a.

theorem PositiveLinearMap.law_eq_law_iff_forall_apply_pow {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)

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).

Realization of compactly supported measures

theorem PositiveLinearMap.law_integralPositiveLinearMap_realToRCLike {X : Type u_2} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (ν : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure ν] (g : C(X, ℝ)) : (ContinuousMap.integralPositiveLinearMap ν).law (ContinuousMap.realToRCLike ℂ g) = MeasureTheory.Measure.map (⇑g) ν

In the commutative C⋆-algebra C(X, ℂ) of a compact space X, the law of a real continuous function g with respect to integration against a finite measure ν is the pushforward ν ∘ g⁻¹ of ν along g.

theorem 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 ℝ))) = μ

Realization 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).