English
For any submodule s ≠ ⊤ of a finite-dimensional real vector space E with Haar measure μ, μ(s) = 0.
Русский
Любое подмодуль p ≠ ⊤ в конечномерном вещественном пространстве E имеет нулевую меру μ.
LaTeX
$$$\\mu(s) = 0$$$
Lean4
theorem map_linearMap_addHaar_eq_smul_addHaar {f : E →ₗ[ℝ] E} (hf : LinearMap.det f ≠ 0) :
Measure.map f μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ := by
-- we reduce to the case of `E = ι → ℝ`, for which we have already proved the result using
-- matrices in `map_linearMap_addHaar_pi_eq_smul_addHaar`.
let ι := Fin (finrank ℝ E)
haveI : FiniteDimensional ℝ (ι → ℝ) := by infer_instance
have : finrank ℝ E = finrank ℝ (ι → ℝ) := by simp [ι]
have e : E ≃ₗ[ℝ] ι → ℝ := LinearEquiv.ofFinrankEq E (ι → ℝ) this
obtain ⟨g, hg⟩ : ∃ g, g = (e : E →ₗ[ℝ] ι → ℝ).comp (f.comp (e.symm : (ι → ℝ) →ₗ[ℝ] E)) := ⟨_, rfl⟩
have gdet : LinearMap.det g = LinearMap.det f := by rw [hg]; exact LinearMap.det_conj f e
rw [← gdet] at hf ⊢
have fg : f = (e.symm : (ι → ℝ) →ₗ[ℝ] E).comp (g.comp (e : E →ₗ[ℝ] ι → ℝ)) :=
by
ext x
simp only [LinearEquiv.coe_coe, Function.comp_apply, LinearMap.coe_comp, LinearEquiv.symm_apply_apply, hg]
simp only [fg, LinearEquiv.coe_coe, LinearMap.coe_comp]
have Ce : Continuous e := (e : E →ₗ[ℝ] ι → ℝ).continuous_of_finiteDimensional
have Cg : Continuous g := LinearMap.continuous_of_finiteDimensional g
have Cesymm : Continuous e.symm := (e.symm : (ι → ℝ) →ₗ[ℝ] E).continuous_of_finiteDimensional
rw [← map_map Cesymm.measurable (Cg.comp Ce).measurable, ← map_map Cg.measurable Ce.measurable]
haveI : IsAddHaarMeasure (map e μ) := (e : E ≃+ (ι → ℝ)).isAddHaarMeasure_map μ Ce Cesymm
have ecomp : e.symm ∘ e = id := by ext x; simp only [id, Function.comp_apply, LinearEquiv.symm_apply_apply]
rw [map_linearMap_addHaar_pi_eq_smul_addHaar hf (map e μ), Measure.map_smul, map_map Cesymm.measurable Ce.measurable,
ecomp, Measure.map_id]
