Continuity and measurability of the Cholesky equivalence

This file proves that Cholesky factorization is a homeomorphism between the positive-definite symmetric matrices and the positive-diagonal lower-triangular matrices, both carrying their subtype topologies, and hence a measurable equivalence for the corresponding Borel structures.

Reconstruction L ↦ L * Lᵀ is visibly continuous. The continuity of the factorization itself is deduced from a properness argument rather than from formulas for the Cholesky entries: a compact set K of positive-definite matrices has bounded diagonal entries, and the i-th row of a Gram factor of A has squared norm A i i, so the factors of the matrices in K form a bounded set. It is also closed, since a lower-triangular limit with nonnegative diagonal and positive-definite Gram matrix has nonzero determinant, hence positive diagonal. Reconstruction is therefore a continuous proper bijection, hence closed, hence a homeomorphism.

Main results

• TauCeti.continuous_choleskyReconstruction — reconstruction is continuous.
• TauCeti.isProperMap_choleskyReconstruction — reconstruction is a proper map.
• TauCeti.continuous_cholesky — Cholesky factorization is continuous.
• TauCeti.choleskyHomeomorph — the resulting homeomorphism.
• TauCeti.measurable_cholesky, TauCeti.measurable_choleskyReconstruction — measurability in both directions.
• TauCeti.choleskyMeasurableEquiv — the resulting measurable equivalence.

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, second edition, Cambridge University Press, 2013, Section 7.2.

theorem TauCeti.continuous_choleskyReconstruction {p : ℕ} : Continuous choleskyReconstruction

Reconstructing a positive-definite matrix from its lower-triangular factor is continuous.

theorem TauCeti.isProperMap_choleskyReconstruction {p : ℕ} : IsProperMap choleskyReconstruction

Reconstruction from positive-diagonal lower-triangular factors is a proper map: the factors of a compact set of positive-definite matrices form a compact set.

theorem TauCeti.continuous_cholesky {p : ℕ} : Continuous cholesky

Cholesky factorization is continuous.

noncomputable def TauCeti.choleskyHomeomorph {p : ℕ} : PosDefMatrix p ≃ₜ PosDiagLowerTriangular p

Cholesky factorization as a homeomorphism between positive-definite symmetric matrices and positive-diagonal lower-triangular matrices.

Equations

• TauCeti.choleskyHomeomorph = { toFun := TauCeti.cholesky, invFun := TauCeti.choleskyReconstruction, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.choleskyHomeomorph_toEquiv {p : ℕ} : choleskyHomeomorph.toEquiv = choleskyEquiv

The equivalence underlying choleskyHomeomorph is choleskyEquiv.

@[simp]

theorem TauCeti.choleskyHomeomorph_apply {p : ℕ} (A : PosDefMatrix p) : choleskyHomeomorph A = cholesky A

@[simp]

theorem TauCeti.choleskyHomeomorph_symm_apply {p : ℕ} (L : PosDiagLowerTriangular p) : choleskyHomeomorph.symm L = choleskyReconstruction L

theorem TauCeti.measurable_cholesky {p : ℕ} : Measurable cholesky

Cholesky factorization is measurable.

theorem TauCeti.measurable_choleskyReconstruction {p : ℕ} : Measurable choleskyReconstruction

Reconstructing a positive-definite matrix from its lower-triangular factor is measurable.

noncomputable def TauCeti.choleskyMeasurableEquiv {p : ℕ} : PosDefMatrix p ≃ᵐ PosDiagLowerTriangular p

Cholesky factorization as a measurable equivalence between positive-definite symmetric matrices and positive-diagonal lower-triangular matrices.

Equations

• TauCeti.choleskyMeasurableEquiv = TauCeti.choleskyHomeomorph.toMeasurableEquiv

@[simp]

theorem TauCeti.choleskyMeasurableEquiv_apply {p : ℕ} (A : PosDefMatrix p) : choleskyMeasurableEquiv A = cholesky A

@[simp]

theorem TauCeti.choleskyMeasurableEquiv_symm_apply {p : ℕ} (L : PosDiagLowerTriangular p) : choleskyMeasurableEquiv.symm L = choleskyReconstruction L