volume_preserving_measurableEquiv

English

The measurable equivalence between the Euclidean space and the index space preserves volume.

Русский

Измеримое эквивалентное отображение между Евклидовым пространством и индексным пространством сохраняет объём.

LaTeX

$$$\\text{volume-preserving observable}$$$

Lean4

/-- The measure equivalence between `EuclideanSpace ℝ ι` and `ι → ℝ` is volume preserving. -/
theorem volume_preserving_measurableEquiv : MeasurePreserving (EuclideanSpace.measurableEquiv ι) :=
  by
  suffices volume = map (EuclideanSpace.measurableEquiv ι).symm volume by
    convert ((EuclideanSpace.measurableEquiv ι).symm.measurable.measurePreserving _).symm
  rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar_def, coe_measurableEquiv_symm, ←
    PiLp.continuousLinearEquiv_symm_apply 2 ℝ, Basis.map_addHaar]
  exact (EuclideanSpace.basisFun _ _).addHaar_eq_volume.symm

Похожие утверждения