English
Let G act on α by a measurable action and μ be a SMul-invariant measure on α. Then the integral of f(g • x) over α with respect to μ equals the integral of f(x) for all g ∈ G.
Русский
Пусть G действует на α измеримо, и μ — мера на α, сохраняемая под умножением. Тогда интеграл от f(g • x) по μ равен интегралу от f(x) по μ для всех g.
LaTeX
$$$$ \\mathrm{Integrable}(f, \\mu) \\Rightarrow \\forall g \\in G, \\; \\int_\\alpha f(g \\cdot x) \\, d\\mu(x) = \\int_\\alpha f(x) \\, d\\mu(x). $$$$
Lean4
@[to_additive]
theorem integral_mconv [NormedSpace ℝ F] [SFinite μ] [SFinite ν] (hf : Integrable f (μ ∗ₘ ν)) :
∫ x, f x ∂(μ ∗ₘ ν) = ∫ x, ∫ y, f (x * y) ∂ν ∂μ :=
by
unfold Measure.mconv
rw [integral_map (by fun_prop) hf.1, integral_prod]
exact (integrable_map_measure hf.1 (by fun_prop)).mp hf
