English
Integrals transform under Haar changes-of-variables similar to standard change-of-variables formula.
Русский
Интегралы преобразуются при изменении переменных в рамках меры Хаара аналогично обычной замене переменных.
LaTeX
$$$\int_G f \ d(μ.map φ) = mulEquivHaarChar φ^{-1} \int_G f \ dμ$$$
Lean4
theorem setIntegral_comp_smul (f : E → F) {R : ℝ} (s : Set E) (hR : R ≠ 0) :
∫ x in s, f (R • x) ∂μ = |(R ^ finrank ℝ E)⁻¹| • ∫ x in R • s, f x ∂μ :=
by
let e : E ≃ᵐ E := (Homeomorph.smul (Units.mk0 R hR)).toMeasurableEquiv
calc
∫ x in s, f (R • x) ∂μ = ∫ x in e ⁻¹' (e.symm ⁻¹' s), f (e x) ∂μ := by simp [← preimage_comp]; rfl
_ = ∫ y in e.symm ⁻¹' s, f y ∂map (fun x ↦ R • x) μ := (setIntegral_map_equiv _ _ _).symm
_ = |(R ^ finrank ℝ E)⁻¹| • ∫ y in e.symm ⁻¹' s, f y ∂μ := by
simp [map_addHaar_smul μ hR, integral_smul_measure, ENNReal.toReal_ofReal, abs_nonneg]
_ = |(R ^ finrank ℝ E)⁻¹| • ∫ x in R • s, f x ∂μ := by
congr 3
ext y
rw [mem_smul_set_iff_inv_smul_mem₀ hR]
rfl
