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)
:
theorem
Matrix.measurable_iff
{m : Type u_1}
{n : Type u_2}
{α : Type u_3}
[MeasurableSpace α]
{β : Type u_4}
[MeasurableSpace β]
{M : β → Matrix m n α}
:
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
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 α)
The map from m → n → α to Matrix m n α as a measurable equivalence.
Equations
- Matrix.ofMeasurableEquiv m n α = { toEquiv := Matrix.of, measurable_toFun := ⋯, measurable_invFun := ⋯ }
Instances For
theorem
Matrix.coe_ofMeasurableEquiv
(m : Type u_1)
(n : Type u_2)
(α : Type u_3)
[MeasurableSpace α]
:
theorem
Matrix.coe_ofMeasurableEquiv_symm
(m : Type u_1)
(n : Type u_2)
(α : Type u_3)
[MeasurableSpace α]
:
@[simp]
theorem
Matrix.ofMeasurableEquiv_apply
(m : Type u_1)
(n : Type u_2)
(α : Type u_3)
[MeasurableSpace α]
(f : m → n → α)
:
@[simp]
theorem
Matrix.ofMeasurableEquiv_symm_apply
(m : Type u_1)
(n : Type u_2)
(α : Type u_3)
[MeasurableSpace α]
(M : Matrix m n α)
: