addHaar_preimage_linearMap — Mathlib

English

If f is a linear map with det f ≠ 0, then μ(f^{-1}(s)) = |det f|^{-1} μ(s).

Русский

Пусть линейное отображение f удовлетворяет det f ≠ 0. Тогда μ(f^{-1}(S)) = |det f|^{-1} μ(S).

LaTeX

$$$\\mu(f^{-1}(S)) = |\\det f|^{-1} \\mu(S)$$$

Lean4

/-- The preimage of a set `s` under a linear map `f` with nonzero determinant has measure
equal to `μ s` times the absolute value of the inverse of the determinant of `f`. -/
@[simp]
theorem addHaar_preimage_linearMap {f : E →ₗ[ℝ] E} (hf : LinearMap.det f ≠ 0) (s : Set E) :
    μ (f ⁻¹' s) = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s :=
  calc
    μ (f ⁻¹' s) = Measure.map f μ s :=
      ((f.equivOfDetNeZero hf).toContinuousLinearEquiv.toHomeomorph.toMeasurableEquiv.map_apply s).symm
    _ = ENNReal.ofReal |(LinearMap.det f)⁻¹| * μ s := by rw [map_linearMap_addHaar_eq_smul_addHaar μ hf]; rfl

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