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