English
If μ is invariant under left and/or right translations, then integrals are unchanged by such translations.
Русский
Если μ инвариантна относительно левых и/или правых преобразований, то интегралы не изменяются под такими преобразованиями.
LaTeX
$$$\\int_G f(x) dμ(x) = \\int_G f(gx) dμ(x) = \\int_G f(xg) dμ(x)$ for all g.$$
Lean4
/-- Translating a function by right-multiplication does not change its integral with respect to a
right-invariant measure. -/
@[to_additive /-- Translating a function by right-addition does not change its integral with respect to a
right-invariant measure. -/
]
theorem integral_mul_right_eq_self [IsMulRightInvariant μ] (f : G → E) (g : G) : (∫ x, f (x * g) ∂μ) = ∫ x, f x ∂μ :=
by
have h_mul : MeasurableEmbedding fun x => x * g := (MeasurableEquiv.mulRight g).measurableEmbedding
rw [← h_mul.integral_map, map_mul_right_eq_self]
