Congruence and the change of variables on the symmetric subspace

For a rectangular matrix M, congruence A ↦ M * A * Mᵀ is a linear map between symmetric subspaces. For an invertible square matrix C, it is a continuous linear automorphism. In the upper-triangular coordinates its determinant is (det C) ^ (p + 1), so the congruence image of a set has |det C| ^ (p + 1) times its TauCeti.symmetricLebesgue volume, and the pushforward of symmetricLebesgue is (|det C| ^ (p + 1))⁻¹ • symmetricLebesgue. This change of variables supplies the general-scale Wishart formulas.

The determinant is computed for an arbitrary square matrix M, not only invertible ones, with the invertible case as a corollary. The underlying generic trace and determinant-pencil identities for rectangular congruence are in TauCeti.LinearAlgebra.Matrix.Congruence.

Main declarations

• Matrix.symmetricCongruenceLinearMap — congruence by an arbitrary rectangular matrix, as a linear map between symmetric subspaces.
• Matrix.inner_symmetricCongruenceLinearMap — congruence by M is adjoint to congruence by Mᵀ for the Frobenius pairing.
• MeasureTheory.Measure.charFun_map_symmetricCongruenceLinearMap — the corresponding transformation rule for characteristic functions.
• Matrix.det_symmetricCongruenceLinearMap — its determinant is (det M) ^ (p + 1).
• Matrix.GeneralLinearGroup.symmetricCongruence — congruence by an invertible matrix, as a continuous linear automorphism.
• Matrix.GeneralLinearGroup.map_symmetricCongruence_symmetricLebesgue — the induced change of variables for symmetricLebesgue.
• Matrix.GeneralLinearGroup.det_symmetricCongruence_apply — the determinant of a congruence image is (det C) ^ 2 times the determinant.
• Matrix.GeneralLinearGroup.trace_inv_mul_symmetricCongruence_apply — congruence by C turns the trace against the inverse scale (C * Cᵀ)⁻¹ into the plain trace.
• Matrix.GeneralLinearGroup.map_symmetricCongruence_restrict_posDef — the same change of variables on the positive-definite cone, which congruence by an invertible matrix preserves, together with its lower- and Bochner-integral forms.

References

• R. J. Muirhead, Aspects of Multivariate Statistical Theory, Wiley, 1982, chapter 2 (the congruence Jacobian for symmetric matrices and the induced change of variables).

def Matrix.symmetricCongruenceLinearMap {p q : ℕ} (M : Matrix (Fin q) (Fin p) ℝ) : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) →ₗ[ℝ] ↥(selfAdjoint.submodule ℝ (Matrix (Fin q) (Fin q) ℝ))

Congruence A ↦ M * A * Mᵀ by an arbitrary rectangular matrix, as a linear map between symmetric subspaces.

Equations

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

@[simp]

theorem Matrix.coe_symmetricCongruenceLinearMap_apply {p q : ℕ} (M : Matrix (Fin q) (Fin p) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : ↑(M.symmetricCongruenceLinearMap A) = M * ↑A * M.transpose

theorem Matrix.trace_mul_coe_symmetricCongruenceLinearMap {p q : ℕ} (M : Matrix (Fin q) (Fin p) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) (Θ : ↥(selfAdjoint.submodule ℝ (Matrix (Fin q) (Fin q) ℝ))) : (↑Θ * ↑(M.symmetricCongruenceLinearMap A)).trace = (M.transpose * ↑Θ * M * ↑A).trace

The trace pairing of a congruated symmetric matrix can be evaluated on the source by congruating the test matrix with the transpose.

theorem Matrix.inner_symmetricCongruenceLinearMap {p q : ℕ} (M : Matrix (Fin q) (Fin p) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) (Θ : ↥(selfAdjoint.submodule ℝ (Matrix (Fin q) (Fin q) ℝ))) : inner ℝ (M.symmetricCongruenceLinearMap A) Θ = inner ℝ A (M.transpose.symmetricCongruenceLinearMap Θ)

For the Frobenius pairing, congruence by M is adjoint to congruence by Mᵀ.

theorem Matrix.symmetricCongruenceLinearMap_mul {p q r : ℕ} (M : Matrix (Fin q) (Fin p) ℝ) (N : Matrix (Fin p) (Fin r) ℝ) : (M * N).symmetricCongruenceLinearMap = M.symmetricCongruenceLinearMap ∘ₗ N.symmetricCongruenceLinearMap

@[simp]

theorem Matrix.symmetricCongruenceLinearMap_one {p : ℕ} : symmetricCongruenceLinearMap 1 = LinearMap.id

The determinant of congruence

theorem Matrix.det_symmetricCongruenceLinearMap {p : ℕ} (M : Matrix (Fin p) (Fin p) ℝ) : LinearMap.det M.symmetricCongruenceLinearMap = M.det ^ (p + 1)

The determinant of congruence by M on the symmetric subspace is (det M) ^ (p + 1).

Congruence by an invertible matrix

noncomputable def Matrix.GeneralLinearGroup.symmetricCongruence {p : ℕ} (C : GL (Fin p) ℝ) : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) ≃L[ℝ] ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

Congruence A ↦ C * A * Cᵀ by an invertible matrix, as a continuous linear automorphism of the symmetric subspace.

Equations

• C.symmetricCongruence = (LinearEquiv.ofLinearMap (↑C).symmetricCongruenceLinearMap (↑C⁻¹).symmetricCongruenceLinearMap ⋯ ⋯).toContinuousLinearEquiv

@[simp]

theorem Matrix.GeneralLinearGroup.coe_symmetricCongruence_apply {p : ℕ} (C : GL (Fin p) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : ↑(C.symmetricCongruence A) = ↑C * ↑A * (↑C).transpose

@[simp]

theorem Matrix.GeneralLinearGroup.symmetricCongruence_toLinearMap {p : ℕ} (C : GL (Fin p) ℝ) : ↑↑C.symmetricCongruence = (↑C).symmetricCongruenceLinearMap

@[simp]

theorem Matrix.GeneralLinearGroup.symmetricCongruence_one {p : ℕ} : symmetricCongruence 1 = ContinuousLinearEquiv.refl ℝ ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))

Congruence by the identity is the identity.

@[simp]

theorem Matrix.GeneralLinearGroup.symmetricCongruence_mul {p : ℕ} (C D : GL (Fin p) ℝ) : (C * D).symmetricCongruence = D.symmetricCongruence.trans C.symmetricCongruence

Congruence by a product is the composite of the two congruences, the right factor acting first.

@[simp]

theorem Matrix.GeneralLinearGroup.symmetricCongruence_symm {p : ℕ} (C : GL (Fin p) ℝ) : C.symmetricCongruence.symm = C⁻¹.symmetricCongruence

Undoing congruence by C is congruence by C⁻¹.

theorem Matrix.GeneralLinearGroup.det_symmetricCongruence {p : ℕ} (C : GL (Fin p) ℝ) : LinearMap.det ↑↑C.symmetricCongruence = (↑C).det ^ (p + 1)

In the upper-triangular coordinates, congruence by C has determinant (det C) ^ (p + 1).

theorem Matrix.GeneralLinearGroup.det_symmetricCongruence_apply {p : ℕ} (C : GL (Fin p) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : (↑(C.symmetricCongruence A)).det = (↑C).det ^ 2 * (↑A).det

Congruence by C multiplies the determinant of a symmetric matrix by (det C) ^ 2.

theorem Matrix.GeneralLinearGroup.trace_inv_mul_symmetricCongruence_apply {p : ℕ} (C : GL (Fin p) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : ((↑C * (↑C).transpose)⁻¹ * ↑(C.symmetricCongruence A)).trace = (↑A).trace

Congruence by C turns the trace against the inverse of the scale C * Cᵀ into the plain trace: the two copies of C cancel against the inverse.

theorem Matrix.GeneralLinearGroup.map_symmetricCongruence_symmetricLebesgue {p : ℕ} (C : GL (Fin p) ℝ) : MeasureTheory.Measure.map (⇑C.symmetricCongruence) (TauCeti.symmetricLebesgue p) = (ENNReal.ofReal |(↑C).det| ^ (p + 1))⁻¹ • TauCeti.symmetricLebesgue p

The pushforward of symmetricLebesgue under congruence by C is (|det C| ^ (p + 1))⁻¹ • symmetricLebesgue; equivalently, the congruence image of a set has |det C| ^ (p + 1) times its volume. This change of variables supplies the general-scale Wishart formulas.

Congruence on the positive-definite cone

theorem Matrix.GeneralLinearGroup.posDef_symmetricCongruence_iff {p : ℕ} (C : GL (Fin p) ℝ) (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) : (↑(C.symmetricCongruence A)).PosDef ↔ (↑A).PosDef

Congruence by an invertible matrix preserves positive definiteness in both directions.

theorem Matrix.GeneralLinearGroup.preimage_symmetricCongruence_posDef {p : ℕ} (C : GL (Fin p) ℝ) : ⇑C.symmetricCongruence ⁻¹' {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef} = {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}

Congruence by an invertible matrix maps the positive-definite cone onto itself.

theorem Matrix.GeneralLinearGroup.map_symmetricCongruence_restrict_posDef {p : ℕ} (C : GL (Fin p) ℝ) : MeasureTheory.Measure.map (⇑C.symmetricCongruence) ((TauCeti.symmetricLebesgue p).restrict {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}) = (ENNReal.ofReal |(↑C).det| ^ (p + 1))⁻¹ • (TauCeti.symmetricLebesgue p).restrict {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}

The change of variables of TauCeti.symmetricLebesgue under congruence, restricted to the positive-definite cone: congruence by C leaves the cone invariant, so the restricted measure picks up the same factor (|det C| ^ (p + 1))⁻¹ as the unrestricted one.

theorem Matrix.GeneralLinearGroup.lintegral_posDef_symmetricCongruence {p : ℕ} (C : GL (Fin p) ℝ) (f : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) → ENNReal) : ∫⁻ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, f (C.symmetricCongruence A) ∂TauCeti.symmetricLebesgue p = (ENNReal.ofReal |(↑C).det| ^ (p + 1))⁻¹ * ∫⁻ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, f A ∂TauCeti.symmetricLebesgue p

The congruence change of variables for lower integrals over the positive-definite cone. No measurability hypothesis on f is needed, because congruence by C is a measurable equivalence.

theorem Matrix.GeneralLinearGroup.integral_posDef_symmetricCongruence {p : ℕ} (C : GL (Fin p) ℝ) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) → E) : ∫ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, f (C.symmetricCongruence A) ∂TauCeti.symmetricLebesgue p = (|(↑C).det| ^ (p + 1))⁻¹ • ∫ (A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) in {A : ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ)) | (↑A).PosDef}, f A ∂TauCeti.symmetricLebesgue p

The congruence change of variables for Bochner integrals over the positive-definite cone.

theorem MeasureTheory.Measure.charFun_map_symmetricCongruenceLinearMap {p q : ℕ} (μ : Measure ↥(selfAdjoint.submodule ℝ (Matrix (Fin p) (Fin p) ℝ))) (M : Matrix (Fin q) (Fin p) ℝ) (Θ : ↥(selfAdjoint.submodule ℝ (Matrix (Fin q) (Fin q) ℝ))) : charFun (map (⇑M.symmetricCongruenceLinearMap) μ) Θ = charFun μ (M.transpose.symmetricCongruenceLinearMap Θ)

Mapping a measure by rectangular congruence precomposes its characteristic function with congruence by the transpose.