Measurability in the space of square matrices

Matrix inversion is not continuous: it jumps at the singular matrices, where Mathlib's totalized inverse takes the value 0. It is still measurable, because Cramer's rule writes it as the adjugate — a polynomial in the entries — scaled by the inverse of the determinant, and inversion of scalars is measurable even at zero.

Main results

• TauCeti.measurable_matrix_inv — matrix inversion is measurable, and the MeasurableInv instance it supplies.

theorem TauCeti.measurable_matrix_inv {m : Type u_1} [Fintype m] [DecidableEq m] {𝕜 : Type u_2} [Field 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [MeasurableSpace 𝕜] [BorelSpace 𝕜] [SecondCountableTopology 𝕜] [MeasurableInv 𝕜] : Measurable fun (A : Matrix m m 𝕜) => A⁻¹

Matrix inversion is measurable.

instance TauCeti.instMeasurableInvMatrix_tauCeti {m : Type u_1} [Fintype m] [DecidableEq m] {𝕜 : Type u_2} [Field 𝕜] [TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [MeasurableSpace 𝕜] [BorelSpace 𝕜] [SecondCountableTopology 𝕜] [MeasurableInv 𝕜] : MeasurableInv (Matrix m m 𝕜)

Square matrices inherit MeasurableInv from the measurability of Cramer's rule, which makes the generic measurable_inv API and Measurable.inv dot notation available for matrices.