English
For a domain action g on α and a function f, the integral under the action equals the integral of f evaluated at the transformed argument.
Русский
Для действия домена g на область и функции f интеграл равен интегралу от f, оцениваемому по преобразованному аргументу.
LaTeX
$$$$\int x, f(x) \partial g \!\cdot \mu = \int x, f((DomMulAct.mk.symm g)^{-1} \cdot x) \partial\mu.$$$$
Lean4
theorem integral_map {β} [MeasurableSpace β] {φ : α → β} (hφ : AEMeasurable φ μ) {f : β → G}
(hfm : AEStronglyMeasurable f (Measure.map φ μ)) : ∫ y, f y ∂Measure.map φ μ = ∫ x, f (φ x) ∂μ :=
let g := hfm.mk f
calc
∫ y, f y ∂Measure.map φ μ = ∫ y, g y ∂Measure.map φ μ := integral_congr_ae hfm.ae_eq_mk
_ = ∫ y, g y ∂Measure.map (hφ.mk φ) μ := by congr 1; exact Measure.map_congr hφ.ae_eq_mk
_ = ∫ x, g (hφ.mk φ x) ∂μ := (integral_map_of_stronglyMeasurable hφ.measurable_mk hfm.stronglyMeasurable_mk)
_ = ∫ x, g (φ x) ∂μ := (integral_congr_ae (hφ.ae_eq_mk.symm.fun_comp _))
_ = ∫ x, f (φ x) ∂μ := integral_congr_ae <| ae_eq_comp hφ hfm.ae_eq_mk.symm
