English
The image of a set under a linear map scales by the absolute value of the determinant: μ(f''s) = |det f| μ(s) if det f ≠ 0; otherwise the image has zero measure when the determinant is zero.
Русский
Образ множества под линейным отображением масштабируется по модулю детерминанта: μ(f''S) = |det f| μ(S), если det f ≠ 0; иначе образ имеет нулевую меру при det f = 0.
LaTeX
$$$\\mu(f''S) = |\\det f| \\mu(S) \\quad(\\det f \\neq 0),\\quad \\mu(f''S) = 0 \\quad(\\det f = 0)$$$
Lean4
/-- The image of a set `s` under a linear map `f` has measure
equal to `μ s` times the absolute value of the determinant of `f`. -/
@[simp]
theorem addHaar_image_linearMap (f : E →ₗ[ℝ] E) (s : Set E) : μ (f '' s) = ENNReal.ofReal |LinearMap.det f| * μ s :=
by
rcases ne_or_eq (LinearMap.det f) 0 with (hf | hf)
· let g := (f.equivOfDetNeZero hf).toContinuousLinearEquiv
change μ (g '' s) = _
rw [ContinuousLinearEquiv.image_eq_preimage g s, addHaar_preimage_continuousLinearEquiv]
congr
· simp only [hf, zero_mul, ENNReal.ofReal_zero, abs_zero]
have : μ (LinearMap.range f) = 0 := addHaar_submodule μ _ (LinearMap.range_lt_top_of_det_eq_zero hf).ne
exact le_antisymm (le_trans (measure_mono (image_subset_range _ _)) this.le) (zero_le _)
