The carrier of symmetric-matrix distributions

The Wishart and related symmetric-matrix distributions live on Mathlib's self-adjoint subspace selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ). Over ℝ, star is transpose, so this is exactly the subspace of symmetric matrices, and Matrix.isHermitian_iff_isSelfAdjoint connects membership to the spectral API.

This file equips that subspace with the ambient Frobenius norm and inner product while keeping the subtype topology and uniformity it already carries: the norm structure is induced from Matrix.frobeniusNormedAddCommGroup, whose topology and uniformity are definitionally the product ones, so the induced structures agree definitionally with the subtype instances. The measurable structure is the Borel structure of the subtype topology, and volume is supplied by measureSpaceOfInnerProductSpace.

It also fixes the upper-triangular coordinate system used to normalize Lebesgue measure on the subspace: TauCeti.symmetricCoordinates reads off the entries above the diagonal.

Main declarations

• TauCeti.upperTriangle — the index type of upper-triangular positions.
• TauCeti.card_upperTriangle — there are p * (p + 1) / 2 such positions.
• TauCeti.symmetricMatrixNormedAddCommGroup, TauCeti.symmetricMatrixInnerProductSpace — the Frobenius structure on the symmetric subspace.
• selfAdjoint.coe_inner — the subspace inner product is the ambient one on the coercions.
• TauCeti.symmetricCoordinates — the continuous linear equivalence with upperTriangle p → ℝ.
• TauCeti.symmetricCoordinatesMeasurableEquiv — its measurable-equivalence form.
• TauCeti.symmetricBasis — the basis dual to the upper-triangular coordinates.
• TauCeti.symmetricFinOneEquiv — the identification of 1 × 1 symmetric matrices with ℝ.
• TauCeti.finrank_symmetricMatrix — the dimension is p * (p + 1) / 2.
• selfAdjoint.inner_eq_trace_mul — the Frobenius pairing is the trace pairing, and selfAdjoint.continuous_trace_mul_coe — that pairing is continuous in its second argument, as is its exponential selfAdjoint.continuous_exp_trace_mul_coe.
• TauCeti.symmetricEntry — the symmetric matrix representing evaluation at an entry under the trace pairing, with TauCeti.trace_symmetricEntry_mul and TauCeti.trace_symmetricEntry_mul_mul_symmetricEntry_mul.

@[reducible, inline]

abbrev TauCeti.upperTriangle (p : ℕ) : Type

The index type for the on-or-above-diagonal positions of a p × p matrix. A symmetric matrix is determined by these entries, and TauCeti.symmetricCoordinates reads them off.

Equations

• TauCeti.upperTriangle p = { ij : Fin p × Fin p // ij.1 ≤ ij.2 }

theorem TauCeti.card_upperTriangle (p : ℕ) : Fintype.card (upperTriangle p) = p * (p + 1) / 2

There are p * (p + 1) / 2 on-or-above-diagonal positions in a p × p matrix.

The Frobenius structure on the symmetric subspace

The instances below install the Frobenius norm and inner product on the symmetric subspace: the norm is induced from the ambient (scoped) Frobenius instances, and the inner product pairs the underlying matrices. Because the Frobenius norm is definitionally compatible with the product topology and uniformity of Matrix, the induced structures agree definitionally with the subtype instances already present.

@[instance_reducible]

noncomputable instance TauCeti.symmetricMatrixNormedAddCommGroup (p : ℕ) : NormedAddCommGroup ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

The symmetric subspace carries the Frobenius norm induced from the ambient matrices, with its metric rebuilt on the subtype uniformity so that the uniform and topological structures are the subtype ones on the nose.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance TauCeti.symmetricMatrixInnerProductSpace (p : ℕ) : InnerProductSpace ℝ ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

The symmetric subspace carries the Frobenius inner product ⟪A, B⟫ = ∑ i, ∑ j, A i j * B i j of the underlying matrices, which on this subspace is the trace pairing selfAdjoint.inner_eq_trace_mul.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.symmetricMatrixIsUniformAddGroup (p : ℕ) : IsUniformAddGroup ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

instance TauCeti.symmetricMatrixSecondCountableTopology (p : ℕ) : SecondCountableTopology ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

instance TauCeti.symmetricMatrixCompleteSpace (p : ℕ) : CompleteSpace ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

@[instance_reducible]

noncomputable instance TauCeti.symmetricMatrixContinuousENorm (p : ℕ) : ContinuousENorm ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

Equations

• TauCeti.symmetricMatrixContinuousENorm p = SeminormedAddGroup.toContinuousENorm

instance TauCeti.symmetricMatrixBorelSpace (p : ℕ) : BorelSpace ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

The measurable structure is the Borel structure of the subtype topology. Declared explicitly so that instance search finds it regardless of which (definitionally equal) route it takes to the topology.

The inner product of the symmetric subspace

@[simp]

theorem selfAdjoint.coe_inner {p : ℕ} (A B : ↥(submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : inner ℝ A B = inner ℝ ↑A ↑B

The inner product of the symmetric subspace is the Frobenius inner product of the underlying matrices.

Symmetry of the entries

theorem selfAdjoint.isHermitian_coe {p : ℕ} (A : ↥(submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : (↑A).IsHermitian

An element of the symmetric subspace is a Hermitian matrix; over ℝ this says that it is symmetric, as spelled out by selfAdjoint.coe_apply_comm.

theorem selfAdjoint.coe_apply_comm {p : ℕ} (A : ↥(submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) (i j : Fin p) : ↑A i j = ↑A j i

The entries of a symmetric matrix are unchanged by swapping the two indices.

@[simp]

theorem selfAdjoint.transpose_coe {p : ℕ} (A : ↥(submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : (↑A).transpose = ↑A

An element of the symmetric subspace is fixed by transposition.

Upper-triangular coordinates

noncomputable def TauCeti.symmetricCoordinates (p : ℕ) : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) ≃L[ℝ] upperTriangle p → ℝ

The continuous linear equivalence reading off the on-or-above-diagonal entries of a symmetric matrix. Its inverse reconstructs the matrix by reflecting them across the diagonal.

This coordinate system fixes the normalization of TauCeti.symmetricLebesgue.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.symmetricCoordinates_apply (p : ℕ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) (ij : upperTriangle p) : (symmetricCoordinates p) A ij = ↑A (↑ij).1 (↑ij).2

@[simp]

theorem TauCeti.coe_symmetricCoordinates_symm_apply_of_le (p : ℕ) (x : upperTriangle p → ℝ) {i j : Fin p} (h : i ≤ j) : ↑((symmetricCoordinates p).symm x) i j = x ⟨(i, j), h⟩

@[simp]

theorem TauCeti.coe_symmetricCoordinates_symm_apply_of_ge (p : ℕ) (x : upperTriangle p → ℝ) {i j : Fin p} (h : j ≤ i) : ↑((symmetricCoordinates p).symm x) i j = x ⟨(j, i), h⟩

noncomputable def TauCeti.symmetricCoordinatesMeasurableEquiv (p : ℕ) : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) ≃ᵐ (upperTriangle p → ℝ)

The measurable equivalence induced by TauCeti.symmetricCoordinates.

Equations

• TauCeti.symmetricCoordinatesMeasurableEquiv p = (TauCeti.symmetricCoordinates p).toHomeomorph.toMeasurableEquiv

@[simp]

theorem TauCeti.symmetricCoordinatesMeasurableEquiv_coe (p : ℕ) : ⇑(symmetricCoordinatesMeasurableEquiv p) = ⇑(symmetricCoordinates p)

@[simp]

theorem TauCeti.symmetricCoordinatesMeasurableEquiv_symm_coe (p : ℕ) : ⇑(symmetricCoordinatesMeasurableEquiv p).symm = ⇑(symmetricCoordinates p).symm

theorem TauCeti.finrank_symmetricMatrix (p : ℕ) : Module.finrank ℝ ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) = p * (p + 1) / 2

The symmetric subspace has dimension p * (p + 1) / 2.

noncomputable def TauCeti.symmetricBasis (p : ℕ) : Module.Basis (upperTriangle p) ℝ ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

The basis of the symmetric subspace dual to the upper-triangular coordinates: its vector at an on-or-above-diagonal position is the symmetric matrix carrying a one at that position and at its mirror image, and nothing else.

Equations

• TauCeti.symmetricBasis p = (Pi.basisFun ℝ (TauCeti.upperTriangle p)).map ↑(TauCeti.symmetricCoordinates p).symm

theorem TauCeti.symmetricBasis_apply (p : ℕ) (ij : upperTriangle p) : (symmetricBasis p) ij = (symmetricCoordinates p).symm (Pi.single ij 1)

@[simp]

theorem TauCeti.symmetricBasis_repr (p : ℕ) (x : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) (ij : upperTriangle p) : ((symmetricBasis p).repr x) ij = ↑x (↑ij).1 (↑ij).2

The coordinates of a symmetric matrix in TauCeti.symmetricBasis are its on-or-above-diagonal entries.

theorem TauCeti.coe_symmetricBasis_apply_of_le (p : ℕ) (ij : upperTriangle p) {k l : Fin p} (h : k ≤ l) : ↑((symmetricBasis p) ij) k l = if ij = ⟨(k, l), h⟩ then 1 else 0

theorem TauCeti.coe_symmetricBasis_apply_of_ge (p : ℕ) (ij : upperTriangle p) {k l : Fin p} (h : l ≤ k) : ↑((symmetricBasis p) ij) k l = if ij = ⟨(l, k), h⟩ then 1 else 0

theorem TauCeti.coe_symmetricBasis_diag (p : ℕ) (i : Fin p) : ↑((symmetricBasis p) ⟨(i, i), ⋯⟩) = Matrix.single i i 1

On the diagonal, the coordinate basis vector is a single matrix unit.

theorem TauCeti.coe_symmetricBasis_offDiag (p : ℕ) {i j : Fin p} (hij : i ≤ j) (hne : i ≠ j) : ↑((symmetricBasis p) ⟨(i, j), hij⟩) = Matrix.single i j 1 + Matrix.single j i 1

Off the diagonal, the coordinate basis vector is a symmetrized pair of matrix units.

The one-dimensional carrier

@[instance_reducible]

instance TauCeti.uniqueUpperTriangleOne : Unique (upperTriangle 1)

In dimension one there is a single on-or-above-diagonal position.

Equations

• TauCeti.uniqueUpperTriangleOne = { default := ⟨(0, 0), TauCeti.uniqueUpperTriangleOne._proof_2⟩, uniq := TauCeti.uniqueUpperTriangleOne._proof_3 }

noncomputable def TauCeti.symmetricFinOneEquiv : ↥(selfAdjoint.submodule ℝ (Matrix (Fin 1) (Fin 1) ℝ)) ≃L[ℝ] ℝ

A 1 × 1 symmetric matrix is its single entry. This is the upper-triangular coordinate system TauCeti.symmetricCoordinates in dimension one, with the single coordinate read as a real number rather than as a function on a one-element index type. It is the identification under which a one-dimensional symmetric-matrix law becomes a law on ℝ.

Equations

• TauCeti.symmetricFinOneEquiv = (TauCeti.symmetricCoordinates 1).trans (ContinuousLinearEquiv.funUnique (TauCeti.upperTriangle 1) ℝ ℝ)

@[simp]

theorem TauCeti.symmetricFinOneEquiv_apply (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin 1) (Fin 1) ℝ))) : symmetricFinOneEquiv A = ↑A 0 0

@[simp]

theorem TauCeti.coe_symmetricFinOneEquiv_symm_apply (x : ℝ) (i j : Fin 1) : ↑(symmetricFinOneEquiv.symm x) i j = x

The trace pairing

theorem selfAdjoint.inner_eq_trace_mul {p : ℕ} (A Θ : ↥(submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : inner ℝ A Θ = (↑Θ * ↑A).trace

On the symmetric subspace, the Frobenius inner product is the trace pairing. This makes MeasureTheory.charFun on the subspace use the same pairing as the Wishart trace statistics.

theorem selfAdjoint.continuous_trace_mul_coe {p : ℕ} (Θ : ↥(submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : Continuous fun (A : ↥(submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => (↑Θ * ↑A).trace

The trace pairing against a fixed symmetric matrix is continuous, being the Frobenius inner product with that matrix.

theorem selfAdjoint.continuous_coe_apply {p : ℕ} (i j : Fin p) : Continuous fun (A : ↥(submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => ↑A i j

Reading off an entry of a symmetric matrix is continuous.

theorem selfAdjoint.measurable_coe_apply {p : ℕ} (i j : Fin p) : Measurable fun (A : ↥(submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => ↑A i j

Reading off an entry of a symmetric matrix is measurable.

theorem selfAdjoint.continuous_exp_trace_mul_coe {p : ℕ} (Θ : ↥(submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) (t : ℝ) : Continuous fun (A : ↥(submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => Real.exp (t * (↑Θ * ↑A).trace)

The exponential of a scalar multiple of the trace pairing is continuous. This is the measurability side condition of the exponential-moment computations on the symmetric subspace.

Representers of the matrix entries

noncomputable def TauCeti.symmetricEntry {p : ℕ} (i j : Fin p) : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

The symmetric matrix (Eᵢⱼ + Eⱼᵢ) / 2, which represents evaluation at the (i, j) entry under the trace pairing: trace (symmetricEntry i j * A) = A i j for every symmetric A.

Equations

• TauCeti.symmetricEntry i j = ⟨(1 / 2) • (Matrix.single i j 1 + Matrix.single j i 1), ⋯⟩

theorem TauCeti.coe_symmetricEntry {p : ℕ} (i j : Fin p) : ↑(symmetricEntry i j) = (1 / 2) • (Matrix.single i j 1 + Matrix.single j i 1)

theorem TauCeti.trace_symmetricEntry_mul {p : ℕ} (i j : Fin p) {A : Matrix (Fin p) (Fin p) ℝ} (hA : A.IsHermitian) : (↑(symmetricEntry i j) * A).trace = A i j

Pairing a Hermitian matrix with TauCeti.symmetricEntry i j under the trace reads off its (i, j) entry.

@[simp]

theorem TauCeti.trace_symmetricEntry_mul_coe {p : ℕ} (i j : Fin p) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : (↑(symmetricEntry i j) * ↑A).trace = ↑A i j

The trace pairing of TauCeti.symmetricEntry i j with an element of the symmetric subspace is its (i, j) entry.

theorem TauCeti.trace_symmetricEntry_mul_mul_symmetricEntry_mul {p : ℕ} (i j k l : Fin p) {S : Matrix (Fin p) (Fin p) ℝ} (hS : S.IsHermitian) : (↑(symmetricEntry i j) * S * ↑(symmetricEntry k l) * S).trace = (S i k * S j l + S i l * S j k) / 2

The bilinear map (M, N) ↦ trace (M * S * N * S) at two entry representers, for a Hermitian S.