English
For a finite index set ι and diagonal D with det(diagonal D) ≠ 0, ENNReal.ofReal(|det(diagonal D)|)⁻¹ times the volume after applying the diagonal map equals the original volume.
Русский
Для конечного множества индексeй ι и диагональной матрицы D с det(diagonal D) ≠ 0, ENNReal.ofReal(|det(diagonal D)|)⁻¹ умножение на объём после применения диагонали даёт исходный объём.
LaTeX
$$$$ \\mathrm{ofReal}(|\\det(\\operatorname{diagonal} D)|)^{-1} \\cdot \\mathrm{volume}(\\text{toLin'}(\\operatorname{diagonal} D)) = \\mathrm{volume}. $$$$
Lean4
/-- A diagonal matrix rescales Lebesgue according to its determinant. This is a special case of
`Real.map_matrix_volume_pi_eq_smul_volume_pi`, that one should use instead (and whose proof
uses this particular case). -/
theorem smul_map_diagonal_volume_pi [DecidableEq ι] {D : ι → ℝ} (h : det (diagonal D) ≠ 0) :
ENNReal.ofReal (abs (det (diagonal D))) • Measure.map (toLin' (diagonal D)) volume = volume :=
by
refine (Measure.pi_eq fun s hs => ?_).symm
simp only [det_diagonal, Measure.coe_smul, Algebra.id.smul_eq_mul, Pi.smul_apply]
rw [Measure.map_apply _ (MeasurableSet.univ_pi hs)]
swap; · exact Continuous.measurable (LinearMap.continuous_on_pi _)
have :
(Matrix.toLin' (diagonal D) ⁻¹' Set.pi Set.univ fun i : ι => s i) =
Set.pi Set.univ fun i : ι => (D i * ·) ⁻¹' s i :=
by
ext f
simp only [LinearMap.coe_proj, Algebra.id.smul_eq_mul, LinearMap.smul_apply, mem_univ_pi, mem_preimage,
LinearMap.pi_apply, diagonal_toLin']
have B : ∀ i, ofReal (abs (D i)) * volume ((D i * ·) ⁻¹' s i) = volume (s i) :=
by
intro i
have A : D i ≠ 0 := by
simp only [det_diagonal, Ne] at h
exact Finset.prod_ne_zero_iff.1 h i (Finset.mem_univ i)
rw [volume_preimage_mul_left A, ← mul_assoc, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, mul_inv_cancel₀ A,
abs_one, ENNReal.ofReal_one, one_mul]
rw [this, volume_pi_pi, Finset.abs_prod, ENNReal.ofReal_prod_of_nonneg fun i _ => abs_nonneg (D i), ←
Finset.prod_mul_distrib]
simp only [B]
