Inversion and the change of variables on the positive-definite cone

Matrix inversion is a self-map TauCeti.symmetricInv of the symmetric subspace, and an involution of the positive-definite cone. Its derivative at an invertible A is H ↦ -A⁻¹ H A⁻¹, that is, minus the congruence by A⁻¹, whose determinant Matrix.det_symmetricCongruenceLinearMap already computes. Hence the absolute Jacobian of inversion is |det A| ^ (-(p + 1)), and TauCeti.map_symmetricInv_symmetricLebesgue records the resulting change of variables: inversion carries TauCeti.symmetricLebesgue restricted to the cone to the same restriction weighted by (det B) ^ (-(p + 1)).

This is the change of variables behind the inverse-Wishart density: it reads the density of the image of a Wishart law under inversion off the density of the law itself.

Main declarations

• TauCeti.symmetricInv — matrix inversion as a self-map of the symmetric subspace.
• TauCeti.bijOn_symmetricInv — inversion is a bijection of the positive-definite cone onto itself.
• TauCeti.measurable_symmetricInv — inversion is measurable.
• TauCeti.hasFDerivAt_symmetricInv — its derivative at an invertible matrix is minus the congruence by the inverse.
• TauCeti.abs_det_fderiv_symmetricInv — the absolute Jacobian of inversion.
• TauCeti.map_symmetricInv_symmetricLebesgue — the change of variables on the positive-definite cone.

References

• R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley, 1982, chapter 2 (the Jacobian of symmetric inversion and the inverse-Wishart density).

Inversion on the symmetric subspace

noncomputable def TauCeti.symmetricInv {p : ℕ} (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

Matrix inversion as a self-map of the symmetric subspace. Mathlib's totalized inverse is zero on singular matrices and that value is kept here; on the positive-definite cone, where the Wishart laws live, the map is an involution.

@[simp]

theorem TauCeti.coe_symmetricInv {p : ℕ} (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : ↑(symmetricInv A) = (↑A)⁻¹

The underlying matrix of the inverse is the inverse of the underlying matrix.

@[simp]

theorem TauCeti.symmetricInv_symmetricInv {p : ℕ} {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} (hA : (↑A).det ≠ 0) : symmetricInv (symmetricInv A) = A

Inversion is an involution at an invertible matrix.

theorem TauCeti.bijOn_symmetricInv (p : ℕ) : Set.BijOn symmetricInv {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef} {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}

Inversion is a bijection of the positive-definite cone onto itself: it maps the cone into itself and is its own inverse there.

Measurability of inversion

theorem TauCeti.measurable_symmetricInv {p : ℕ} : Measurable symmetricInv

Inversion is measurable, being a rational expression in the entries: Mathlib's totalized inverse is (det A)⁻¹ • adjugate A everywhere.

The derivative of inversion

theorem TauCeti.hasFDerivAt_symmetricInv {p : ℕ} {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} (hA : IsUnit (↑A).det) : HasFDerivAt symmetricInv (-LinearMap.toContinuousLinearMap (↑A)⁻¹.symmetricCongruenceLinearMap) A

The derivative of inversion at an invertible symmetric matrix A is H ↦ -A⁻¹ H A⁻¹, minus the congruence by A⁻¹.

theorem TauCeti.abs_det_fderiv_symmetricInv {p : ℕ} {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))} (hA : IsUnit (↑A).det) : |(fderiv ℝ symmetricInv A).det| = |(↑A).det| ^ (-(↑p + 1))

The absolute Jacobian of inversion at an invertible symmetric matrix A is |det A| ^ (-(p + 1)).

The change of variables

theorem TauCeti.map_symmetricInv_symmetricLebesgue (p : ℕ) : MeasureTheory.Measure.map symmetricInv ((symmetricLebesgue p).restrict {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}) = ((symmetricLebesgue p).restrict {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}).withDensity fun (B : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) => ENNReal.ofReal ((↑B).det ^ (-(↑p + 1)))

The change of variables for inversion on the positive-definite cone. The pushforward of TauCeti.symmetricLebesgue restricted to the cone under inversion is the same restriction weighted by (det B) ^ (-(p + 1)). This is what turns the Wishart density into the inverse-Wishart density.