Measurable space structure on Matrices

If α is a measurable space, we set the measurable space structure on Matrix m n α to be the same as the one on m → n → α.

@[instance_reducible]

instance Matrix.instMeasurableSpace {m : Type u_1} {n : Type u_2} {α : Type u_3} [MeasurableSpace α] : MeasurableSpace (Matrix m n α)

theorem Measurable.eval_matrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [MeasurableSpace α] {β : Type u_4} [MeasurableSpace β] {i : m} {j : n} {M : β → Matrix m n α} (hM : Measurable M) : Measurable fun (x : β) => M x i j

theorem Measurable.of_eval_matrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [MeasurableSpace α] {β : Type u_4} [MeasurableSpace β] (M : β → Matrix m n α) (hM : ∀ (i : m) (j : n), Measurable fun (x : β) => M x i j) : Measurable M

theorem Matrix.measurable_iff {m : Type u_1} {n : Type u_2} {α : Type u_3} [MeasurableSpace α] {β : Type u_4} [MeasurableSpace β] {M : β → Matrix m n α} : Measurable M ↔ ∀ (i : m) (j : n), Measurable fun (x : β) => M x i j

theorem Matrix.measurable_apply {m : Type u_1} {n : Type u_2} {α : Type u_3} [MeasurableSpace α] {i : m} {j : n} : Measurable fun (M : Matrix m n α) => M i j

theorem Matrix.measurable_of (m : Type u_1) (n : Type u_2) (α : Type u_3) [MeasurableSpace α] : Measurable ⇑of

instance Matrix.instBorelSpaceOfCountableOfSecondCountableTopology (m : Type u_1) (n : Type u_2) (α : Type u_3) [MeasurableSpace α] [Countable m] [Countable n] [TopologicalSpace α] [SecondCountableTopology α] [BorelSpace α] : BorelSpace (Matrix m n α)

def Matrix.ofMeasurableEquiv (m : Type u_1) (n : Type u_2) (α : Type u_3) [MeasurableSpace α] : (m → n → α) ≃ᵐ Matrix m n α

The map from m → n → α to Matrix m n α as a measurable equivalence.

theorem Matrix.coe_ofMeasurableEquiv (m : Type u_1) (n : Type u_2) (α : Type u_3) [MeasurableSpace α] : ⇑(Matrix.ofMeasurableEquiv m n α) = ⇑of

theorem Matrix.coe_ofMeasurableEquiv_symm (m : Type u_1) (n : Type u_2) (α : Type u_3) [MeasurableSpace α] : ⇑(Matrix.ofMeasurableEquiv m n α).symm = ⇑of.symm

@[simp]

theorem Matrix.ofMeasurableEquiv_apply (m : Type u_1) (n : Type u_2) (α : Type u_3) [MeasurableSpace α] (f : m → n → α) : (Matrix.ofMeasurableEquiv m n α) f = of f

@[simp]

theorem Matrix.ofMeasurableEquiv_symm_apply (m : Type u_1) (n : Type u_2) (α : Type u_3) [MeasurableSpace α] (M : Matrix m n α) : (Matrix.ofMeasurableEquiv m n α).symm M = of.symm M