map_addHaar_smul — Mathlib

English

The image under a linear map scales by |det f|: μ(f''s) = |det f| μ(s) (nonzero det) or zero otherwise.

Русский

Изображение под линейным отображением масштабируется на |det f|: μ(f''S) = |det f| μ(S) (det ≠ 0), иначе μ(f''S)=0.

LaTeX

$$$\\mu(f''S) = |\\det f| \\mu(S)$$$

Lean4

theorem map_addHaar_smul {r : ℝ} (hr : r ≠ 0) : Measure.map (r • ·) μ = ENNReal.ofReal (abs (r ^ finrank ℝ E)⁻¹) • μ :=
  by
  let f : E →ₗ[ℝ] E := r • (1 : E →ₗ[ℝ] E)
  change Measure.map f μ = _
  have hf : LinearMap.det f ≠ 0 :=
    by
    simp only [f, mul_one, LinearMap.det_smul, Ne, MonoidHom.map_one]
    intro h
    exact hr (pow_eq_zero h)
  simp only [f, map_linearMap_addHaar_eq_smul_addHaar μ hf, mul_one, LinearMap.det_smul, map_one]

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