The Cholesky change of variables on the symmetric matrices

Every positive-definite symmetric matrix is L * Lᵀ for a unique lower-triangular L with positive diagonal, so the on-or-below-diagonal entries of L are free coordinates on the positive-definite cone. This file transports TauCeti.symmetricLebesgue through that parametrization: on the cone it is the pushforward of Lebesgue measure on the region where every diagonal coordinate is positive, weighted by the Jacobian 2 ^ p * ∏ i, (L i i) ^ (p - i) of L ↦ L * Lᵀ.

That weight is a product of powers of the diagonal coordinates alone, so the resulting coordinate integral splits into independent one-dimensional integrals. This is how the cone integral defining the multivariate Gamma function, and with it the Wishart normalizing constant, is evaluated.

The symmetric matrices carry the on-or-above-diagonal coordinates TauCeti.symmetricCoordinates, whereas the Cholesky Jacobian is computed in the on-or-below-diagonal coordinates. Transposing positions relabels one coordinate system into the other, and the resulting chart TauCeti.symmetricLowerCoordinates carries the same Lebesgue normalization.

Main declarations

• TauCeti.symmetricLowerCoordinates — the on-or-below-diagonal chart on the symmetric matrices.
• TauCeti.lowerTriangleGram — the symmetric matrix L * Lᵀ built from coordinates for L.
• TauCeti.posDiagLowerRegion — the coordinate region cut out by a positive diagonal.
• TauCeti.choleskyLowerCoordinates — the Cholesky factor of a positive-definite matrix, read in those coordinates, inverting the Gram map there.
• TauCeti.choleskyJacobianDensity — the Jacobian weight of the change of variables.
• TauCeti.map_cholesky_symmetricLebesgue — the change of variables.
• TauCeti.setLIntegral_posDef_symmetricLebesgue — its integral form.
• TauCeti.integral_posDef_symmetricLebesgue — its Bochner-integral form.

References

• R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley, 1982, Theorem 2.1.9.

The on-or-below-diagonal chart

def TauCeti.lowerTriangleEquivUpperTriangle (p : ℕ) : lowerTriangle p ≃ upperTriangle p

Transposing a position matches the on-or-below-diagonal positions of a p × p matrix with the on-or-above-diagonal ones.

Equations

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

@[simp]

theorem TauCeti.lowerTriangleEquivUpperTriangle_apply_coe (p : ℕ) (ij : lowerTriangle p) : ↑((lowerTriangleEquivUpperTriangle p) ij) = (↑ij).swap

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

The continuous linear equivalence reading off the on-or-below-diagonal entries of a symmetric matrix. It is TauCeti.symmetricCoordinates relabelled by transposing positions, so the Lebesgue measure it induces is again TauCeti.symmetricLebesgue.

Equations

• TauCeti.symmetricLowerCoordinates p = (TauCeti.symmetricCoordinates p).trans (LinearEquiv.funCongrLeft ℝ ℝ (TauCeti.lowerTriangleEquivUpperTriangle p)).toContinuousLinearEquiv

@[simp]

theorem TauCeti.symmetricLowerCoordinates_apply (p : ℕ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) (ij : lowerTriangle p) : (symmetricLowerCoordinates p) A ij = ↑A (↑ij).1 (↑ij).2

@[simp]

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

@[simp]

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

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

The measurable equivalence induced by TauCeti.symmetricLowerCoordinates.

Equations

• TauCeti.symmetricLowerCoordinatesMeasurableEquiv p = (TauCeti.symmetricLowerCoordinates p).toHomeomorph.toMeasurableEquiv

@[simp]

theorem TauCeti.symmetricLowerCoordinatesMeasurableEquiv_coe (p : ℕ) : ⇑(symmetricLowerCoordinatesMeasurableEquiv p) = ⇑(symmetricLowerCoordinates p)

@[simp]

theorem TauCeti.symmetricLowerCoordinatesMeasurableEquiv_symm_coe (p : ℕ) : ⇑(symmetricLowerCoordinatesMeasurableEquiv p).symm = ⇑(symmetricLowerCoordinates p).symm

theorem TauCeti.measurePreserving_symmetricLowerCoordinates (p : ℕ) : MeasureTheory.MeasurePreserving (⇑(symmetricLowerCoordinates p)) (symmetricLebesgue p) MeasureTheory.volume

The on-or-below-diagonal chart carries TauCeti.symmetricLebesgue to Lebesgue measure on the coordinate space: relabelling coordinates by a bijection of index types preserves product Lebesgue measure.

theorem TauCeti.measurePreserving_symmetricLowerCoordinates_symm (p : ℕ) : MeasureTheory.MeasurePreserving (⇑(symmetricLowerCoordinates p).symm) MeasureTheory.volume (symmetricLebesgue p)

The chart reconstruction carries Lebesgue measure on the coordinate space to TauCeti.symmetricLebesgue.

The Gram map and the positive-diagonal region

def TauCeti.lowerTriangleGram (p : ℕ) (x : lowerTriangle p → ℝ) : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

The symmetric matrix L * Lᵀ, where L is the lower-triangular matrix whose on-or-below-diagonal entries are x. On the positive-diagonal region this is Cholesky reconstruction.

Equations

• TauCeti.lowerTriangleGram p x = ⟨(TauCeti.lowerTriangleMatrix p) x * ((TauCeti.lowerTriangleMatrix p) x).transpose, ⋯⟩

@[simp]

theorem TauCeti.coe_lowerTriangleGram (p : ℕ) (x : lowerTriangle p → ℝ) : ↑(lowerTriangleGram p x) = (lowerTriangleMatrix p) x * ((lowerTriangleMatrix p) x).transpose

theorem TauCeti.continuous_lowerTriangleGram (p : ℕ) : Continuous (lowerTriangleGram p)

theorem TauCeti.measurable_lowerTriangleGram (p : ℕ) : Measurable (lowerTriangleGram p)

@[simp]

theorem TauCeti.symmetricLowerCoordinates_lowerTriangleGram (p : ℕ) (x : lowerTriangle p → ℝ) : (symmetricLowerCoordinates p) (lowerTriangleGram p x) = choleskyReconstructionCoordinates p x

Reading the on-or-below-diagonal entries of L * Lᵀ is the coordinate form of Cholesky reconstruction.

theorem TauCeti.lowerTriangleGram_eq_symm_apply (p : ℕ) (x : lowerTriangle p → ℝ) : lowerTriangleGram p x = (symmetricLowerCoordinates p).symm (choleskyReconstructionCoordinates p x)

The Gram map factors through the chart: it reconstructs a symmetric matrix from the coordinate form of Cholesky reconstruction.

def TauCeti.posDiagLowerRegion (p : ℕ) : Set (lowerTriangle p → ℝ)

The region of the lower-triangular coordinates with positive diagonal: the set underlying TauCeti.PosDiagLowerCoordinates, and the set of coordinates of Cholesky factors.

Equations

• TauCeti.posDiagLowerRegion p = {x : TauCeti.lowerTriangle p → ℝ | ∀ (i : Fin p), 0 < x ⟨(i, i), ⋯⟩}

theorem TauCeti.posDiagLowerRegion_def (p : ℕ) : posDiagLowerRegion p = {x : lowerTriangle p → ℝ | ∀ (i : Fin p), 0 < x ⟨(i, i), ⋯⟩}

The positive-diagonal region is the set of coordinate vectors whose diagonal coordinates are positive.

@[simp]

theorem TauCeti.mem_posDiagLowerRegion (p : ℕ) {x : lowerTriangle p → ℝ} : x ∈ posDiagLowerRegion p ↔ ∀ (i : Fin p), 0 < x ⟨(i, i), ⋯⟩

theorem TauCeti.isOpen_posDiagLowerRegion (p : ℕ) : IsOpen (posDiagLowerRegion p)

theorem TauCeti.measurableSet_posDiagLowerRegion (p : ℕ) : MeasurableSet (posDiagLowerRegion p)

theorem TauCeti.lowerTriangleGram_image_posDiagLowerRegion (p : ℕ) : lowerTriangleGram p '' posDiagLowerRegion p = {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}

The Gram map sends the positive-diagonal region onto the positive-definite cone: a positive-diagonal lower-triangular matrix has positive-definite Gram matrix, and conversely every positive-definite matrix is the Gram matrix of its Cholesky factor.

theorem TauCeti.injOn_lowerTriangleGram (p : ℕ) : Set.InjOn (lowerTriangleGram p) (posDiagLowerRegion p)

Cholesky factors are unique, so the Gram map is injective on the positive-diagonal region.

theorem TauCeti.injOn_choleskyReconstructionCoordinates (p : ℕ) : Set.InjOn (choleskyReconstructionCoordinates p) (posDiagLowerRegion p)

The coordinate form of Cholesky reconstruction is injective on the positive-diagonal region: it is the Gram map read through a chart.

Cholesky coordinates of a positive-definite matrix

theorem TauCeti.posDef_lowerTriangleGram (p : ℕ) {x : lowerTriangle p → ℝ} (hx : x ∈ posDiagLowerRegion p) : (↑(lowerTriangleGram p x)).PosDef

The Gram map lands in the positive-definite cone on the positive-diagonal region.

noncomputable def TauCeti.choleskyLowerCoordinates (p : ℕ) (A : PosDefMatrix p) : lowerTriangle p → ℝ

The on-or-below-diagonal entries of the Cholesky factor of a positive-definite symmetric matrix: the same coordinates in which TauCeti.map_cholesky_symmetricLebesgue expresses the change of variables, read off the matrix itself.

Equations

• TauCeti.choleskyLowerCoordinates p A = ↑((TauCeti.lowerTriangleCoordinatesHomeomorph p) (TauCeti.cholesky A))

@[simp]

theorem TauCeti.choleskyLowerCoordinates_apply (p : ℕ) (A : PosDefMatrix p) (ij : lowerTriangle p) : choleskyLowerCoordinates p A ij = ↑(cholesky A) (↑ij).1 (↑ij).2

theorem TauCeti.continuous_choleskyLowerCoordinates (p : ℕ) : Continuous (choleskyLowerCoordinates p)

theorem TauCeti.measurable_choleskyLowerCoordinates (p : ℕ) : Measurable (choleskyLowerCoordinates p)

theorem TauCeti.choleskyLowerCoordinates_mem_posDiagLowerRegion (p : ℕ) (A : PosDefMatrix p) : choleskyLowerCoordinates p A ∈ posDiagLowerRegion p

The Cholesky factor has positive diagonal, so its coordinates lie in the positive-diagonal region.

@[simp]

theorem TauCeti.lowerTriangleGram_choleskyLowerCoordinates (p : ℕ) (A : PosDefMatrix p) : lowerTriangleGram p (choleskyLowerCoordinates p A) = ↑A

The Gram map inverts Cholesky factorization. A positive-definite matrix is the Gram matrix built from the coordinates of its Cholesky factor.

@[simp]

theorem TauCeti.choleskyLowerCoordinates_lowerTriangleGram (p : ℕ) {x : lowerTriangle p → ℝ} (hx : x ∈ posDiagLowerRegion p) : choleskyLowerCoordinates p ⟨lowerTriangleGram p x, ⋯⟩ = x

Cholesky factorization inverts the Gram map. On the positive-diagonal region the coordinates of the Cholesky factor of L * Lᵀ are the coordinates of L again.

The change of variables

def TauCeti.choleskyJacobianDensity (p : ℕ) (x : lowerTriangle p → ℝ) : ENNReal

The Jacobian weight of the Cholesky change of variables, in lower-triangular coordinates: ENNReal.ofReal (2 ^ p * ∏ i, (L i i) ^ (p - i)). On TauCeti.posDiagLowerRegion, where the diagonal coordinates are positive, this is the absolute determinant of the derivative of L ↦ L * Lᵀ; elsewhere the product can be negative, and the weight then truncates to 0. The change of variables below uses the weight only on that region.

Equations

• TauCeti.choleskyJacobianDensity p x = ENNReal.ofReal (2 ^ p * ∏ i : Fin p, x ⟨(i, i), ⋯⟩ ^ (p - ↑i))

theorem TauCeti.choleskyJacobianDensity_def (p : ℕ) (x : lowerTriangle p → ℝ) : choleskyJacobianDensity p x = ENNReal.ofReal (2 ^ p * ∏ i : Fin p, x ⟨(i, i), ⋯⟩ ^ (p - ↑i))

theorem TauCeti.measurable_choleskyJacobianDensity (p : ℕ) : Measurable (choleskyJacobianDensity p)

theorem TauCeti.map_cholesky_symmetricLebesgue (p : ℕ) : MeasureTheory.Measure.map (lowerTriangleGram p) ((MeasureTheory.volume.restrict (posDiagLowerRegion p)).withDensity (choleskyJacobianDensity p)) = (symmetricLebesgue p).restrict {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}

The Cholesky change of variables. Lebesgue measure on the symmetric matrices, restricted to the positive-definite cone, is the image of the positive-diagonal coordinate region under L ↦ L * Lᵀ, weighted by the Cholesky Jacobian.

@[simp]

theorem TauCeti.toReal_choleskyJacobianDensity (p : ℕ) {x : lowerTriangle p → ℝ} (hx : x ∈ posDiagLowerRegion p) : (choleskyJacobianDensity p x).toReal = 2 ^ p * ∏ i : Fin p, x ⟨(i, i), ⋯⟩ ^ (p - ↑i)

On the positive-diagonal region the Jacobian weight is nonnegative, so it agrees with the real number 2 ^ p * ∏ i, (L i i) ^ (p - i) it truncates.

theorem TauCeti.setLIntegral_posDef_symmetricLebesgue (p : ℕ) {f : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) → ENNReal} (hf : Measurable f) : ∫⁻ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, f A ∂symmetricLebesgue p = ∫⁻ (x : lowerTriangle p → ℝ) in posDiagLowerRegion p, choleskyJacobianDensity p x * f (lowerTriangleGram p x)

The integral form of the Cholesky change of variables: an integral over the positive-definite cone becomes a weighted integral over the positive-diagonal coordinate region.

theorem TauCeti.integral_posDef_symmetricLebesgue (p : ℕ) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) → E} (hf : MeasureTheory.AEStronglyMeasurable f ((symmetricLebesgue p).restrict {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef})) : ∫ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, f A ∂symmetricLebesgue p = ∫ (x : lowerTriangle p → ℝ) in posDiagLowerRegion p, (2 ^ p * ∏ i : Fin p, x ⟨(i, i), ⋯⟩ ^ (p - ↑i)) • f (lowerTriangleGram p x)

The Bochner-integral form of the Cholesky change of variables: an integral over the positive-definite cone becomes a weighted integral over the positive-diagonal coordinate region.