English
If μ is right-invariant on G, then translating the argument of a nonnegative function by right multiplication by g leaves the Lebesgue integral unchanged.
Русский
Если μ — правая инвариантная на группе G, то перенос аргумента функции вправо на g не изменяет линейный интеграл.
LaTeX
$$$$ \\int_G f(x \\cdot g) \\, d\\mu(x) = \\int_G f(x) \\, d\\mu(x). $$$$
Lean4
/-- Translating a function by right-multiplication does not change its Lebesgue integral
with respect to a right-invariant measure. -/
@[to_additive /-- Translating a function by right-addition does not change its Lebesgue integral with
respect to a right-invariant measure. -/
]
theorem lintegral_mul_right_eq_self [IsMulRightInvariant μ] (f : G → ℝ≥0∞) (g : G) :
(∫⁻ x, f (x * g) ∂μ) = ∫⁻ x, f x ∂μ :=
by
convert (lintegral_map_equiv f <| MeasurableEquiv.mulRight g).symm using 1
simp [map_mul_right_eq_self μ g]
