English
Same as above: mulEquivHaarChar φ • ∫ f d(μ.map φ) = ∫ f dμ for Haar μ and regular μ.
Русский
То же самое: mulEquivHaarChar φ • ∫ f d(μ.map φ) = ∫ f dμ.
LaTeX
$$$mulEquivHaarChar(\phi) \cdot \int f \; d(μ.map φ) = \int f \; dμ$$$
Lean4
@[to_additive integral_comap_eq_addEquivAddHaarChar_smul]
theorem integral_comap_eq_mulEquivHaarChar_smul (μ : Measure G) [IsHaarMeasure μ] [Regular μ] {f : G → ℝ}
(φ : G ≃ₜ* G) : ∫ a, f a ∂(μ.comap φ) = mulEquivHaarChar φ • ∫ a, f a ∂μ :=
by
let e := φ.toHomeomorph.toMeasurableEquiv
change ∫ a, f a ∂(comap e μ) = mulEquivHaarChar φ • ∫ a, f a ∂μ
have : (map (e.symm) μ).IsHaarMeasure := φ.symm.isHaarMeasure_map μ
have : (map (e.symm) μ).Regular := Regular.map φ.symm.toHomeomorph
rw [← e.map_symm, ← mulEquivHaarChar_smul_integral_map (map e.symm μ) φ,
map_map (by exact φ.toHomeomorph.toMeasurableEquiv.measurable) e.symm.measurable]
-- congr -- breaks to_additive
rw [show ⇑φ ∘ ⇑e.symm = id by ext; simp [e]]
simp
