The Jacobian of Cholesky reconstruction

Cholesky reconstruction sends a lower-triangular matrix L to the symmetric matrix L * Lᵀ. Both sides are determined by their on-or-below-diagonal entries, so in the coordinates of TauCeti.lowerTriangle the reconstruction becomes a quadratic self-map TauCeti.choleskyReconstructionCoordinates of a Euclidean space. This file computes its derivative and the determinant 2 ^ p * ∏ i, (L i i) ^ (p - i) of that derivative.

This determinant is the Jacobian factor of the change of variables S = L * Lᵀ, which runs from the positive-diagonal lower-triangular matrices to the positive-definite cone carrying Lebesgue measure in symmetric coordinates. Substituting it into an integral over the cone — the multivariate Gamma integral, and through it the Wishart normalizing constant — turns that integral into a product of independent one-dimensional integrals.

The determinant is computed by ordering the lower-triangular positions by column and then by row. In that order the derivative is triangular, and its diagonal entry at position (i, j) is L j j, doubled when i = j.

Main declarations

• TauCeti.choleskyReconstructionCoordinates — reconstruction read in triangular coordinates.
• TauCeti.fderivCholeskyReconstructionCoordinates — its derivative, H ↦ L * Hᵀ + H * Lᵀ.
• TauCeti.abs_det_fderiv_choleskyReconstructionCoordinates — the Jacobian factor.

References

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

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

Cholesky reconstruction L ↦ L * Lᵀ read in lower-triangular coordinates on both sides: the input lists the on-or-below-diagonal entries of L, and the output lists those of L * Lᵀ, which determine that symmetric matrix.

Equations

• TauCeti.choleskyReconstructionCoordinates p x ij = ((TauCeti.lowerTriangleMatrix p) x * ((TauCeti.lowerTriangleMatrix p) x).transpose) (↑ij).1 (↑ij).2

noncomputable def TauCeti.fderivCholeskyReconstructionCoordinates (p : ℕ) (x : lowerTriangle p → ℝ) : (lowerTriangle p → ℝ) →L[ℝ] lowerTriangle p → ℝ

The derivative of TauCeti.choleskyReconstructionCoordinates at x: writing L for the lower-triangular matrix of x, it sends the lower-triangular matrix H of an increment to the on-or-below-diagonal entries of L * Hᵀ + H * Lᵀ.

Equations

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

@[simp]

theorem TauCeti.choleskyReconstructionCoordinates_apply {p : ℕ} (x : lowerTriangle p → ℝ) (ij : lowerTriangle p) : choleskyReconstructionCoordinates p x ij = ∑ k : Fin p, (lowerTriangleMatrix p) x (↑ij).1 k * (lowerTriangleMatrix p) x (↑ij).2 k

theorem TauCeti.choleskyReconstructionCoordinates_lowerTriangleCoordinatesHomeomorph {p : ℕ} (L : PosDiagLowerTriangular p) (ij : lowerTriangle p) : choleskyReconstructionCoordinates p (↑((lowerTriangleCoordinatesHomeomorph p) L)) ij = ↑↑(choleskyReconstruction L) (↑ij).1 (↑ij).2

On the coordinates of a positive-diagonal lower-triangular matrix, the coordinate form of Cholesky reconstruction reads off TauCeti.choleskyReconstruction.

@[simp]

theorem TauCeti.fderivCholeskyReconstructionCoordinates_apply {p : ℕ} (x h : lowerTriangle p → ℝ) (ij : lowerTriangle p) : (fderivCholeskyReconstructionCoordinates p x) h ij = ((lowerTriangleMatrix p) x * ((lowerTriangleMatrix p) h).transpose + (lowerTriangleMatrix p) h * ((lowerTriangleMatrix p) x).transpose) (↑ij).1 (↑ij).2

theorem TauCeti.hasFDerivAt_choleskyReconstructionCoordinates {p : ℕ} (x : lowerTriangle p → ℝ) : HasFDerivAt (choleskyReconstructionCoordinates p) (fderivCholeskyReconstructionCoordinates p x) x

Cholesky reconstruction is quadratic in the triangular coordinates, hence differentiable, with the derivative computed entrywise from the product rule.

theorem TauCeti.differentiable_choleskyReconstructionCoordinates {p : ℕ} : Differentiable ℝ (choleskyReconstructionCoordinates p)

@[simp]

theorem TauCeti.fderiv_choleskyReconstructionCoordinates {p : ℕ} (x : lowerTriangle p → ℝ) : fderiv ℝ (choleskyReconstructionCoordinates p) x = fderivCholeskyReconstructionCoordinates p x

The Fréchet derivative of TauCeti.choleskyReconstructionCoordinates at x is TauCeti.fderivCholeskyReconstructionCoordinates p x.

The determinant of the derivative

theorem TauCeti.det_fderiv_choleskyReconstructionCoordinates {p : ℕ} (x : lowerTriangle p → ℝ) : (fderiv ℝ (choleskyReconstructionCoordinates p) x).det = 2 ^ p * ∏ i : Fin p, x ⟨(i, i), ⋯⟩ ^ (p - ↑i)

The Jacobian determinant of Cholesky reconstruction. In lower-triangular coordinates the derivative of L ↦ L * Lᵀ has determinant 2 ^ p * ∏ i, (L i i) ^ (p - i).

theorem TauCeti.abs_det_fderiv_choleskyReconstructionCoordinates {p : ℕ} (x : lowerTriangle p → ℝ) (hx : ∀ (i : Fin p), 0 < x ⟨(i, i), ⋯⟩) : |(fderiv ℝ (choleskyReconstructionCoordinates p) x).det| = 2 ^ p * ∏ i : Fin p, x ⟨(i, i), ⋯⟩ ^ (p - ↑i)

The absolute Jacobian factor of Cholesky reconstruction. On the positive-diagonal region, which is where the Cholesky factors live, the determinant above is positive and is therefore the density appearing in the change-of-variables formula.