Lebesgue measure under matrix vectorization

Matrices over a measure space inherit the product measure on their entries via Matrix.ofMeasurableEquiv. This measure is sigma-finite whenever the entry measure is.

Column-stacking vectorization preserves product Lebesgue measure, also when either index type is empty. Thus a density on Euclidean vector coordinates transfers to a matrix density without a Jacobian factor. The proof regroups product coordinates with TauCeti.measurePreserving_piCurry and uses Mathlib's PiLp.volume_preserving_toLp for the Euclidean volume normalization.

@[instance_reducible]

noncomputable instance Matrix.instMeasureSpace {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype m] [Fintype n] [MeasureTheory.MeasureSpace α] : MeasureTheory.MeasureSpace (Matrix m n α)

Matrices inherit the product measure of their entries.

theorem Matrix.volume_preserving_ofMeasurableEquiv (m : Type u_1) (n : Type u_2) (α : Type u_3) [Fintype m] [Fintype n] [MeasureTheory.MeasureSpace α] : MeasureTheory.MeasurePreserving (⇑(Matrix.ofMeasurableEquiv m n α)) MeasureTheory.volume MeasureTheory.volume

Reading an array of entries as a matrix preserves product volume.

instance Matrix.instSigmaFiniteVolume {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype m] [Fintype n] [MeasureTheory.MeasureSpace α] [MeasureTheory.SigmaFinite MeasureTheory.volume] : MeasureTheory.SigmaFinite MeasureTheory.volume

Product matrix volume is sigma-finite whenever entry volume is.

theorem TauCeti.volume_preserving_matrixVecMeasurableEquiv {m : Type u_1} {n : Type u_2} [Fintype m] [Fintype n] : MeasureTheory.MeasurePreserving (⇑(matrixVecMeasurableEquiv 2)) MeasureTheory.volume MeasureTheory.volume

Column-stacking vectorization carries product Lebesgue measure on real matrices to Euclidean volume on the vectorized coordinates.