Measurability of the L2 operator norm and the matrix inverse

The Oseledets / Furstenberg–Kesten development needs that the (scoped) L2 operator norm ‖·‖ and the matrix inverse M ↦ M⁻¹ are measurable as functions on Matrix (Fin d) (Fin d) ℝ equipped with the entrywise (Pi) measurable structure Oseledets.instMeasurableSpaceMatrix.

The subtlety is that Mathlib's Measurable.norm is stated for a BorelSpace, whereas the matrix σ-algebra here is the Pi structure. The L2 operator-norm topology on Matrix (Fin d) (Fin d) ℝ is definitionally the Pi product topology (it is installed via replaceTopology along the entrywise-continuous identification with continuous linear maps of EuclideanSpace), so the Pi measurable structure is exactly the Borel structure of the norm topology. We record the corresponding OpensMeasurableSpace instance and deduce measurability of ‖·‖ from continuity; the matrix inverse is handled entrywise via the adjugate/determinant formula.

Main results

• Oseledets.instOpensMeasurableSpaceMatrix: the Pi measurable structure on square real matrices is an OpensMeasurableSpace for the L2 operator-norm topology.
• Oseledets.measurable_l2_opNorm: the L2 operator norm is measurable.
• Oseledets.measurable_det: the determinant is measurable.
• Oseledets.measurable_inv_matrix: the matrix inverse M ↦ M⁻¹ is measurable.

instance Oseledets.instOpensMeasurableSpaceMatrix {d : ℕ} : OpensMeasurableSpace (Matrix (Fin d) (Fin d) ℝ)

The Pi measurable structure on matrices is the Borel structure of the L2 operator-norm topology (which is definitionally the Pi product topology), so it is an OpensMeasurableSpace.

theorem Oseledets.measurable_l2_opNorm {d : ℕ} : Measurable fun (M : Matrix (Fin d) (Fin d) ℝ) => ‖M‖

Measurability of the L2 operator norm on the entrywise (Pi) measurable structure.

theorem Oseledets.measurable_matrix_entry {d : ℕ} (i j : Fin d) : Measurable fun (M : Matrix (Fin d) (Fin d) ℝ) => M i j

Each matrix entry is measurable.

theorem Oseledets.measurable_det {d : ℕ} : Measurable fun (M : Matrix (Fin d) (Fin d) ℝ) => M.det

The determinant is measurable (a polynomial in the entries).

theorem Oseledets.measurable_adjugate {d : ℕ} : Measurable fun (M : Matrix (Fin d) (Fin d) ℝ) => M.adjugate

The adjugate is measurable (each entry is a determinant of a row update).

theorem Oseledets.measurable_inv_matrix {d : ℕ} : Measurable fun (M : Matrix (Fin d) (Fin d) ℝ) => M⁻¹

Measurability of the matrix inverse M ↦ M⁻¹ on the entrywise measurable structure (M⁻¹ = (det M)⁻¹ • adjugate M, entrywise a ratio of polynomials).