map_linearMap_addHaar_pi_eq_smul_addHaar

English

Let ι be finite and f a linear map with det f ≠ 0 on the space ι → ℝ. Then the pushforward of Haar measure μ by f satisfies f_∗μ = |det f|^{-1} μ.

Русский

Пусть ι конечен, а f — линейное отображение с det f ≠ 0 на пространство ι → ℝ. ТогдаGauss мера μ после применения f удовлетворяет f_* μ = |det f|^{-1} μ.

LaTeX

$$$f_*\\mu = |\\det f|^{-1} \\mu$$$

Lean4

theorem map_linearMap_addHaar_pi_eq_smul_addHaar {ι : Type*} [Finite ι] {f : (ι → ℝ) →ₗ[ℝ] ι → ℝ}
    (hf : LinearMap.det f ≠ 0) (μ : Measure (ι → ℝ)) [IsAddHaarMeasure μ] :
    Measure.map f μ = ENNReal.ofReal (abs (LinearMap.det f)⁻¹) • μ :=
  by
  cases nonempty_fintype ι
  have := addHaarMeasure_unique μ (piIcc01 ι)
  rw [this, addHaarMeasure_eq_volume_pi, Measure.map_smul, Real.map_linearMap_volume_pi_eq_smul_volume_pi hf, smul_comm]

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